From fe38333f3152f1757f9b85d47aec2e23b33aacce Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 14 Jul 2026 20:01:36 +0200 Subject: restructure --- CoalgebraicMuCalculus.lean | 3 + CoalgebraicMuCalculus/AlternationDepth.lean | 165 +++++++++++++++ CoalgebraicMuCalculus/FixedPoints.lean | 51 +++++ CoalgebraicMuCalculus/Instances/Relational.lean | 58 ++++++ CoalgebraicMuCalculus/MuCalculus.lean | 254 ++++++++++++++++++++++++ SymbolicModalLogic.lean | 3 - SymbolicModalLogic/AlternationDepth.lean | 165 --------------- SymbolicModalLogic/FixedPoints.lean | 51 ----- SymbolicModalLogic/Instances/Relational.lean | 58 ------ SymbolicModalLogic/MuCalculus.lean | 254 ------------------------ lake-manifest.json | 213 +++++++++++--------- lakefile.toml | 6 +- 12 files changed, 651 insertions(+), 630 deletions(-) create mode 100644 CoalgebraicMuCalculus.lean create mode 100644 CoalgebraicMuCalculus/AlternationDepth.lean create mode 100644 CoalgebraicMuCalculus/FixedPoints.lean create mode 100644 CoalgebraicMuCalculus/Instances/Relational.lean create mode 100644 CoalgebraicMuCalculus/MuCalculus.lean delete mode 100644 SymbolicModalLogic.lean delete mode 100644 SymbolicModalLogic/AlternationDepth.lean delete mode 100644 SymbolicModalLogic/FixedPoints.lean delete mode 100644 SymbolicModalLogic/Instances/Relational.lean delete mode 100644 SymbolicModalLogic/MuCalculus.lean diff --git a/CoalgebraicMuCalculus.lean b/CoalgebraicMuCalculus.lean new file mode 100644 index 0000000..e58c455 --- /dev/null +++ b/CoalgebraicMuCalculus.lean @@ -0,0 +1,3 @@ +import CoalgebraicMuCalculus.FixedPoints +import CoalgebraicMuCalculus.MuCalculus +import CoalgebraicMuCalculus.Instances.Relational diff --git a/CoalgebraicMuCalculus/AlternationDepth.lean b/CoalgebraicMuCalculus/AlternationDepth.lean new file mode 100644 index 0000000..fae628d --- /dev/null +++ b/CoalgebraicMuCalculus/AlternationDepth.lean @@ -0,0 +1,165 @@ +import CoalgebraicMuCalculus.MuCalculus +import Mathlib + +inductive FixedPointOp where + | μ + | ν + deriving DecidableEq + +variable {Λ : Type} [Modalities Λ] +open Formula + +inductive IsAlternationDepthBound : FixedPointOp → ℕ → Formula Λ → Prop where + | top {η : FixedPointOp} : IsAlternationDepthBound η 0 .top + | bot {η : FixedPointOp} : IsAlternationDepthBound η 0 .bot + | var {η : FixedPointOp} (x : ℕ) : IsAlternationDepthBound η 0 (.var x) + | or {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} : + IsAlternationDepthBound η n φ → + IsAlternationDepthBound η n ψ → + IsAlternationDepthBound η n (.or φ ψ) + | and {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} : + IsAlternationDepthBound η n φ → + IsAlternationDepthBound η n ψ → + IsAlternationDepthBound η n (.and φ ψ) + | modality {η : FixedPointOp} {n : ℕ} {l : Λ} {args : Modalities.signature l → Formula Λ} : + (∀ l, IsAlternationDepthBound η n (args l)) → + IsAlternationDepthBound η n (.modality l args) + | lfp {n : ℕ} {φ : Formula Λ} : + IsAlternationDepthBound .ν n φ → + IsAlternationDepthBound .ν n (μ, φ) + | gfp {n : ℕ} {φ : Formula Λ} : + IsAlternationDepthBound .μ n φ → + IsAlternationDepthBound .μ n (ν, φ) + | subst {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} {x : ℕ} : + IsAlternationDepthBound η n φ → + IsAlternationDepthBound η n ψ → + IsAlternationDepthBound η n (φ.subst (x, ψ)) + | up {η₁ η₂ : FixedPointOp} {n : ℕ} {φ : Formula Λ} : + IsAlternationDepthBound η₁ n φ → + IsAlternationDepthBound η₂ (n + 1) φ + +noncomputable def alternationDepth (φ : Formula Λ) : ℕ := + sInf { n : ℕ | IsAlternationDepthBound .μ n φ ∧ IsAlternationDepthBound .ν n φ } + +def Formula.closure : Formula Λ → List (ℕ × Formula Λ) + | .top => [(0, ⊤)] + | .bot => [(0, ⊥)] + | .or φ ψ => [(0, φ ∨ ψ)] ++ closure φ ++ closure ψ + | .and φ ψ => [(0, φ ∧ ψ)] ++ closure φ ++ closure ψ + | .modality l args => + [(0, .modality l args)] ++ (Modalities.args l |>.flatMap fun a ↦ closure (args a)) + | .var x => [(0, ^x)] + | .lfp φ => [(0, μ, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ)) + | .gfp φ => [(0, ν, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ)) + +def mentionsVar (n : ℕ) : Formula Λ → Bool + | .top => false + | .bot => false + | .or φ ψ => mentionsVar n φ || mentionsVar n ψ + | .and φ ψ => mentionsVar n φ || mentionsVar n ψ + | .modality l args => + Modalities.args l |>.any fun a ↦ mentionsVar n (args a) + | .var x => x == n + | .lfp φ => mentionsVar (n + 1) φ + | .gfp φ => mentionsVar (n + 1) φ + +def size : Formula Λ → ℕ + | .top => 1 + | .bot => 1 + | .or φ ψ => 1 + size φ + size ψ + | .and φ ψ => 1 + size φ + size ψ + | .modality l args => + 1 + (Modalities.args l |>.map (fun a ↦ size (args a)) |>.sum) + | .var _ => 1 + | .lfp φ => 1 + size φ + | .gfp φ => 1 + size φ + +lemma closure_mem_size (φ : Formula Λ) : ∀ {n ψ}, (n, ψ) ∈ φ.closure → size ψ ≤ size φ := by + intro n χ + induction φ generalizing n χ with + | top => grind [Formula.closure] + | bot => grind [Formula.closure] + | or φ ψ hφ hψ => + intro h + simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h + cases h with + | inl eq => rw [eq.right] + | inr h => cases h <;> grind [size] + | and φ ψ hφ hψ => + intro h + simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h + cases h with + | inl eq => rw [eq.right] + | inr h => cases h <;> grind [size] + | modality l args hargs => + intro h + simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_flatMap] at h + cases h with + | inl eq => rw [eq.right] + | inr h => + obtain ⟨a, _, ha⟩ := h + simp only [size] + grw [hargs _ ha] + apply Nat.le_add_left_of_le + apply List.le_sum_of_mem + apply List.mem_map_of_mem + apply Modalities.args_mem + | var x => grind [Formula.closure] + | lfp φ hφ => + intro h + simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h + cases h with + | inl eq => rw [eq.right] + | inr h => obtain ⟨_, h, _⟩ := h; grind [size] + | gfp φ hφ => + intro h + simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h + cases h with + | inl eq => rw [eq.right] + | inr h => obtain ⟨_, h, _⟩ := h; grind [size] + +def ad : Formula Λ → ℕ + | .top => 0 + | .bot => 0 + | .or φ ψ => Nat.max (ad φ) (ad ψ) + | .and φ ψ => Nat.max (ad φ) (ad ψ) + | .modality l args => + Modalities.args l + |>.map (fun a ↦ ad (args a)) + |> List.foldr Nat.max 0 + | .var _ => 0 + | .lfp φ => Id.run do + let mut n := Nat.max 1 (ad φ) + for h : (offset, ψ) in closure φ do + if h' : mentionsVar offset ψ then + if let Formula.gfp χ := ψ then + n := Nat.max n (ad (ν, χ) + 1) + return n + | .gfp φ => Id.run do + let mut n := Nat.max 1 (ad φ) + for h : (offset, ψ) in closure φ do + if h' : mentionsVar offset ψ then + if let Formula.lfp χ := ψ then + n := Nat.max n (ad (μ, χ) + 1) + return n + termination_by φ => size φ + decreasing_by + · grind [size] + · grind [size] + · grind [size] + · grind [size] + · rw [size, Nat.lt_one_add_iff] + apply List.le_sum_of_mem + apply List.mem_map_of_mem + apply Modalities.args_mem + · grind [size] + · rw [show size (μ, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff] + apply closure_mem_size + exact h + · grind [size] + · rw [show size (ν, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff] + apply closure_mem_size + exact h + +lemma ad_eq_alternationDepth (φ : Formula Λ) : ad φ = alternationDepth φ := by + sorry diff --git a/CoalgebraicMuCalculus/FixedPoints.lean b/CoalgebraicMuCalculus/FixedPoints.lean new file mode 100644 index 0000000..58d768c --- /dev/null +++ b/CoalgebraicMuCalculus/FixedPoints.lean @@ -0,0 +1,51 @@ +import Mathlib + +variable {α : Type} [CompleteLattice α] + +structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where + fixedPt : Function.IsFixedPt f x + least : ∀ y, Function.IsFixedPt f y → x ≤ y + +structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where + fixedPt : Function.IsFixedPt f x + greatest : ∀ y, Function.IsFixedPt f y → y ≤ x + +namespace FixedPoints + +def lfp (f : α → α) : α := sInf { x | f x ≤ x } + +def gfp (f : α → α) : α := sSup { x | x ≤ f x } + +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] + +-- 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/CoalgebraicMuCalculus/Instances/Relational.lean b/CoalgebraicMuCalculus/Instances/Relational.lean new file mode 100644 index 0000000..0b0f7fc --- /dev/null +++ b/CoalgebraicMuCalculus/Instances/Relational.lean @@ -0,0 +1,58 @@ +import Mathlib +import CoalgebraicMuCalculus.MuCalculus + +inductive Relational where + | box + | diamond + deriving Repr + +namespace Relational + +instance : Modalities Relational where + signature _ := Unit + dual + | .box => .diamond + | .diamond => .box + dualSignature + | .box, f => f + | .diamond, f => f + dual_involution := by intro l; cases l <;> simp + +instance : Model Relational Set where + lifting + | .box, A => { B | B ⊆ A () } + | .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/CoalgebraicMuCalculus/MuCalculus.lean b/CoalgebraicMuCalculus/MuCalculus.lean new file mode 100644 index 0000000..5d4cab9 --- /dev/null +++ b/CoalgebraicMuCalculus/MuCalculus.lean @@ -0,0 +1,254 @@ +import Mathlib +import CoalgebraicMuCalculus.FixedPoints + +class Modalities (Λ : Type) where + signature : Λ → Type + [signature_finenum : ∀ l, FinEnum (signature l)] + dual : Λ → Λ + dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α) + dual_involution : ∀ l, dual (dual l) = l + +def Modalities.args {Λ : Type} [Modalities Λ] (l : Λ) : List (Modalities.signature l) := + have : FinEnum (signature l) := Modalities.signature_finenum l + FinEnum.toList (signature l) + +def Modalities.args_mem {Λ : Type} [Modalities Λ] (l : Λ) (a : Modalities.signature l) : a ∈ args l := by + rw [args] + apply @FinEnum.mem_toList _ (Modalities.signature_finenum l) + +inductive Formula (Λ : Type) [Modalities Λ] where + | top : Formula Λ + | bot : Formula Λ + | or : Formula Λ → Formula Λ → Formula Λ + | and : Formula Λ → Formula Λ → Formula Λ + | modality : (l : Λ) → (args : Modalities.signature l → Formula Λ) → Formula Λ + | var : ℕ → Formula Λ + | lfp : Formula Λ → Formula Λ + | gfp : Formula Λ → Formula Λ + +namespace Formula + +scoped notation "⊤" => Formula.top +scoped notation "⊥" => Formula.bot +scoped infixl:30 " ∨ " => Formula.or +scoped infixl:35 " ∧ " => Formula.and +scoped notation "^" n:max => Formula.var n +scoped notation "μ, " φ => Formula.lfp φ +scoped notation "ν, " φ => Formula.gfp φ + +variable {Λ : Type} [Modalities Λ] + +instance [Repr Λ] : ToString (Formula Λ) where + toString := + let rec impl : Formula Λ → String + | .top => "⊤" + | .bot => "⊥" + | .or φ ψ => s!"({impl φ}) ∨ ({impl ψ})" + | .and φ ψ => s!"({impl φ}) ∧ ({impl ψ})" + | .var x => s!"^{x}" + | .modality l args => + have : FinEnum (Modalities.signature l) := Modalities.signature_finenum l + let argsStr := FinEnum.toList (Modalities.signature l) + |>.map (fun a ↦ impl (args a)) + |> String.intercalate ", " + s!"{reprStr l}({argsStr})" + | .lfp φ => s!"μ, {impl φ}" + | .gfp φ => s!"ν, {impl φ}" + impl + +def not : Formula Λ → Formula Λ + | .top => ⊥ + | .bot => ⊤ + | .or φ ψ => (not φ) ∧ (not ψ) + | .and φ ψ => (not φ) ∨ (not ψ) + | .modality l args => .modality (Modalities.dual l) (Modalities.dualSignature l fun a ↦ not (args a)) + | .var x => ^x + | .lfp φ => ν, not φ + | .gfp φ => μ, not φ + +scoped notation "¬" φ:60 => Formula.not φ +scoped infixl:25 " ⇒ " => fun φ ψ ↦ ¬φ ∨ ψ + +def up : Formula Λ → (start : ℕ := 0) → Formula Λ + | .top, _ => ⊤ + | .bot, _ => ⊥ + | .or φ ψ, start => up φ start ∨ up ψ start + | .and φ ψ, start => up φ start ∧ up ψ start + | .modality l args, start => .modality l fun a ↦ up (args a) start + | .var x, start => if x < start then ^x else ^(x + 1) + | .lfp φ, start => μ, up φ (start + 1) + | .gfp φ, start => ν, up φ (start + 1) + +scoped notation "⇑ " φ => Formula.up φ + +def subst : Formula Λ → (ℕ × Formula Λ) → Formula Λ + | .top, _ => ⊤ + | .bot, _ => ⊥ + | .or φ ψ, σ => subst φ σ ∨ subst ψ σ + | .and φ ψ, σ => subst φ σ ∧ subst ψ σ + | .modality l args, σ => .modality l fun a ↦ subst (args a) σ + | .var x, (y, ψ) => if x < y then ^x else + if x > y then ^(x - 1) else + ψ + | .lfp φ, (y, ψ) => μ, subst φ (y + 1, ⇑ψ) + | .gfp φ, (y, ψ) => ν, subst φ (y + 1, ⇑ψ) + +macro_rules + | `($φ[$ψ/^$n]) => `(Formula.subst $φ ($n, $ψ)) + +end Formula + +section Semantics + +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) : + (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) → Model.lift l F args ⊆ Model.lift l F args' + lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) : + 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] + +def Environment (X : Type) : Type := ℕ → Set X + +namespace Environment + +variable {X : Type} + +def empty : Environment X := λ _ ↦ ∅ + +def up (xs : Environment X) : Environment X + | 0 => ∅ + | n + 1 => xs n + +def subst (xs : Environment X) (n : ℕ) (x : Set X) : Environment X := + λ m ↦ if m = n then x else xs m + +scoped notation "⇑ " φ => Environment.up φ + +def add (x : Set X) (xs : Environment X) : Environment X := subst (⇑ xs) 0 x + +infixr:67 " :: " => Environment.add + +variable {xs : Environment X} {x y : Set X} {n m : ℕ} + +@[simp] +lemma subst_eq : subst xs n x n = x := by simp [subst] + +@[simp] +lemma subst_neq : m ≠ n → subst xs n x m = xs m := by intro h; simp [subst, h] + +@[simp] +lemma subst_subst_eq : subst (subst xs n x) n y = subst xs n y := by + apply funext + intro m + by_cases h : m = n <;> simp [h] + +lemma subst_subst_neq : m ≠ n → subst (subst xs n x) m y = subst (subst xs m y) n x := by + intro hneq + apply funext + intro k + by_cases h₁ : k = m <;> by_cases h₂ : k = n <;> simp [h₁, h₂, hneq, Ne.symm hneq] + +lemma subst_up : (⇑(subst xs n x)) = subst (⇑xs) (n + 1) x := by + apply funext + intro m + cases m with + | zero => simp [up] + | succ m => by_cases h : m = n <;> simp [h, up] + +lemma subst_add : x :: subst xs n y = subst (x :: xs) (n + 1) y := by + rw [add, add, subst_subst_neq, subst_up] + simp + +end Environment + +def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X + | .top, _ => Set.univ + | .bot, _ => ∅ + | .or φ ψ, xs => (interp γ φ xs) ∪ (interp γ ψ xs) + | .and φ ψ, xs => (interp γ φ xs) ∩ (interp γ ψ 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 [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 => + intro S S' hle + rfl + | bot => + intro S S' hle + rfl + | or φ ψ ihφ ihψ => + intro S S' hle + simp only [Set.le_eq_subset, Set.union_subset_iff, interp] + constructor + · apply Set.subset_union_of_subset_left + exact ihφ xs n hle + · apply Set.subset_union_of_subset_right + exact ihψ xs n hle + | and φ ψ ihφ ihψ => + intro S S' hle + simp only [Set.le_eq_subset, Set.subset_inter_iff, interp] + constructor + · intro x ⟨hx, _⟩ + exact ihφ xs n hle hx + · intro x ⟨_, hx⟩ + exact ihψ xs n hle hx + | modality l args ih => + intro S S' hle + simp only [Set.le_eq_subset] + apply Set.preimage_mono + apply LawfulModel.lifting_monotone + intro a + exact ih a xs n hle + | var x => + intro S S' hle + by_cases h : x = n + · simp only [interp, h, Environment.subst_eq, Set.le_eq_subset] + exact hle + · simp [h, interp] + | lfp φ ihφ => + intro S S' hle + 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 + interp γ φ (U :: xs.subst n S) = interp γ φ ((U :: xs).subst (n + 1) S) := by rw [Environment.subst_add] + _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle + _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] + _ ⊆ U := hU + | gfp φ ihφ => + intro S S' hle + 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 + U ⊆ interp γ φ (U :: xs.subst n S) := hU + _ = interp γ φ ((U :: xs).subst (n + 1) S) := by rw [Environment.subst_add] + _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle + _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] + · exact hx + +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_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] + +end Semantics diff --git a/SymbolicModalLogic.lean b/SymbolicModalLogic.lean deleted file mode 100644 index dd1d18a..0000000 --- a/SymbolicModalLogic.lean +++ /dev/null @@ -1,3 +0,0 @@ -import SymbolicModalLogic.FixedPoints -import SymbolicModalLogic.MuCalculus -import SymbolicModalLogic.Instances.Relational diff --git a/SymbolicModalLogic/AlternationDepth.lean b/SymbolicModalLogic/AlternationDepth.lean deleted file mode 100644 index 717c928..0000000 --- a/SymbolicModalLogic/AlternationDepth.lean +++ /dev/null @@ -1,165 +0,0 @@ -import SymbolicModalLogic.MuCalculus -import Mathlib - -inductive FixedPointOp where - | μ - | ν - deriving DecidableEq - -variable {Λ : Type} [Modalities Λ] -open Formula - -inductive IsAlternationDepthBound : FixedPointOp → ℕ → Formula Λ → Prop where - | top {η : FixedPointOp} : IsAlternationDepthBound η 0 .top - | bot {η : FixedPointOp} : IsAlternationDepthBound η 0 .bot - | var {η : FixedPointOp} (x : ℕ) : IsAlternationDepthBound η 0 (.var x) - | or {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} : - IsAlternationDepthBound η n φ → - IsAlternationDepthBound η n ψ → - IsAlternationDepthBound η n (.or φ ψ) - | and {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} : - IsAlternationDepthBound η n φ → - IsAlternationDepthBound η n ψ → - IsAlternationDepthBound η n (.and φ ψ) - | modality {η : FixedPointOp} {n : ℕ} {l : Λ} {args : Modalities.signature l → Formula Λ} : - (∀ l, IsAlternationDepthBound η n (args l)) → - IsAlternationDepthBound η n (.modality l args) - | lfp {n : ℕ} {φ : Formula Λ} : - IsAlternationDepthBound .ν n φ → - IsAlternationDepthBound .ν n (μ, φ) - | gfp {n : ℕ} {φ : Formula Λ} : - IsAlternationDepthBound .μ n φ → - IsAlternationDepthBound .μ n (ν, φ) - | subst {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} {x : ℕ} : - IsAlternationDepthBound η n φ → - IsAlternationDepthBound η n ψ → - IsAlternationDepthBound η n (φ.subst (x, ψ)) - | up {η₁ η₂ : FixedPointOp} {n : ℕ} {φ : Formula Λ} : - IsAlternationDepthBound η₁ n φ → - IsAlternationDepthBound η₂ (n + 1) φ - -noncomputable def alternationDepth (φ : Formula Λ) : ℕ := - sInf { n : ℕ | IsAlternationDepthBound .μ n φ ∧ IsAlternationDepthBound .ν n φ } - -def Formula.closure : Formula Λ → List (ℕ × Formula Λ) - | .top => [(0, ⊤)] - | .bot => [(0, ⊥)] - | .or φ ψ => [(0, φ ∨ ψ)] ++ closure φ ++ closure ψ - | .and φ ψ => [(0, φ ∧ ψ)] ++ closure φ ++ closure ψ - | .modality l args => - [(0, .modality l args)] ++ (Modalities.args l |>.flatMap fun a ↦ closure (args a)) - | .var x => [(0, ^x)] - | .lfp φ => [(0, μ, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ)) - | .gfp φ => [(0, ν, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ)) - -def mentionsVar (n : ℕ) : Formula Λ → Bool - | .top => false - | .bot => false - | .or φ ψ => mentionsVar n φ || mentionsVar n ψ - | .and φ ψ => mentionsVar n φ || mentionsVar n ψ - | .modality l args => - Modalities.args l |>.any fun a ↦ mentionsVar n (args a) - | .var x => x == n - | .lfp φ => mentionsVar (n + 1) φ - | .gfp φ => mentionsVar (n + 1) φ - -def size : Formula Λ → ℕ - | .top => 1 - | .bot => 1 - | .or φ ψ => 1 + size φ + size ψ - | .and φ ψ => 1 + size φ + size ψ - | .modality l args => - 1 + (Modalities.args l |>.map (fun a ↦ size (args a)) |>.sum) - | .var _ => 1 - | .lfp φ => 1 + size φ - | .gfp φ => 1 + size φ - -lemma closure_mem_size (φ : Formula Λ) : ∀ {n ψ}, (n, ψ) ∈ φ.closure → size ψ ≤ size φ := by - intro n χ - induction φ generalizing n χ with - | top => grind [Formula.closure] - | bot => grind [Formula.closure] - | or φ ψ hφ hψ => - intro h - simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h - cases h with - | inl eq => rw [eq.right] - | inr h => cases h <;> grind [size] - | and φ ψ hφ hψ => - intro h - simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h - cases h with - | inl eq => rw [eq.right] - | inr h => cases h <;> grind [size] - | modality l args hargs => - intro h - simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_flatMap] at h - cases h with - | inl eq => rw [eq.right] - | inr h => - obtain ⟨a, _, ha⟩ := h - simp only [size] - grw [hargs _ ha] - apply Nat.le_add_left_of_le - apply List.le_sum_of_mem - apply List.mem_map_of_mem - apply Modalities.args_mem - | var x => grind [Formula.closure] - | lfp φ hφ => - intro h - simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h - cases h with - | inl eq => rw [eq.right] - | inr h => obtain ⟨_, h, _⟩ := h; grind [size] - | gfp φ hφ => - intro h - simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h - cases h with - | inl eq => rw [eq.right] - | inr h => obtain ⟨_, h, _⟩ := h; grind [size] - -def ad : Formula Λ → ℕ - | .top => 0 - | .bot => 0 - | .or φ ψ => Nat.max (ad φ) (ad ψ) - | .and φ ψ => Nat.max (ad φ) (ad ψ) - | .modality l args => - Modalities.args l - |>.map (fun a ↦ ad (args a)) - |> List.foldr Nat.max 0 - | .var _ => 0 - | .lfp φ => Id.run do - let mut n := Nat.max 1 (ad φ) - for h : (offset, ψ) in closure φ do - if h' : mentionsVar offset ψ then - if let Formula.gfp χ := ψ then - n := Nat.max n (ad (ν, χ) + 1) - return n - | .gfp φ => Id.run do - let mut n := Nat.max 1 (ad φ) - for h : (offset, ψ) in closure φ do - if h' : mentionsVar offset ψ then - if let Formula.lfp χ := ψ then - n := Nat.max n (ad (μ, χ) + 1) - return n - termination_by φ => size φ - decreasing_by - · grind [size] - · grind [size] - · grind [size] - · grind [size] - · rw [size, Nat.lt_one_add_iff] - apply List.le_sum_of_mem - apply List.mem_map_of_mem - apply Modalities.args_mem - · grind [size] - · rw [show size (μ, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff] - apply closure_mem_size - exact h - · grind [size] - · rw [show size (ν, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff] - apply closure_mem_size - exact h - -lemma ad_eq_alternationDepth (φ : Formula Λ) : ad φ = alternationDepth φ := by - sorry diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean deleted file mode 100644 index 58d768c..0000000 --- a/SymbolicModalLogic/FixedPoints.lean +++ /dev/null @@ -1,51 +0,0 @@ -import Mathlib - -variable {α : Type} [CompleteLattice α] - -structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where - fixedPt : Function.IsFixedPt f x - least : ∀ y, Function.IsFixedPt f y → x ≤ y - -structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where - fixedPt : Function.IsFixedPt f x - greatest : ∀ y, Function.IsFixedPt f y → y ≤ x - -namespace FixedPoints - -def lfp (f : α → α) : α := sInf { x | f x ≤ x } - -def gfp (f : α → α) : α := sSup { x | x ≤ f x } - -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] - --- 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 deleted file mode 100644 index 81d428d..0000000 --- a/SymbolicModalLogic/Instances/Relational.lean +++ /dev/null @@ -1,58 +0,0 @@ -import Mathlib -import SymbolicModalLogic.MuCalculus - -inductive Relational where - | box - | diamond - deriving Repr - -namespace Relational - -instance : Modalities Relational where - signature _ := Unit - dual - | .box => .diamond - | .diamond => .box - dualSignature - | .box, f => f - | .diamond, f => f - dual_involution := by intro l; cases l <;> simp - -instance : Model Relational Set where - lifting - | .box, A => { B | B ⊆ A () } - | .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 deleted file mode 100644 index 4722928..0000000 --- a/SymbolicModalLogic/MuCalculus.lean +++ /dev/null @@ -1,254 +0,0 @@ -import Mathlib -import SymbolicModalLogic.FixedPoints - -class Modalities (Λ : Type) where - signature : Λ → Type - [signature_finenum : ∀ l, FinEnum (signature l)] - dual : Λ → Λ - dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α) - dual_involution : ∀ l, dual (dual l) = l - -def Modalities.args {Λ : Type} [Modalities Λ] (l : Λ) : List (Modalities.signature l) := - have : FinEnum (signature l) := Modalities.signature_finenum l - FinEnum.toList (signature l) - -def Modalities.args_mem {Λ : Type} [Modalities Λ] (l : Λ) (a : Modalities.signature l) : a ∈ args l := by - rw [args] - apply @FinEnum.mem_toList _ (Modalities.signature_finenum l) - -inductive Formula (Λ : Type) [Modalities Λ] where - | top : Formula Λ - | bot : Formula Λ - | or : Formula Λ → Formula Λ → Formula Λ - | and : Formula Λ → Formula Λ → Formula Λ - | modality : (l : Λ) → (args : Modalities.signature l → Formula Λ) → Formula Λ - | var : ℕ → Formula Λ - | lfp : Formula Λ → Formula Λ - | gfp : Formula Λ → Formula Λ - -namespace Formula - -scoped notation "⊤" => Formula.top -scoped notation "⊥" => Formula.bot -scoped infixl:30 " ∨ " => Formula.or -scoped infixl:35 " ∧ " => Formula.and -scoped notation "^" n:max => Formula.var n -scoped notation "μ, " φ => Formula.lfp φ -scoped notation "ν, " φ => Formula.gfp φ - -variable {Λ : Type} [Modalities Λ] - -instance [Repr Λ] : ToString (Formula Λ) where - toString := - let rec impl : Formula Λ → String - | .top => "⊤" - | .bot => "⊥" - | .or φ ψ => s!"({impl φ}) ∨ ({impl ψ})" - | .and φ ψ => s!"({impl φ}) ∧ ({impl ψ})" - | .var x => s!"^{x}" - | .modality l args => - have : FinEnum (Modalities.signature l) := Modalities.signature_finenum l - let argsStr := FinEnum.toList (Modalities.signature l) - |>.map (fun a ↦ impl (args a)) - |> String.intercalate ", " - s!"{reprStr l}({argsStr})" - | .lfp φ => s!"μ, {impl φ}" - | .gfp φ => s!"ν, {impl φ}" - impl - -def not : Formula Λ → Formula Λ - | .top => ⊥ - | .bot => ⊤ - | .or φ ψ => (not φ) ∧ (not ψ) - | .and φ ψ => (not φ) ∨ (not ψ) - | .modality l args => .modality (Modalities.dual l) (Modalities.dualSignature l fun a ↦ not (args a)) - | .var x => ^x - | .lfp φ => ν, not φ - | .gfp φ => μ, not φ - -scoped notation "¬" φ:60 => Formula.not φ -scoped infixl:25 " ⇒ " => fun φ ψ ↦ ¬φ ∨ ψ - -def up : Formula Λ → (start : ℕ := 0) → Formula Λ - | .top, _ => ⊤ - | .bot, _ => ⊥ - | .or φ ψ, start => up φ start ∨ up ψ start - | .and φ ψ, start => up φ start ∧ up ψ start - | .modality l args, start => .modality l fun a ↦ up (args a) start - | .var x, start => if x < start then ^x else ^(x + 1) - | .lfp φ, start => μ, up φ (start + 1) - | .gfp φ, start => ν, up φ (start + 1) - -scoped notation "⇑ " φ => Formula.up φ - -def subst : Formula Λ → (ℕ × Formula Λ) → Formula Λ - | .top, _ => ⊤ - | .bot, _ => ⊥ - | .or φ ψ, σ => subst φ σ ∨ subst ψ σ - | .and φ ψ, σ => subst φ σ ∧ subst ψ σ - | .modality l args, σ => .modality l fun a ↦ subst (args a) σ - | .var x, (y, ψ) => if x < y then ^x else - if x > y then ^(x - 1) else - ψ - | .lfp φ, (y, ψ) => μ, subst φ (y + 1, ⇑ψ) - | .gfp φ, (y, ψ) => ν, subst φ (y + 1, ⇑ψ) - -macro_rules - | `($φ[$ψ/^$n]) => `(Formula.subst $φ ($n, $ψ)) - -end Formula - -section Semantics - -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) : - (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) → Model.lift l F args ⊆ Model.lift l F args' - lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) : - 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] - -def Environment (X : Type) : Type := ℕ → Set X - -namespace Environment - -variable {X : Type} - -def empty : Environment X := λ _ ↦ ∅ - -def up (xs : Environment X) : Environment X - | 0 => ∅ - | n + 1 => xs n - -def subst (xs : Environment X) (n : ℕ) (x : Set X) : Environment X := - λ m ↦ if m = n then x else xs m - -scoped notation "⇑ " φ => Environment.up φ - -def add (x : Set X) (xs : Environment X) : Environment X := subst (⇑ xs) 0 x - -infixr:67 " :: " => Environment.add - -variable {xs : Environment X} {x y : Set X} {n m : ℕ} - -@[simp] -lemma subst_eq : subst xs n x n = x := by simp [subst] - -@[simp] -lemma subst_neq : m ≠ n → subst xs n x m = xs m := by intro h; simp [subst, h] - -@[simp] -lemma subst_subst_eq : subst (subst xs n x) n y = subst xs n y := by - apply funext - intro m - by_cases h : m = n <;> simp [h] - -lemma subst_subst_neq : m ≠ n → subst (subst xs n x) m y = subst (subst xs m y) n x := by - intro hneq - apply funext - intro k - by_cases h₁ : k = m <;> by_cases h₂ : k = n <;> simp [h₁, h₂, hneq, Ne.symm hneq] - -lemma subst_up : (⇑(subst xs n x)) = subst (⇑xs) (n + 1) x := by - apply funext - intro m - cases m with - | zero => simp [up] - | succ m => by_cases h : m = n <;> simp [h, up] - -lemma subst_add : x :: subst xs n y = subst (x :: xs) (n + 1) y := by - rw [add, add, subst_subst_neq, subst_up] - simp - -end Environment - -def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X - | .top, _ => Set.univ - | .bot, _ => ∅ - | .or φ ψ, xs => (interp γ φ xs) ∪ (interp γ ψ xs) - | .and φ ψ, xs => (interp γ φ xs) ∩ (interp γ ψ 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 [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 => - intro S S' hle - rfl - | bot => - intro S S' hle - rfl - | or φ ψ ihφ ihψ => - intro S S' hle - simp only [Set.le_eq_subset, Set.union_subset_iff, interp] - constructor - · apply Set.subset_union_of_subset_left - exact ihφ xs n hle - · apply Set.subset_union_of_subset_right - exact ihψ xs n hle - | and φ ψ ihφ ihψ => - intro S S' hle - simp only [Set.le_eq_subset, Set.subset_inter_iff, interp] - constructor - · intro x ⟨hx, _⟩ - exact ihφ xs n hle hx - · intro x ⟨_, hx⟩ - exact ihψ xs n hle hx - | modality l args ih => - intro S S' hle - simp only [Set.le_eq_subset] - apply Set.preimage_mono - apply LawfulModel.lifting_monotone - intro a - exact ih a xs n hle - | var x => - intro S S' hle - by_cases h : x = n - · simp only [interp, h, Environment.subst_eq, Set.le_eq_subset] - exact hle - · simp [h, interp] - | lfp φ ihφ => - intro S S' hle - 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 - interp γ φ (U :: xs.subst n S) = interp γ φ ((U :: xs).subst (n + 1) S) := by rw [Environment.subst_add] - _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle - _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] - _ ⊆ U := hU - | gfp φ ihφ => - intro S S' hle - 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 - U ⊆ interp γ φ (U :: xs.subst n S) := hU - _ = interp γ φ ((U :: xs).subst (n + 1) S) := by rw [Environment.subst_add] - _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle - _ = interp γ φ (U :: xs.subst n S') := by rw [Environment.subst_add] - · exact hx - -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_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] - -end Semantics diff --git a/lake-manifest.json b/lake-manifest.json index 190adef..fc5713b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,96 +1,117 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a456461b368b71d2accd95234832cd9c174b5437", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.99", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "558915ae105bfd8074e22d597613d1961822adc2", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "32dc18cde3684679f3c003de608743b57498c56f", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "SymbolicModalLogic", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.99", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "CoalgebraicMuCalculus", + "lakeDir": ".lake", + "fixedToolchain": false +} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index d6fcfd6..5730c3f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,6 @@ -name = "SymbolicModalLogic" +name = "CoalgebraicMuCalculus" version = "0.1.0" -defaultTargets = ["SymbolicModalLogic"] +defaultTargets = ["CoalgebraicMuCalculus"] [[require]] name = "mathlib" @@ -8,4 +8,4 @@ scope = "leanprover-community" rev = "v4.30.0" [[lean_lib]] -name = "SymbolicModalLogic" +name = "CoalgebraicMuCalculus" -- cgit v1.3.1