diff options
Diffstat (limited to 'SymbolicModalLogic')
| -rw-r--r-- | SymbolicModalLogic/FixedPoints.lean | 46 | ||||
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 27 |
2 files changed, 69 insertions, 4 deletions
diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean new file mode 100644 index 0000000..2074992 --- /dev/null +++ b/SymbolicModalLogic/FixedPoints.lean @@ -0,0 +1,46 @@ +import Mathlib + +namespace FixedPoints + +variable {α : Type} [CompleteLattice α] + +def lfp (f : α → α) : α := sInf { x | f x ≤ x } + +def gfp (f : α → α) : α := sSup { x | x ≤ f 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)) + +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] + +-- TODO: Avoid repitition + +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 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] + +end FixedPoints diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean index a2e322e..cad6a75 100644 --- a/SymbolicModalLogic/MuCalculus.lean +++ b/SymbolicModalLogic/MuCalculus.lean @@ -1,4 +1,5 @@ import Mathlib +import SymbolicModalLogic.FixedPoints class Modalities (Λ : Type) where signature : Λ → Type @@ -146,8 +147,8 @@ def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X | .and φ ψ, xs => (interp γ φ xs) ∩ (interp γ ψ xs) | .modality l args, xs => γ ⁻¹' Model.lifting l fun a ↦ interp γ (args a) xs | .var x, xs => xs x - | .lfp φ, xs => ⋂₀ { S | interp γ φ (S :: xs) ⊆ S } - | .gfp φ, xs => ⋃₀ { S | S ⊆ interp γ φ (S :: xs) } + | .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 : ℕ) : Monotone fun x ↦ interp γ φ (xs.subst n x) := by @@ -189,7 +190,7 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En · simp [h, interp] | lfp φ ihφ => intro S S' hle - simp only [interp, Set.le_eq_subset, Set.subset_sInter_iff, Set.mem_setOf_eq] + simp only [interp, Set.le_eq_subset, FixedPoints.lfp, Set.sInf_eq_sInter, Set.subset_sInter_iff, Set.mem_setOf_eq] intro U hU x hx apply hx calc @@ -199,7 +200,7 @@ def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : En _ ⊆ U := hU | gfp φ ihφ => intro S S' hle - simp only [interp, Set.le_eq_subset, Set.sUnion_subset_iff, Set.mem_setOf_eq] + simp only [interp, Set.le_eq_subset, FixedPoints.gfp, Set.sSup_eq_sUnion, Set.sUnion_subset_iff, Set.mem_setOf_eq] intro U hU x hx use U; constructor · calc @@ -209,4 +210,22 @@ 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 + 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 + 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 |