diff options
| -rw-r--r-- | SymbolicModalLogic/FixedPoints.lean | 73 | ||||
| -rw-r--r-- | SymbolicModalLogic/Instances/Relational.lean | 85 | ||||
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 39 |
3 files changed, 90 insertions, 107 deletions
diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean index 2074992..58d768c 100644 --- a/SymbolicModalLogic/FixedPoints.lean +++ b/SymbolicModalLogic/FixedPoints.lean @@ -1,46 +1,51 @@ import Mathlib -namespace FixedPoints - variable {α : Type} [CompleteLattice α] -def lfp (f : α → α) : α := sInf { x | f x ≤ x } +structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where + fixedPt : Function.IsFixedPt f x + least : ∀ y, Function.IsFixedPt f y → x ≤ y -def gfp (f : α → α) : α := sSup { x | x ≤ f x } +structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where + fixedPt : Function.IsFixedPt f x + greatest : ∀ y, Function.IsFixedPt f y → y ≤ x -lemma lfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (lfp f) := by - have hmem : f (lfp f) ≤ lfp f := by - rw [lfp, le_sInf_iff] - intro x hx - grw [h (sInf_le hx)] - exact hx - apply Std.IsPartialOrder.le_antisymm - · exact hmem - · exact (sInf_le (h hmem)) +namespace FixedPoints -lemma lfp_is_least (f : α → α) : - ∀ x, Function.IsFixedPt f x → lfp f ≤ x := by - intro x hfix - apply sInf_le - simp [show f x = x from hfix] +def lfp (f : α → α) : α := sInf { x | f x ≤ x } --- TODO: Avoid repitition +def gfp (f : α → α) : α := sSup { x | x ≤ f x } -lemma gfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (gfp f) := by - have hmem : gfp f ≤ f (gfp f) := by - rw [gfp, sSup_le_iff] - intro x hx - grw [show x ≤ f x from hx] - exact h (le_sSup hx) - apply Std.IsPartialOrder.le_antisymm - · apply le_sSup - exact h hmem - · exact hmem +lemma lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where + fixedPt := by + have hmem : f (lfp f) ≤ lfp f := by + rw [lfp, le_sInf_iff] + intro x hx + grw [hf (sInf_le hx)] + exact hx + apply Std.IsPartialOrder.le_antisymm + · exact hmem + · exact (sInf_le (hf hmem)) + least := by + intro x hfix + apply sInf_le + simp [show f x = x from hfix] -lemma gfp_is_greatest (f : α → α) : - ∀ x, Function.IsFixedPt f x → x ≤ gfp f := by - intro x hfix - apply le_sSup - simp [show f x = x from hfix] +-- TODO: Avoid repitition +lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where + fixedPt := by + have hmem : gfp f ≤ f (gfp f) := by + rw [gfp, sSup_le_iff] + intro x hx + grw [show x ≤ f x from hx] + exact hf (le_sSup hx) + apply Std.IsPartialOrder.le_antisymm + · apply le_sSup + exact hf hmem + · exact hmem + greatest := by + intro x hfix + apply le_sSup + simp [show f x = x from hfix] end FixedPoints diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean index 840a6b5..4c9155b 100644 --- a/SymbolicModalLogic/Instances/Relational.lean +++ b/SymbolicModalLogic/Instances/Relational.lean @@ -20,57 +20,38 @@ instance : Modalities Relational where instance : Model Relational Set where lifting | .box, A => { B | B ⊆ A () } - | .diamond, A => { B | A () ∩ B ≠ ∅ } - lifting_natural {X Y} f - | .box => by simp - | .diamond => by - intro A; ext B - simp only [Set.mem_setOf_eq, Set.preimage_setOf_eq, Set.fmap_eq_image] - rw [← Set.nonempty_iff_ne_empty, ← Set.nonempty_iff_ne_empty] - show (∃ x, x ∈ f ⁻¹' A () ∧ x ∈ B) ↔ (∃ x, x ∈ A () ∧ x ∈ f '' B) - constructor - · intro ⟨x, h₁, h₂⟩ - use f x; exact ⟨Set.mem_preimage.mpr h₁, Set.mem_image_of_mem f h₂⟩ - · intro ⟨fx, h₁, h₂⟩ - rw [Set.mem_image] at h₂ - obtain ⟨x, hx₁, hx₂⟩ := h₂ - use x; rw [Set.mem_preimage, hx₂]; exact ⟨h₁, hx₁⟩ - lifting_monotone {X} - | .box => by - intro A A' h - simp only [Set.setOf_subset_setOf] - intro B hB; trans - · exact hB - · exact h () - | .diamond => by - intro A A' h - simp only [Set.setOf_subset_setOf, ← Set.nonempty_iff_ne_empty] - intro B ⟨x, hx₁, hx₂⟩; use x - exact ⟨h () hx₁, hx₂⟩ - lifting_dual {X} - | .box => by - intro A; ext B - simp only [Set.mem_setOf_eq, Modalities.dualSignature, ← Set.nonempty_iff_ne_empty] - constructor - · intro ⟨x, hx₁, hx₂⟩ hcontra - exact hcontra hx₂ hx₁ - · show (¬(∀ x ∈ B, x ∈ (A ()).compl)) → (A () ∩ B).Nonempty - simp only [not_forall] - intro ⟨x, hx₁, hx₂⟩ - use x - exact ⟨Set.not_notMem.mp hx₂, hx₁⟩ - | .diamond => by - intro A; ext B - simp only [Modalities.dualSignature, Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty] - show (∀ x ∈ B, x ∈ A ()) ↔ ¬(∃ x, x ∈ (A ()).compl ∩ B) - rw [not_exists] - constructor - · intro h; by_contra - simp only [Set.mem_inter_iff, not_and, not_forall, not_not] at this - obtain ⟨x, hx₁, hx₂⟩ := this - exact hx₁ (h x hx₂) - · intro h x hx; by_contra - simp only [Set.mem_inter_iff, not_and] at h - exact h x this hx + | .diamond, A => { B | B ∩ A () ≠ ∅ } + +@[simp] +lemma lift_box_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.box Set A ↔ ∀ x ∈ B, x ∈ A () := by + show B ∈ { B | B ⊆ A () } ↔ ∀ x ∈ B, x ∈ A () + exact Set.mem_setOf + +@[simp] +lemma lift_diamond_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.diamond Set A ↔ ∃ x ∈ B, x ∈ A () := by + show B ∈ { B | B ∩ A () ≠ ∅ } ↔ ∃ x ∈ B, x ∈ A () + rw [Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty] + rfl + +instance : LawfulModel Relational Set where + lifting_natural {X Y} f l := by + cases l + all_goals intro A; ext B; simp + lifting_monotone {X} l := by + cases l with + | box => + intro A A' h B hB + rw [lift_box_iff]; intro x hx + rw [lift_box_iff] at hB + exact h () (hB x hx) + | diamond => + intro A A' h B hB + rw [lift_diamond_iff] at hB + obtain ⟨x, hx⟩ := hB + rw [lift_diamond_iff]; use x + exact ⟨hx.left, h () hx.right⟩ + lifting_dual {X} l := by + cases l + all_goals intro A; ext B; simp [Modalities.dual, Modalities.dualSignature] end Relational diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean index cad6a75..73d04f4 100644 --- a/SymbolicModalLogic/MuCalculus.lean +++ b/SymbolicModalLogic/MuCalculus.lean @@ -74,14 +74,19 @@ end Formula section Semantics -class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] where +class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] where lifting {X : Type} (l : Λ) : (args : Modalities.signature l → Set X) → Set (F X) + +abbrev Model.lift {Λ : Type} [Modalities Λ] (l : Λ) (F : Type → Type) [Functor F] [Model Λ F] {X : Type} : (args : Modalities.signature l → Set X) → Set (F X) := + Model.lifting l + +class LawfulModel (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] [Model Λ F] where lifting_natural {X Y : Type} (f : X → Y) (l : Λ) (args : Modalities.signature l → Set Y) : - (lifting l fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (lifting l args)) + (Model.lift l F fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (Model.lift l F args)) lifting_monotone {X : Type} (l : Λ) (args args' : Modalities.signature l → Set X) : - (∀ a, args a ⊆ args' a) → lifting l args ⊆ lifting l args' + (∀ a, args a ⊆ args' a) → Model.lift l F args ⊆ Model.lift l F args' lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) : - lifting (Modalities.dual l) (Modalities.dualSignature l args) = Set.compl (lifting l fun a ↦ Set.compl (args a)) + Model.lift (Modalities.dual l) F (Modalities.dualSignature l args) = (Model.lift l F fun a ↦ (args a)ᶜ)ᶜ variable {Λ : Type} [Modalities Λ] variable {F : Type → Type} [Functor F] [LawfulFunctor F] [Model Λ F] @@ -145,12 +150,12 @@ def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X | .bot, _ => ∅ | .or φ ψ, xs => (interp γ φ xs) ∪ (interp γ ψ xs) | .and φ ψ, xs => (interp γ φ xs) ∩ (interp γ ψ xs) - | .modality l args, xs => γ ⁻¹' Model.lifting l fun a ↦ interp γ (args a) xs + | .modality l args, xs => γ ⁻¹' Model.lift l F fun a ↦ interp γ (args a) xs | .var x, xs => xs x | .lfp φ, xs => FixedPoints.lfp fun S ↦ interp γ φ (S :: xs) | .gfp φ, xs => FixedPoints.gfp fun S ↦ interp γ φ (S :: xs) -def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) : +def interp_subst_monotone [LawfulModel Λ F] {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) : Monotone fun x ↦ interp γ φ (xs.subst n x) := by induction φ generalizing xs n with | top => @@ -179,7 +184,7 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En intro S S' hle simp only [Set.le_eq_subset] apply Set.preimage_mono - apply Model.lifting_monotone + apply LawfulModel.lifting_monotone intro a exact ih a xs n hle | var x => @@ -210,22 +215,14 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] · exact hx -lemma interp_lfp_isFixedPt {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.lfp φ) xs) := by - apply FixedPoints.lfp_isFixedPt +lemma interp_lfp_isLeastFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : + Function.IsLeastFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.lfp φ) xs) := by + apply FixedPoints.lfp_isLeastFixedPt simp [Environment.add, interp_subst_monotone] -lemma interp_lfp_is_least {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - ∀ x, Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) x → interp γ (.lfp φ) xs ⊆ x := by - apply FixedPoints.lfp_is_least - -lemma interp_gfp_isFixedPt {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.gfp φ) xs) := by - apply FixedPoints.gfp_isFixedPt +lemma interp_gfp_isGreatestFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : + Function.IsGreatestFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.gfp φ) xs) := by + apply FixedPoints.gfp_isGreatestFixedPt simp [Environment.add, interp_subst_monotone] -lemma interp_gfp_is_greatest {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) : - ∀ x, Function.IsFixedPt (fun S ↦ interp γ φ (S :: xs)) x → x ⊆ interp γ (.gfp φ) xs := by - apply FixedPoints.gfp_is_greatest - end Semantics |