From 31fb1ca4f13a15184ff7ee49420ccbf13a92e08e Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 21 May 2026 14:48:41 +0200 Subject: [PATCH 1/6] Logical operators --- Cslib.lean | 5 ++++ Cslib/Foundations/Logic/Operators/And.lean | 24 +++++++++++++++++++ Cslib/Foundations/Logic/Operators/Box.lean | 24 +++++++++++++++++++ .../Foundations/Logic/Operators/Diamond.lean | 24 +++++++++++++++++++ Cslib/Foundations/Logic/Operators/Not.lean | 24 +++++++++++++++++++ Cslib/Foundations/Logic/Operators/Tensor.lean | 24 +++++++++++++++++++ 6 files changed, 125 insertions(+) create mode 100644 Cslib/Foundations/Logic/Operators/And.lean create mode 100644 Cslib/Foundations/Logic/Operators/Box.lean create mode 100644 Cslib/Foundations/Logic/Operators/Diamond.lean create mode 100644 Cslib/Foundations/Logic/Operators/Not.lean create mode 100644 Cslib/Foundations/Logic/Operators/Tensor.lean diff --git a/Cslib.lean b/Cslib.lean index b504973c3..a1529e356 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -68,6 +68,11 @@ public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence +public import Cslib.Foundations.Logic.Operators.And +public import Cslib.Foundations.Logic.Operators.Box +public import Cslib.Foundations.Logic.Operators.Diamond +public import Cslib.Foundations.Logic.Operators.Not +public import Cslib.Foundations.Logic.Operators.Tensor public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS diff --git a/Cslib/Foundations/Logic/Operators/And.lean b/Cslib/Foundations/Logic/Operators/And.lean new file mode 100644 index 000000000..65a3633a6 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/And.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Init + +/-! # And connective (∧) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has an and connective (∧). -/ +class HasAnd (α : Type*) where + /-- `a ∧ b` is the conjunction of `a` and `b`. -/ + and (a b : α) : α + +@[inherit_doc] scoped infix:35 " ∧ " => HasAnd.and + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Box.lean b/Cslib/Foundations/Logic/Operators/Box.lean new file mode 100644 index 000000000..5b9dcd7e4 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Box.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Init + +/-! # Box modality (□) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has a box modality (□). -/ +class HasBox (α : Type*) where + /-- `a` is valid in all immediately reachable states. -/ + box (a : α) : α + +@[inherit_doc] scoped prefix:40 "□" => HasBox.box + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Diamond.lean b/Cslib/Foundations/Logic/Operators/Diamond.lean new file mode 100644 index 000000000..c37416abf --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Diamond.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Init + +/-! # Diamond modality (◇) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has a diamond modality (◇). -/ +class HasDiamond (α : Type*) where + /-- `a` is valid in a reachable state. -/ + diamond (a : α) : α + +@[inherit_doc] scoped prefix:40 "◇" => HasDiamond.diamond + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Not.lean b/Cslib/Foundations/Logic/Operators/Not.lean new file mode 100644 index 000000000..40b89eb0f --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Not.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Init + +/-! # Negation connective (¬) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has a negation connective (¬). -/ +class HasNot (α : Type*) where + /-- `¬a` is the negation of `a`. -/ + not (a : α) : α + +@[inherit_doc] scoped prefix:40 "¬" => HasNot.not + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Tensor.lean b/Cslib/Foundations/Logic/Operators/Tensor.lean new file mode 100644 index 000000000..69cf13b15 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Tensor.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Init + +/-! # Tensor connective (⊗) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has a tensor connective (⊗). -/ +class HasTensor (α : Type*) where + /-- `a ⊗ b` is the multiplicative conjunction of `a` and `b`. -/ + tensor (a b : α) : α + +@[inherit_doc] scoped infix:35 " ⊗ " => HasTensor.tensor + +end Cslib.Logic From 31dcc0e4a9eac44d2c9e40797413e2781a3f1d32 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 27 May 2026 00:56:08 +0200 Subject: [PATCH 2/6] PL connectives, start modal --- Cslib/Foundations/Logic/Operators/And.lean | 4 +- Cslib/Foundations/Logic/Operators/Box.lean | 2 +- .../Foundations/Logic/Operators/Diamond.lean | 2 +- Cslib/Foundations/Logic/Operators/Impl.lean | 24 +++++++++ Cslib/Foundations/Logic/Operators/Not.lean | 4 +- Cslib/Foundations/Logic/Operators/Or.lean | 24 +++++++++ Cslib/Foundations/Logic/Operators/Tensor.lean | 2 +- Cslib/Logics/Modal/Basic.lean | 49 +++++++++++++++---- Cslib/Logics/Propositional/Defs.lean | 19 ++++--- 9 files changed, 106 insertions(+), 24 deletions(-) create mode 100644 Cslib/Foundations/Logic/Operators/Impl.lean create mode 100644 Cslib/Foundations/Logic/Operators/Or.lean diff --git a/Cslib/Foundations/Logic/Operators/And.lean b/Cslib/Foundations/Logic/Operators/And.lean index 65a3633a6..f562e919c 100644 --- a/Cslib/Foundations/Logic/Operators/And.lean +++ b/Cslib/Foundations/Logic/Operators/And.lean @@ -14,11 +14,11 @@ public import Cslib.Init namespace Cslib.Logic -/-- The type `α` has an and connective (∧). -/ +/-- The type `α` has an and connective (`∧`). -/ class HasAnd (α : Type*) where /-- `a ∧ b` is the conjunction of `a` and `b`. -/ and (a b : α) : α -@[inherit_doc] scoped infix:35 " ∧ " => HasAnd.and +@[inherit_doc] scoped infixr:36 " ∧ " => HasAnd.and end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Box.lean b/Cslib/Foundations/Logic/Operators/Box.lean index 5b9dcd7e4..19421c8d4 100644 --- a/Cslib/Foundations/Logic/Operators/Box.lean +++ b/Cslib/Foundations/Logic/Operators/Box.lean @@ -14,7 +14,7 @@ public import Cslib.Init namespace Cslib.Logic -/-- The type `α` has a box modality (□). -/ +/-- The type `α` has a box modality (`□`). -/ class HasBox (α : Type*) where /-- `a` is valid in all immediately reachable states. -/ box (a : α) : α diff --git a/Cslib/Foundations/Logic/Operators/Diamond.lean b/Cslib/Foundations/Logic/Operators/Diamond.lean index c37416abf..d15741fb5 100644 --- a/Cslib/Foundations/Logic/Operators/Diamond.lean +++ b/Cslib/Foundations/Logic/Operators/Diamond.lean @@ -14,7 +14,7 @@ public import Cslib.Init namespace Cslib.Logic -/-- The type `α` has a diamond modality (◇). -/ +/-- The type `α` has a diamond modality (`◇`). -/ class HasDiamond (α : Type*) where /-- `a` is valid in a reachable state. -/ diamond (a : α) : α diff --git a/Cslib/Foundations/Logic/Operators/Impl.lean b/Cslib/Foundations/Logic/Operators/Impl.lean new file mode 100644 index 000000000..5ef62666e --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Impl.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi, Thomas Waring +-/ + +module + +public import Cslib.Init + +/-! # Impl connective (→) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has an implication connective (`→`). -/ +class HasImpl (α : Type*) where + /-- `a → b` denotes `a` implies `b`. -/ + impl (a b : α) : α + +@[inherit_doc] scoped infixr:25 " → " => HasImpl.impl + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Not.lean b/Cslib/Foundations/Logic/Operators/Not.lean index 40b89eb0f..76489f4a1 100644 --- a/Cslib/Foundations/Logic/Operators/Not.lean +++ b/Cslib/Foundations/Logic/Operators/Not.lean @@ -14,11 +14,11 @@ public import Cslib.Init namespace Cslib.Logic -/-- The type `α` has a negation connective (¬). -/ +/-- The type `α` has a negation connective (`¬`). -/ class HasNot (α : Type*) where /-- `¬a` is the negation of `a`. -/ not (a : α) : α -@[inherit_doc] scoped prefix:40 "¬" => HasNot.not +@[inherit_doc] scoped notation:max "¬" p:40 => HasNot.not p end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Or.lean b/Cslib/Foundations/Logic/Operators/Or.lean new file mode 100644 index 000000000..1f1aadab0 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Or.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi, Thomas Waring +-/ + +module + +public import Cslib.Init + +/-! # Or connective (∨) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has an or connective (`∨`). -/ +class HasOr (α : Type*) where + /-- `a ∨ b` is the disjunction of `a` and `b`. -/ + or (a b : α) : α + +@[inherit_doc] scoped infixr:30 " ∨ " => HasOr.or + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/Tensor.lean b/Cslib/Foundations/Logic/Operators/Tensor.lean index 69cf13b15..45f66174c 100644 --- a/Cslib/Foundations/Logic/Operators/Tensor.lean +++ b/Cslib/Foundations/Logic/Operators/Tensor.lean @@ -19,6 +19,6 @@ class HasTensor (α : Type*) where /-- `a ⊗ b` is the multiplicative conjunction of `a` and `b`. -/ tensor (a b : α) : α -@[inherit_doc] scoped infix:35 " ⊗ " => HasTensor.tensor +@[inherit_doc] scoped infixr:35 " ⊗ " => HasTensor.tensor end Cslib.Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index a62792367..1a9d1c86a 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -6,7 +6,12 @@ Authors: Fabrizio Montesi, Marianna Girlando module -public import Cslib.Init +public import Cslib.Foundations.Logic.Operators.And +public import Cslib.Foundations.Logic.Operators.Or +public import Cslib.Foundations.Logic.Operators.Impl +public import Cslib.Foundations.Logic.Operators.Not +public import Cslib.Foundations.Logic.Operators.Box +public import Cslib.Foundations.Logic.Operators.Diamond public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.Set.Basic public import Mathlib.Order.Defs.Unbundled @@ -47,19 +52,38 @@ inductive Proposition (Atom : Type u) : Type u where /-- Possibility. -/ | diamond (φ : Proposition Atom) -@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg -@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and +-- scoped notation:max "¬" p:40 => Proposition.neg p +instance : HasNot (Proposition Atom) := {not := Proposition.neg} +-- scoped infixr:35 " ∧ " => Proposition.and +instance : HasAnd (Proposition Atom) := {and := Proposition.and} @[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond +-- instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} + +@[simp, grind =] +lemma Proposition.neg_def (φ : Proposition Atom) : φ.neg = ¬φ := rfl + +@[simp, grind =] +lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl + +@[simp, grind =] +lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl /-- Disjunction. -/ def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) -@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or +-- scoped infixr:30 " ∨ " => Proposition.or +instance : HasOr (Proposition Atom) := {or := Proposition.or} + +@[grind =] +lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∨ φ₂) = ¬(¬φ₁ ∧ ¬φ₂) := rfl /-- Implication. -/ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ -@[inherit_doc] scoped infix:30 " → " => Proposition.impl +instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} + +@[grind =] +lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = (¬φ₁ ∨ φ₂) := rfl /-- Bi-implication. -/ def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) @@ -107,8 +131,7 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/ @[scoped grind =] -theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by - induction φ generalizing w <;> grind +theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl /-- Characterisation of the `∨` connective. @@ -116,7 +139,9 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or] + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by + simp_rw [HasOr.or, Proposition.or, ←Proposition.neg_def, ←Proposition.and_def] + grind /-- Characterisation of the `→` connective. @@ -125,7 +150,9 @@ This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.impl_iff_impl {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl] + ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by + -- simp_rw [HasImpl.impl, Proposition.impl] + grind /-- Characterisation of the `□` modality. @@ -133,7 +160,9 @@ Necessity is defined in terms of the more primitive connectives given in `Propos This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.box_iff_forall {m : Model World Atom} : - ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box] + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by + simp_rw [Proposition.box, ←Proposition.neg_def] + grind /-- The theory of a world in a model is the set of all propositions that it satifies. -/ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index fa3caf53e..ebbc7df57 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -6,7 +6,10 @@ Authors: Thomas Waring module -public import Cslib.Init +public import Cslib.Foundations.Logic.Operators.And +public import Cslib.Foundations.Logic.Operators.Or +public import Cslib.Foundations.Logic.Operators.Impl +public import Cslib.Foundations.Logic.Operators.Not public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags @@ -30,8 +33,10 @@ theory. ## Notation -We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum, -conjunction, disjunction, implication and negation. +We instantiate the notation classes `HasAnd`, `HasOr`, `HasImpl` and `HasNot` for `Proposition Atom` +to give access to, respectively, the notations `∧, ∨, →` and `¬` for propositional connectives. +In the case that `Atom` has a bottom element (respectively, is inhabited) we give instances +`HasBot (Proposition Atom)` and (respectively, `HasTop (Proposition Atom)`). -/ @[expose] public section @@ -67,10 +72,10 @@ instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl -@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and -@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or -@[inherit_doc] scoped infix:30 " → " => Proposition.impl -@[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg +instance : HasAnd (Proposition Atom) := {and := Proposition.and} +instance : HasOr (Proposition Atom) := {or := Proposition.or} +instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} +instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg} /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic language. -/ From 060954ec8589c8321bf359f44201a91127224744 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 27 May 2026 19:31:06 +0200 Subject: [PATCH 3/6] fix not_def --- Cslib/Logics/Modal/Basic.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 1a9d1c86a..0f6f21b5a 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -55,12 +55,14 @@ inductive Proposition (Atom : Type u) : Type u where -- scoped notation:max "¬" p:40 => Proposition.neg p instance : HasNot (Proposition Atom) := {not := Proposition.neg} -- scoped infixr:35 " ∧ " => Proposition.and +@[scoped grind =] instance : HasAnd (Proposition Atom) := {and := Proposition.and} + @[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond -- instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} -@[simp, grind =] -lemma Proposition.neg_def (φ : Proposition Atom) : φ.neg = ¬φ := rfl +@[simp, scoped grind =] +lemma Proposition.not_def (φ : Proposition Atom) : (¬φ : Proposition Atom) = φ.neg := rfl @[simp, grind =] lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl @@ -140,7 +142,7 @@ This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by - simp_rw [HasOr.or, Proposition.or, ←Proposition.neg_def, ←Proposition.and_def] + simp_rw [HasOr.or, Proposition.or, ←Proposition.and_def] grind /-- Characterisation of the `→` connective. @@ -161,7 +163,7 @@ This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.box_iff_forall {m : Model World Atom} : ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by - simp_rw [Proposition.box, ←Proposition.neg_def] + simp_rw [Proposition.box] grind /-- The theory of a world in a model is the set of all propositions that it satifies. -/ From 2f4b4c9e5a4b48f6a4018d6c11a46485671d89af Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 28 May 2026 12:15:26 +0200 Subject: [PATCH 4/6] fix modal connectives --- Cslib/Foundations/Logic/Operators/Iff.lean | 24 ++++++++++ Cslib/Logics/Modal/Basic.lean | 52 +++++++++------------- 2 files changed, 46 insertions(+), 30 deletions(-) create mode 100644 Cslib/Foundations/Logic/Operators/Iff.lean diff --git a/Cslib/Foundations/Logic/Operators/Iff.lean b/Cslib/Foundations/Logic/Operators/Iff.lean new file mode 100644 index 000000000..7617b9e35 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators/Iff.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi, Thomas Waring +-/ + +module + +public import Cslib.Init + +/-! # Iff connective (↔) -/ + +@[expose] public section + +namespace Cslib.Logic + +/-- The type `α` has a bi-implication connective (`↔`). -/ +class HasIff (α : Type*) where + /-- `a ↔ b` denotes `a` implies `b` and vice-versa. -/ + iff (a b : α) : α + +@[inherit_doc] scoped infixr:20 " ↔ " => HasIff.iff + +end Cslib.Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 0f6f21b5a..8aec61a43 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -12,6 +12,7 @@ public import Cslib.Foundations.Logic.Operators.Impl public import Cslib.Foundations.Logic.Operators.Not public import Cslib.Foundations.Logic.Operators.Box public import Cslib.Foundations.Logic.Operators.Diamond +public import Cslib.Foundations.Logic.Operators.Iff public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.Set.Basic public import Mathlib.Order.Defs.Unbundled @@ -52,31 +53,25 @@ inductive Proposition (Atom : Type u) : Type u where /-- Possibility. -/ | diamond (φ : Proposition Atom) --- scoped notation:max "¬" p:40 => Proposition.neg p instance : HasNot (Proposition Atom) := {not := Proposition.neg} --- scoped infixr:35 " ∧ " => Proposition.and -@[scoped grind =] instance : HasAnd (Proposition Atom) := {and := Proposition.and} - -@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond --- instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} +instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} @[simp, scoped grind =] -lemma Proposition.not_def (φ : Proposition Atom) : (¬φ : Proposition Atom) = φ.neg := rfl +lemma Proposition.not_def (φ : Proposition Atom) : (¬φ) = φ.neg := rfl -@[simp, grind =] -lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl +@[simp, scoped grind =] +lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∧ φ₂) = φ₁.and φ₂:= rfl -@[simp, grind =] -lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl +@[simp, scoped grind =] +lemma Proposition.diamond_def (φ : Proposition Atom) : (◇φ) = φ.diamond := rfl /-- Disjunction. -/ def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) --- scoped infixr:30 " ∨ " => Proposition.or instance : HasOr (Proposition Atom) := {or := Proposition.or} -@[grind =] +@[scoped grind =] lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∨ φ₂) = ¬(¬φ₁ ∧ ¬φ₂) := rfl /-- Implication. -/ @@ -84,18 +79,25 @@ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} -@[grind =] +@[scoped grind =] lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = (¬φ₁ ∨ φ₂) := rfl /-- Bi-implication. -/ def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff +instance : HasIff (Proposition Atom) := {iff := Proposition.iff} + +@[scoped grind =] +lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) : + (φ₁ ↔ φ₂) = ((φ₁ → φ₂) ∧ (φ₂ → φ₁)) := rfl /-- Necessity. -/ def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ -@[inherit_doc] scoped prefix:40 "□" => Proposition.box +instance : HasBox (Proposition Atom) := {box := Proposition.box} + +@[scoped grind =] +lemma Proposition.box_def (φ : Proposition Atom) : (□φ) = ¬◇¬φ := rfl /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies the proposition `φ`. -/ @@ -141,9 +143,7 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by - simp_rw [HasOr.or, Proposition.or, ←Proposition.and_def] - grind + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind /-- Characterisation of the `→` connective. @@ -152,9 +152,7 @@ This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.impl_iff_impl {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by - -- simp_rw [HasImpl.impl, Proposition.impl] - grind + ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind /-- Characterisation of the `□` modality. @@ -162,9 +160,7 @@ Necessity is defined in terms of the more primitive connectives given in `Propos This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.box_iff_forall {m : Model World Atom} : - ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by - simp_rw [Proposition.box] - grind + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind /-- The theory of a world in a model is the set of all propositions that it satifies. -/ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := @@ -195,13 +191,9 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂) /-- The K axiom, valid for all models. -/ theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind -set_option linter.tacticAnalysis.verifyGrindOnly false in /-- The dual axiom, valid for all models. -/ theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by - constructor - · grind - · grind only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def, - = neg_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true] + constructor <;> grind /-- The T axiom, valid for all reflexive models. -/ theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World} From d4410e34f16cd012c26358bfa258901bfd350c81 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 29 May 2026 09:01:17 +0200 Subject: [PATCH 5/6] indirection in _def lemmas --- Cslib/Logics/Modal/Basic.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 8aec61a43..d4ba2e5e1 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -72,7 +72,7 @@ def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬ instance : HasOr (Proposition Atom) := {or := Proposition.or} @[scoped grind =] -lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∨ φ₂) = ¬(¬φ₁ ∧ ¬φ₂) := rfl +lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∨ φ₂) = φ₁.or φ₂ := rfl /-- Implication. -/ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ @@ -80,7 +80,7 @@ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} @[scoped grind =] -lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = (¬φ₁ ∨ φ₂) := rfl +lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = φ₁.impl φ₂ := rfl /-- Bi-implication. -/ def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) @@ -89,7 +89,7 @@ instance : HasIff (Proposition Atom) := {iff := Proposition.iff} @[scoped grind =] lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) : - (φ₁ ↔ φ₂) = ((φ₁ → φ₂) ∧ (φ₂ → φ₁)) := rfl + (φ₁ ↔ φ₂) = φ₁.iff φ₂ := rfl /-- Necessity. -/ def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ @@ -97,7 +97,7 @@ def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ instance : HasBox (Proposition Atom) := {box := Proposition.box} @[scoped grind =] -lemma Proposition.box_def (φ : Proposition Atom) : (□φ) = ¬◇¬φ := rfl +lemma Proposition.box_def (φ : Proposition Atom) : (□φ) = φ.box := rfl /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies the proposition `φ`. -/ @@ -143,7 +143,7 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or] /-- Characterisation of the `→` connective. @@ -152,7 +152,7 @@ This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.impl_iff_impl {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind + ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl] /-- Characterisation of the `□` modality. @@ -160,7 +160,7 @@ Necessity is defined in terms of the more primitive connectives given in `Propos This result proves that the definition is correct. -/ @[scoped grind =] theorem Satisfies.box_iff_forall {m : Model World Atom} : - ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box] /-- The theory of a world in a model is the set of all propositions that it satifies. -/ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := From 63918a2c1ac8d103ce7f86cbe65adaf1f5e7e2bf Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 29 May 2026 15:04:22 +0200 Subject: [PATCH 6/6] update cslib.lean --- Cslib.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Cslib.lean b/Cslib.lean index 9a780df9a..d56972af2 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -71,7 +71,10 @@ public import Cslib.Foundations.Logic.LogicalEquivalence public import Cslib.Foundations.Logic.Operators.And public import Cslib.Foundations.Logic.Operators.Box public import Cslib.Foundations.Logic.Operators.Diamond +public import Cslib.Foundations.Logic.Operators.Iff +public import Cslib.Foundations.Logic.Operators.Impl public import Cslib.Foundations.Logic.Operators.Not +public import Cslib.Foundations.Logic.Operators.Or public import Cslib.Foundations.Logic.Operators.Tensor public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS