-
Notifications
You must be signed in to change notification settings - Fork 197
feat(Logic): General Modal Logic #863
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
fmontesi
wants to merge
15
commits into
main
Choose a base branch
from
fmontesi/multimodal
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
15 commits
Select commit
Hold shift + click to select a range
eb6d1e4
multimodal logic begings
fmontesi 5fc60be
General Modal Logic
fmontesi ad6a5db
some polishing
fmontesi 9956ebd
some grind tests
fmontesi f3910fb
unimodal cube tests
fmontesi e6c0cac
add false and rebase on or
fmontesi 38a031a
add truth
fmontesi d6bd382
HML as a specific unary logic
fmontesi d090f27
merge main
fmontesi d78aa6e
import fix
fmontesi aa29158
Merge branch 'main' into fmontesi/multimodal
fmontesi 6a63033
merge main
fmontesi 629a6f0
Merge branch 'main' into fmontesi/multimodal
fmontesi fbb3ce4
generalise finiteAnd/Or and make HML have the same interface
fmontesi 781f2fd
lint errors
fmontesi File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| /- | ||
| Copyright (c) 2026 Fabrizio Montesi. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Fabrizio Montesi | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Init | ||
| public import Mathlib.Data.PFunctor.Univariate.Basic | ||
|
|
||
| /-! # Additional basic theory on polynomial functors -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace PFunctor | ||
|
|
||
| /-- The constant child map for `a`. -/ | ||
| def const {P : PFunctor} (a : P.A) (x : α) : P.B a → α := fun _ => x | ||
|
|
||
| @[simp, scoped grind =] | ||
| theorem const_apply {P : PFunctor} (a : P.A) (x : α) (i : P.B a) : PFunctor.const a x i = x := rfl | ||
|
|
||
| section Unary | ||
|
|
||
| /-- A polynomial functor is unary if all child types have exactly one element. -/ | ||
| class Unary (P : PFunctor) where | ||
| unary (a : P.A) : Unique (P.B a) | ||
|
|
||
| attribute [instance_reducible, instance] PFunctor.Unary.unary | ||
|
|
||
| theorem Unary.fun_eq_const [Unary P] | ||
| (a : P.A) (f : P.B a → α) : f = fun _ => f default := by | ||
| funext i | ||
| exact congrArg f (Subsingleton.elim i default) | ||
|
|
||
| /-- A polynomial functor has children with decidable equality. -/ | ||
| class DecidableEqChildren (P : PFunctor) where | ||
| decidableEq (a : P.A) : DecidableEq (P.B a) | ||
|
|
||
| attribute [instance_reducible, instance] DecidableEqChildren.decidableEq | ||
|
|
||
| /-- A unary polynomial functor has decidable child equality. -/ | ||
| instance (P : PFunctor) [P.Unary] : P.DecidableEqChildren where | ||
| decidableEq _ _ _ := isTrue (Subsingleton.elim _ _) | ||
|
|
||
| /-- Constructs a unary polynomial functor. -/ | ||
| abbrev mkUnary (A : Type*) : PFunctor where | ||
| A := A | ||
| B := fun _ => Unit | ||
|
|
||
| instance {A : Type u} : (mkUnary A).Unary where | ||
| unary _ := by | ||
| change Unique Unit | ||
| infer_instance | ||
|
|
||
| end Unary | ||
|
|
||
| end PFunctor | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,105 @@ | ||
| /- | ||
| Copyright (c) 2026 Fabrizio Montesi. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Fabrizio Montesi | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Init | ||
| public import Cslib.Foundations.Data.PFunctor.Basic | ||
|
|
||
| /-! # Modal Frames | ||
|
|
||
| A frame is a structure of relations, each with its own arity. | ||
|
|
||
| ## Implementation notes | ||
|
|
||
| Frames for general modal logic were formulated with modal similarity types [Blackburn2001], which | ||
| we generalise here to arbitrary polynomial functors. | ||
|
|
||
| ## References | ||
|
|
||
| * [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Cslib | ||
|
|
||
| /-- A frame is an indexed structure of potentially heterogeneous relations. | ||
|
|
||
| Frames are typically used in combination with modal logics or akin concepts. This is why we use | ||
| `op` (for operator) to range over relation indexes. | ||
| -/ | ||
| structure Frame World (τ : PFunctor) where | ||
| /-- Accessibility relations. -/ | ||
| r : (op : τ.A) → World → (τ.B op → World) → Prop | ||
|
|
||
| namespace Frame | ||
|
|
||
| /-- The binary relation obtained by observing position `i` of the worlds accessible via `op`. -/ | ||
| def project (f : Frame World τ) (op : τ.A) (i : τ.B op) : World → World → Prop := | ||
| fun w w' => ∃ ws, f.r op w ws ∧ ws i = w' | ||
|
|
||
| /-- The binary relation induced by restricting the accessibility relation of `op` | ||
| to constant tuples of worlds. -/ | ||
| @[instance_reducible] | ||
| def diagonal (f : Frame World τ) (op : τ.A) : World → World → Prop := | ||
| fun w w' => f.r op w (fun _ => w') | ||
|
|
||
| @[scoped grind →, modal →] | ||
| theorem r_const_of_diagonal {f : Frame World τ} (h : f.diagonal op w w') : | ||
| f.r op w (fun _ => w') := by grind [Frame.diagonal] | ||
|
|
||
| @[scoped grind →, modal →] | ||
| theorem diagonal_of_r [PFunctor.Unary τ] {f : Frame World τ} (h : f.r op w ws) : | ||
| f.diagonal op w (ws default) := by grind [Frame.diagonal, PFunctor.Unary.fun_eq_const op ws] | ||
|
|
||
| /-- A frame is diagonally symmetric at `op` if, whenever `w` accesses `ws`, some component of `ws` | ||
| accesses the constant sequence at `w`. -/ | ||
| class DiagonalSymm (f : Frame World τ) (op : τ.A) where | ||
| symm w ws : f.r op w ws → ∃ i, f.r op (ws i) (fun _ => w) | ||
|
|
||
| /-- A frame is transitive at `op` if accessibility can be composed through any accessible component: | ||
| whenever `w` accesses `ws₁` and `ws₁ i` accesses `ws₂`, then `w` accesses `ws₂`. | ||
| -/ | ||
| class Trans (f : Frame World τ) (op : τ.A) where | ||
| trans w ws₁ i ws₂ : f.r op w ws₁ → f.r op (ws₁ i) ws₂ → f.r op w ws₂ | ||
|
|
||
| instance (f : Frame World τ) [f.Trans op] (i : τ.B op) : | ||
| IsTrans World (f.project op i) where | ||
| trans w₁ w₂ w₃ h₁ h₂ := by | ||
| rcases h₁ with ⟨ws₁, hr₁, rfl⟩ | ||
| rcases h₂ with ⟨ws₂, hr₂, h⟩ | ||
| exact ⟨ws₂, Frame.Trans.trans _ _ _ _ hr₁ hr₂, h⟩ | ||
|
|
||
| /-- A frame is right Euclidean at `op` if, whenever a world `w` accesses two tuples `ws₁` and | ||
| `ws₂`, some component of `ws₂` accesses `ws₁`. -/ | ||
| class RightEuclidean (f : Frame World τ) (op : τ.A) where | ||
| rightEuclidean w ws₁ ws₂ : f.r op w ws₁ → f.r op w ws₂ → ∃ i, f.r op (ws₂ i) ws₁ | ||
|
|
||
| /-- A predicate map `Ps` is preserved from `P` by `op` if, whenever `P` holds at a world `w`, | ||
| then for every tuple `ws` accessible from `w` via `op`, each component `ws i` satisfies the | ||
| corresponding predicate `Ps i`. -/ | ||
| def PreservesMap (f : Frame α τ) (op : τ.A) (P : α → Prop) (Ps : τ.B op → α → Prop) : Prop := | ||
| ∀ w ws, f.r op w ws → P w → ∃ i, Ps i (ws i) | ||
|
|
||
| /-- Builds a unary frame from an indexed family of binary relations. -/ | ||
| def ofRelations {τ : PFunctor} [τ.Unary] (r : τ.A → World → World → Prop) : | ||
| Frame World τ where | ||
| r i w ws := r i w (ws default) | ||
|
|
||
| @[scoped grind =, modal =] | ||
| lemma ofRelations_iff {τ : PFunctor} [τ.Unary] (r : τ.A → World → World → Prop) (i : τ.A) | ||
| (w : World) (ws : τ.B i → World) : (ofRelations r).r i w ws ↔ r i w (ws default) := by rfl | ||
|
|
||
| @[simp, scoped grind =, modal =] | ||
| lemma ofRelations_diagonal_iff {τ : PFunctor} [τ.Unary] | ||
| (r : τ.A → World → World → Prop) (i : τ.A) (w w' : World) : | ||
| (ofRelations r).diagonal i w w' ↔ r i w w' := by | ||
| rfl | ||
|
|
||
| end Frame | ||
|
|
||
| end Cslib |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR seems a bit large. Maybe this API for PFunctors could be a separate PR. It seems fairly straightforward merge.