diff --git a/Cslib.lean b/Cslib.lean index 070e6dc0f..d56972af2 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -68,6 +68,14 @@ 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.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 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..f562e919c --- /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 infixr:36 " ∧ " => 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..19421c8d4 --- /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..d15741fb5 --- /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/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/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 new file mode 100644 index 000000000..76489f4a1 --- /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 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 new file mode 100644 index 000000000..45f66174c --- /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 infixr:35 " ⊗ " => HasTensor.tensor + +end Cslib.Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index a62792367..d4ba2e5e1 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -6,7 +6,13 @@ 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.Operators.Iff public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.Set.Basic public import Mathlib.Order.Defs.Unbundled @@ -47,29 +53,51 @@ 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 -@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond +instance : HasNot (Proposition Atom) := {not := Proposition.neg} +instance : HasAnd (Proposition Atom) := {and := Proposition.and} +instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} + +@[simp, scoped grind =] +lemma Proposition.not_def (φ : Proposition Atom) : (¬φ) = φ.neg := rfl + +@[simp, scoped grind =] +lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∧ φ₂) = φ₁.and φ₂:= rfl + +@[simp, scoped grind =] +lemma Proposition.diamond_def (φ : Proposition Atom) : (◇φ) = φ.diamond := rfl /-- Disjunction. -/ def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) -@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or +instance : HasOr (Proposition Atom) := {or := Proposition.or} + +@[scoped grind =] +lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∨ φ₂) = φ₁.or φ₂ := rfl /-- Implication. -/ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ -@[inherit_doc] scoped infix:30 " → " => Proposition.impl +instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} + +@[scoped grind =] +lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = φ₁.impl φ₂ := 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) : + (φ₁ ↔ φ₂) = φ₁.iff φ₂ := 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) : (□φ) = φ.box := rfl /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies the proposition `φ`. -/ @@ -107,8 +135,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. @@ -164,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} 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. -/