diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-06-15 21:00:06 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-06-15 21:00:06 +0200 |
| commit | 44cbada3881c34d81bd8a74f041eaf7469f1ac74 (patch) | |
| tree | 66bc46680cd8b9b1e1e3b11f5cb0f2f420bf252a /SymbolicModalLogic/MuCalculus.lean | |
| parent | e9ef4cb62cda496667507d47686d7e167f83a126 (diff) | |
fixed point theorems
Diffstat (limited to 'SymbolicModalLogic/MuCalculus.lean')
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 27 |
1 files changed, 23 insertions, 4 deletions
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 |