diff options
Diffstat (limited to 'SymbolicModalLogic')
| -rw-r--r-- | SymbolicModalLogic/AlternationDepth.lean | 165 | ||||
| -rw-r--r-- | SymbolicModalLogic/FixedPoints.lean | 51 | ||||
| -rw-r--r-- | SymbolicModalLogic/Instances/Relational.lean | 58 | ||||
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 254 |
4 files changed, 0 insertions, 528 deletions
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 |