From 31fb1ca4f13a15184ff7ee49420ccbf13a92e08e Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 21 May 2026 14:48:41 +0200 Subject: [PATCH 01/36] 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 02/36] 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 03/36] 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 04/36] 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 05/36] 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 06/36] 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 From 9669f241a0a580aea6ffc7c5fa6b6d92567491d1 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 16 Jun 2026 08:35:07 +0200 Subject: [PATCH 07/36] merge main again --- Cslib.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Cslib.lean b/Cslib.lean index cba18cd0a..79f1a7f81 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -71,7 +71,6 @@ public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence -<<<<<<< HEAD public import Cslib.Foundations.Logic.Operators.And public import Cslib.Foundations.Logic.Operators.Box public import Cslib.Foundations.Logic.Operators.Diamond @@ -80,13 +79,11 @@ 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.Relation.Attr public import Cslib.Foundations.Relation.Confluence public import Cslib.Foundations.Relation.Defs public import Cslib.Foundations.Relation.Domain public import Cslib.Foundations.Relation.Euclidean ->>>>>>> main public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS From 604ba153b0a098bad1423fd8edef0260fbc76ced Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 16 Jun 2026 08:37:22 +0200 Subject: [PATCH 08/36] fix compilationg --- Cslib/Logics/Modal/Basic.lean | 6 +++--- Cslib/Logics/Modal/Denotation.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index a0d32a8d2..882608481 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -57,13 +57,13 @@ instance : HasNot (Proposition Atom) := {not := Proposition.not} instance : HasAnd (Proposition Atom) := {and := Proposition.and} instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} -@[simp, scoped grind =_] +@[simp, scoped grind =] lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl -@[simp, scoped grind =_] +@[simp, scoped grind =] lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl -@[simp, scoped grind =_] +@[simp, scoped grind =] lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl /-- Disjunction. -/ diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean index b74e8f3f1..4b3415b33 100644 --- a/Cslib/Logics/Modal/Denotation.lean +++ b/Cslib/Logics/Modal/Denotation.lean @@ -18,7 +18,7 @@ A denotational semantics for modal logic, inspired by the one for Hennessy-Milne namespace Cslib.Logic.Modal -open scoped Proposition InferenceSystem +open scoped Proposition InferenceSystem Satisfies /-- Denotation of a proposition. -/ @[simp, scoped grind =] From 20b4a92e0e3779b87b20c89e4c943218dcaefb43 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 16 Jun 2026 08:52:23 +0200 Subject: [PATCH 09/36] fix some proofs --- Cslib/Logics/Modal/Basic.lean | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 882608481..9b29ea294 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) : (φ₁ ∨ φ₂) = φ₁.or φ₂ := 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) : (φ₁ → φ₂) = φ₁.impl φ₂ := 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) : - (φ₁ ↔ φ₂) = φ₁.iff φ₂ := 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) : (□φ) = φ.box := 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 `φ`. -/ @@ -151,7 +151,8 @@ 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 + grind [=_ Proposition.or_def, Proposition.or] /-- Characterisation of the `→` connective. @@ -160,7 +161,8 @@ 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 + grind [=_ Proposition.impl_def, Proposition.impl] /-- Characterisation of the `↔` connective. @@ -178,7 +180,8 @@ 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 + grind [=_ Proposition.box_def, 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 c7e5a4cde259d73f06d6c0aae6993bfd520cd3b0 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 16 Jun 2026 08:54:40 +0200 Subject: [PATCH 10/36] fix simp lints --- Cslib/Logics/Modal/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 9b29ea294..0d08da3d5 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -57,13 +57,13 @@ instance : HasNot (Proposition Atom) := {not := Proposition.not} instance : HasAnd (Proposition Atom) := {and := Proposition.and} instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} -@[simp, scoped grind =] +@[scoped grind =] lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl -@[simp, scoped grind =] +@[scoped grind =] lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl -@[simp, scoped grind =] +@[scoped grind =] lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl /-- Disjunction. -/ From 059a85c1c8a7eef6b8766530ed3716aeb8816e15 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 16 Jun 2026 09:21:41 +0200 Subject: [PATCH 11/36] parametrised logical equivalence --- .../Foundations/Logic/LogicalEquivalence.lean | 23 +++++++++++++++---- Cslib/Logics/LinearLogic/CLL/Basic.lean | 2 +- Cslib/Logics/Modal/LogicalEquivalence.lean | 4 ++-- 3 files changed, 21 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean index 7f6c0d332..f4dbc06d9 100644 --- a/Cslib/Foundations/Logic/LogicalEquivalence.lean +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -8,6 +8,7 @@ module public import Cslib.Foundations.Syntax.Context public import Cslib.Foundations.Syntax.Congruence +public import Cslib.Foundations.Logic.InferenceSystem /-! Typeclass and notation for logical equivalence. -/ @@ -15,21 +16,33 @@ public import Cslib.Foundations.Syntax.Congruence namespace Cslib.Logic +open scoped InferenceSystem + /-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that preserves validity of judgements under any judgemental context. -/ -class LogicalEquivalence +class LogicalEquivalence S (Proposition : Type u) [HasContext Proposition] (Judgement : Type v) [HasHContext Judgement Proposition] - (Valid : Judgement → Sort w) where - /-- The logical equivalence relation. -/ + [InferenceSystem S Judgement] where + /-- `a ≡[S] b` means that `a` and `b` are logically equivalent in the inference system `S`. -/ eqv (a b : Proposition) : Prop /-- Proof that `eqv` is a congruence. -/ [congruence : Congruence Proposition eqv] /-- Validity is preserved for any judgemental context. -/ eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition) - (h : Valid (c<[a])) : Valid (c<[b]) + (h : S⇓(c<[a])) : S⇓(c<[b]) @[inherit_doc] -scoped infix:29 " ≡ " => LogicalEquivalence.eqv +scoped notation a " ≡[" S "]" b => LogicalEquivalence.eqv S a b + +/-- Class for types (`α`) that have a canonical logical equivalence (under a canonical, default +inference system). -/ +abbrev HasLogicalEquivalence (Proposition : Type u) [HasContext Proposition] + (Judgement : Type v) [HasHContext Judgement Proposition] + [HasInferenceSystem Judgement] := + LogicalEquivalence InferenceSystem.Default Proposition Judgement + +/-- `a ≡ b` means that `a` and `b` are logically equivalent. -/ +scoped infix:29 " ≡ " => LogicalEquivalence.eqv InferenceSystem.Default end Cslib.Logic diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c331ae2ae..ce8db29a4 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -650,7 +650,7 @@ instance : Congruence (Proposition Atom) Proposition.Equiv where intro ctx a b hab induction ctx <;> grind [= Context.fill] -noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where +noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where eqv := Proposition.Equiv eqvFillValid {a b : Proposition Atom} (heqv : a.Equiv b) (c : HasHContext.Context (Sequent Atom) (Proposition Atom)) diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index 0fc089e4e..0f34ad0e5 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -122,8 +122,8 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} : open scoped Satisfies.Context /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/ -instance : LogicalEquivalence - (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where +instance : HasLogicalEquivalence + (Proposition Atom) (Judgement World Atom) where eqv := Proposition.Equiv Set.univ eqvFillValid heqv c h := by specialize heqv c.m From c2ec296219b83747d45f77f67cd496d79d477835 Mon Sep 17 00:00:00 2001 From: twwar Date: Tue, 16 Jun 2026 09:32:42 +0200 Subject: [PATCH 12/36] grind annotation for not --- Cslib/Logics/Propositional/Defs.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index a44a3ea86..d76539323 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -78,6 +78,10 @@ instance : HasOr (Proposition Atom) := {or := Proposition.or} instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg} +omit [DecidableEq Atom] in +@[grind =] +lemma not_eq [Bot Atom] (A : Proposition Atom) : (A → ⊥) = ¬ A := rfl + /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic language. -/ def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') : From 5c43f8e71a62dc92b9bb8e25e093eebb45584a03 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Jul 2026 15:15:39 +0200 Subject: [PATCH 13/36] refactor operators into a single file with sections --- Cslib.lean | 9 +- Cslib/Foundations/Logic/Operators.lean | 96 +++++++++++++++++++ Cslib/Foundations/Logic/Operators/And.lean | 24 ----- Cslib/Foundations/Logic/Operators/Box.lean | 24 ----- .../Foundations/Logic/Operators/Diamond.lean | 24 ----- Cslib/Foundations/Logic/Operators/Iff.lean | 24 ----- Cslib/Foundations/Logic/Operators/Impl.lean | 24 ----- Cslib/Foundations/Logic/Operators/Not.lean | 24 ----- Cslib/Foundations/Logic/Operators/Or.lean | 24 ----- Cslib/Foundations/Logic/Operators/Tensor.lean | 24 ----- Cslib/Logics/HML/LogicalEquivalence.lean | 4 +- Cslib/Logics/Modal/Basic.lean | 22 ++--- Cslib/Logics/Propositional/Defs.lean | 17 ++-- 13 files changed, 114 insertions(+), 226 deletions(-) create mode 100644 Cslib/Foundations/Logic/Operators.lean delete mode 100644 Cslib/Foundations/Logic/Operators/And.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Box.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Diamond.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Iff.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Impl.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Not.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Or.lean delete mode 100644 Cslib/Foundations/Logic/Operators/Tensor.lean diff --git a/Cslib.lean b/Cslib.lean index 6bd3497ce..4f558680b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -77,14 +77,7 @@ 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.Logic.Operators public import Cslib.Foundations.Relation.Attr public import Cslib.Foundations.Relation.Confluence public import Cslib.Foundations.Relation.Defs diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean new file mode 100644 index 000000000..9d8c38656 --- /dev/null +++ b/Cslib/Foundations/Logic/Operators.lean @@ -0,0 +1,96 @@ +/- +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 + +/-! # Logical operators + +This module contains typeclasses and associated notation for common logical operators: propositional +connectives (like `∧` and `→`), modalities (like `◇`, plain and indexed), linear connectives (like +`⊗`), etc. +-/ + +@[expose] public section + +namespace Cslib.Logic + +section Propositional + +-- ## Propositional connectives + +/-- 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 + +/-- 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 + +/-- The type `α` has an implication connective (`→`). -/ +class HasImp (α : Type*) where + /-- `a → b` denotes `a` implies `b`. -/ + imp (a b : α) : α + +@[inherit_doc] scoped infixr:25 " → " => HasImp.imp + +/-- 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 + +/-- 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 Propositional + +section Modal + +-- ## Modalities + +/-- 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 + +/-- 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 Modal + +section Linear + +-- ## Linear connectives + +/-- 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 Linear + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Operators/And.lean b/Cslib/Foundations/Logic/Operators/And.lean deleted file mode 100644 index f562e919c..000000000 --- a/Cslib/Foundations/Logic/Operators/And.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 19421c8d4..000000000 --- a/Cslib/Foundations/Logic/Operators/Box.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index d15741fb5..000000000 --- a/Cslib/Foundations/Logic/Operators/Diamond.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 7617b9e35..000000000 --- a/Cslib/Foundations/Logic/Operators/Iff.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 5ef62666e..000000000 --- a/Cslib/Foundations/Logic/Operators/Impl.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 76489f4a1..000000000 --- a/Cslib/Foundations/Logic/Operators/Not.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 1f1aadab0..000000000 --- a/Cslib/Foundations/Logic/Operators/Or.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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 deleted file mode 100644 index 45f66174c..000000000 --- a/Cslib/Foundations/Logic/Operators/Tensor.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -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/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 5bad96e46..65a43cbe3 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -102,8 +102,8 @@ instance judgementalContext : HasHContext (Satisfies.Judgement State Label) (Proposition Label) := ⟨Satisfies.Context State Label, Satisfies.Context.fill⟩ -instance : LogicalEquivalence - (Proposition Label) (Satisfies.Judgement State Label) (Satisfies.Bundled) where +instance : HasLogicalEquivalence + (Proposition Label) (Satisfies.Judgement State Label) where eqv := Proposition.Equiv eqvFillValid {a b : Proposition Label} (heqv : a.Equiv (State := State) b) (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label)) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 0d08da3d5..cefa5bece 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -6,13 +6,7 @@ Authors: Fabrizio Montesi, Marianna Girlando module -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.Operators public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.Set.Basic public import Mathlib.Order.Defs.Unbundled @@ -75,12 +69,12 @@ instance : HasOr (Proposition Atom) := {or := Proposition.or} lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl /-- Implication. -/ -def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ +def Proposition.imp (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ -instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} +instance : HasImp (Proposition Atom) := {imp := Proposition.imp} @[scoped grind =] -lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : φ₁.impl φ₂ = (φ₁ → φ₂) := rfl +lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl /-- Bi-implication. -/ def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) @@ -160,9 +154,9 @@ Implication is defined in terms of the more primitive connectives given in `Prop This result proves that the definition is correct. -/ @[scoped grind =] -theorem Satisfies.impl_iff_impl {m : Model World Atom} : +theorem Satisfies.imp_iff_imp {m : Model World Atom} : ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by - grind [=_ Proposition.impl_def, Proposition.impl] + grind [=_ Proposition.imp_def, Proposition.imp] /-- Characterisation of the `↔` connective. @@ -251,13 +245,13 @@ theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty A have a := Classical.arbitrary Atom let v₁ := fun (w' : World) (a : Atom) => w' = w₁ let h₁ := h (v := v₁) (w := w₁) (φ := .atom a) - simp [impl_iff_impl] at h₁ + simp [imp_iff_imp] at h₁ grind /-- The 4 axiom, valid for all transitive models. -/ theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World} (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by - simp only [impl_iff_impl] + simp only [imp_iff_imp] intro h rcases h with ⟨w', h₁, w'', h₂, hs⟩ exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩ diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index d76539323..cea4c2362 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -6,10 +6,7 @@ Authors: Thomas Waring module -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 public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.Set.Image @@ -57,25 +54,25 @@ inductive Proposition (Atom : Type u) : Type u where /-- Disjunction -/ | or (a b : Proposition Atom) /-- Implication -/ - | impl (a b : Proposition Atom) + | imp (a b : Proposition Atom) deriving DecidableEq, BEq instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩ instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩ /-- We view negation as a defined connective ~A := A → ⊥ -/ -abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥) +abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.imp · ⊥) /-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ -abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default) +abbrev Proposition.top [Inhabited Atom] : Proposition Atom := imp (.atom default) (.atom default) instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩ -example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl +example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.imp ⊥ ⊥ := rfl instance : HasAnd (Proposition Atom) := {and := Proposition.and} instance : HasOr (Proposition Atom) := {or := Proposition.or} -instance : HasImpl (Proposition Atom) := {impl := Proposition.impl} +instance : HasImp (Proposition Atom) := {imp := Proposition.imp} instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg} omit [DecidableEq Atom] in @@ -89,7 +86,7 @@ def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') : | atom x => f x | and A B => (A.subst f) ∧ (B.subst f) | or A B => (A.subst f) ∨ (B.subst f) - | impl A B => (A.subst f) → (B.subst f) + | imp A B => (A.subst f) → (B.subst f) -- This is probably a lawful monad, but that doesn't seem to be important. instance : Monad Proposition where From 77ce0c743efef2efafc56979040ba3aa86274200 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 7 Jul 2026 14:06:32 +0200 Subject: [PATCH 14/36] fix HML --- Cslib/Logics/HML/LogicalEquivalence.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 65a43cbe3..2e0c8005a 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -81,6 +81,8 @@ structure Satisfies.Judgement (State : Type u) (Label : Type v) where /-- `Satisfies` variant using bundled judgements. -/ def Satisfies.Bundled (j : Satisfies.Judgement State Label) := Satisfies j.lts j.state j.φ +instance : HasInferenceSystem (Satisfies.Judgement World Atom) := ⟨Satisfies.Bundled⟩ + @[scoped grind =] theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl From 842646e7d72743e64c2da37bbfdc5b10809982c8 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 7 Jul 2026 14:08:35 +0200 Subject: [PATCH 15/36] doc headers --- Cslib/Foundations/Logic/Operators.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index 9d8c38656..9e51d447f 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -21,7 +21,7 @@ namespace Cslib.Logic section Propositional --- ## Propositional connectives +/-! ## Propositional connectives -/ /-- The type `α` has an and connective (`∧`). -/ class HasAnd (α : Type*) where @@ -62,7 +62,7 @@ end Propositional section Modal --- ## Modalities +/-! ## Modalities -/ /-- The type `α` has a box modality (`□`). -/ class HasBox (α : Type*) where @@ -82,7 +82,7 @@ end Modal section Linear --- ## Linear connectives +/-! ## Linear connectives -/ /-- The type `α` has a tensor connective (⊗). -/ class HasTensor (α : Type*) where From 0708becef48018093b2c7f66a957ee573d2cc6af Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 7 Jul 2026 14:40:21 +0200 Subject: [PATCH 16/36] dynamic logic modalities --- Cslib/Foundations/Logic/Operators.lean | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index 9e51d447f..a825155b2 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -62,7 +62,7 @@ end Propositional section Modal -/-! ## Modalities -/ +/-! ## Basic modalities -/ /-- The type `α` has a box modality (`□`). -/ class HasBox (α : Type*) where @@ -80,6 +80,26 @@ class HasDiamond (α : Type*) where end Modal +section Dynamic + +/-! ## Dynamic modalities -/ + +/-- The type `α` has a dynamic box modality with action type `β` (`[a]φ`). -/ +class HasDynamicBox (α β : Type*) where + /-- `b` is necessarily valid after `a`. -/ + dynBox (a : β) (b : α) : α + +@[inherit_doc] scoped notation "[" a "]" φ => HasDynamicBox.dynBox a φ + +/-- The type `α` has a dynamic diamond modality with action type `β` (`[a]φ`). -/ +class HasDynamicDiamond (α β : Type*) where + /-- `b` is possibly valid after `a`. -/ + dynDiamond (a : β) (b : α) : α + +@[inherit_doc] scoped notation "⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ + +end Dynamic + section Linear /-! ## Linear connectives -/ From 0c0cdabd7da67b9c4cd802c6014c5d299abde056 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 7 Jul 2026 14:52:36 +0200 Subject: [PATCH 17/36] comment out notation for dynamic logic --- Cslib/Foundations/Logic/Operators.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index a825155b2..ab6a463b7 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -80,6 +80,7 @@ class HasDiamond (α : Type*) where end Modal +/- section Dynamic /-! ## Dynamic modalities -/ @@ -99,6 +100,7 @@ class HasDynamicDiamond (α β : Type*) where @[inherit_doc] scoped notation "⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ end Dynamic +-/ section Linear From ddc2c9b8b0b7848948eefe00002323d02440c2e3 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 8 Jul 2026 13:18:48 +0200 Subject: [PATCH 18/36] dynlogic operators fix --- Cslib/Foundations/Logic/Operators.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index ab6a463b7..6ae461927 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -80,27 +80,29 @@ class HasDiamond (α : Type*) where end Modal -/- section Dynamic -/-! ## Dynamic modalities -/ +/-! ## Dynamic modalities + +Here we need to use the prefix `d` to distinguish our notation from the normal `[·]` and `⟨·⟩`. +A refactoring that makes this unnecessary would be welcome. +-/ /-- The type `α` has a dynamic box modality with action type `β` (`[a]φ`). -/ class HasDynamicBox (α β : Type*) where /-- `b` is necessarily valid after `a`. -/ dynBox (a : β) (b : α) : α -@[inherit_doc] scoped notation "[" a "]" φ => HasDynamicBox.dynBox a φ +@[inherit_doc] scoped notation "d[" a "]" φ => HasDynamicBox.dynBox a φ /-- The type `α` has a dynamic diamond modality with action type `β` (`[a]φ`). -/ class HasDynamicDiamond (α β : Type*) where /-- `b` is possibly valid after `a`. -/ dynDiamond (a : β) (b : α) : α -@[inherit_doc] scoped notation "⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ +@[inherit_doc] scoped notation "d⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ end Dynamic --/ section Linear From dd9457f75a219d7620044ea052fe774a812370d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?= Date: Wed, 8 Jul 2026 22:05:04 -0600 Subject: [PATCH 19/36] feat(untyped): standardization theorem for the lambda calculus (#679) This PR proves the standardization theorem: if `M` beta-reduces to `N` in any number of steps, then `N` is reachable from `M` by a standard reduction. Builds on #671. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson --- .../LocallyNameless/Untyped/CallByName.lean | 44 ++++- .../Untyped/StandardReduction.lean | 163 +++++++++++++++++- 2 files changed, 202 insertions(+), 5 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean index 7250ae7bb..a2be62e5a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean @@ -31,18 +31,56 @@ inductive CBN : Term Var → Term Var → Prop /-- Evaluates the leftmost term. -/ | app : LC Z → CBN M N → CBN (app M Z) (app N Z) -variable {M N : Term Var} +variable {M M' N N' : Term Var} -/-- The left side of a CBN reduction step is locally closed. -/ +/-- The left side of a Call-by-Name step is locally closed. -/ lemma CBN.lc_l (step : M ⭢ₙ N) : LC M := by induction step with grind +/-- A single Call-by-Name step is a full β-reduction. -/ +lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by + induction step with + | base h => exact .single (.base h) + | app lc_Z _ ih => exact FullBeta.redex_app_l_cong ih lc_Z + +/-- Call-by-Name reduction is contained in full β-reduction. -/ +lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by + induction step + · rfl + · grind [CBN.step_to_redex, Relation.ReflTransGen.trans] + +/-- Left congruence rule for application in Call-by-Name reduction. -/ +lemma CBN.steps_app_l_cong (step : M ↠ₙ M') (lc_N : LC N) : Term.app M N ↠ₙ Term.app M' N := by + induction step + · rfl + · grind [CBN.app] + variable [HasFresh Var] [DecidableEq Var] -/-- The right side of a CBN reduction step is locally closed. -/ +/-- The right side of a Call-by-Name step is locally closed. -/ lemma CBN.lc_r (step : M ⭢ₙ N) : LC N := by induction step with grind +/-- The right side of a Call-by-Name reduction is locally closed. -/ +lemma CBN.steps_lc_r (lc_M : LC M) (step : M ↠ₙ N) : LC N := by + induction step + · exact lc_M + · grind [CBN.lc_r] + +/-- Substitution preserves a single Call-by-Name step. -/ +lemma CBN.step_subst (x : Var) (h : M ⭢ₙ M') (lc_N : LC N) : + M[x := N] ⭢ₙ M'[x := N] := by + induction h + · grind [Term.subst_open, CBN.base] + · grind [CBN.app] + +/-- Substitution preserves Call-by-Name reduction. -/ +lemma CBN.steps_subst (x : Var) (step : M ↠ₙ M') (lc_N : LC N) : + M[x := N] ↠ₙ M'[x := N] := by + induction step + · rfl + · grind [CBN.step_subst] + end LambdaCalculus.LocallyNameless.Untyped.Term end Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean index 74d253b5c..e9cfe09ec 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean @@ -8,7 +8,7 @@ module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName -/-! # Standard Reduction +/-! # Standard Reduction and the Standardization Theorem ## Reference @@ -18,6 +18,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName @[expose] public section +set_option linter.unusedDecidableInType false + namespace Cslib universe u @@ -39,7 +41,7 @@ inductive Standard : Term Var → Term Var → Prop /-- Standard reduction of a head redex. -/ | rdx : LC m → LC n → m ↠ₙ (abs m') → Standard (m' ^ n) p → Standard (app m n) p -variable {M N : Term Var} +variable {M N P M' N' : Term Var} /-- The left side of a standard reduction is locally closed. -/ lemma Standard.lc_l (step : M ⭢ₛ N) : LC M := by @@ -58,6 +60,163 @@ lemma Standard.lc_r (step : M ⭢ₛ N) : LC N := by case abs xs _ ih => exact LC.abs xs _ ih all_goals grind +/-- A single Call-by-Name step is a standard reduction. -/ +lemma Standard.of_cbn_step (step : M ⭢ₙ N) (lc_N : LC N) : M ⭢ₛ N := by + induction step + case base h_beta => + cases h_beta + exact rdx (by assumption) (by assumption) .refl (lc_refl _ lc_N) + case app L _ _ lc_L _ ih => + cases lc_N + exact app (ih (by assumption)) (lc_refl L lc_L) + +/-- A Call-by-Name step followed by a standard reduction is a standard reduction. -/ +lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ N := by + induction step generalizing N + case base h_beta => + cases h_beta + exact rdx (by assumption) (by assumption) .refl std + case app step_M ih => + cases std with + | app std_L' std_M => exact app (ih std_L') std_M + | rdx _ lc_Z cbn_m std_body => exact rdx step_M.lc_l lc_Z (.head step_M cbn_m) std_body + +/-- A Call-by-Name reduction followed by a standard reduction is a standard reduction. -/ +lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by + induction h1 with + | refl => exact h2 + | tail _ h_step ih => exact ih (cbn_step_trans h_step h2) + +/-- Call-by-Name reduction is contained in standard reduction. -/ +lemma Standard.of_cbn (step : M ↠ₙ N) (lc_N : LC N) : M ⭢ₛ N := + cbn_trans step (lc_refl N lc_N) + +variable [DecidableEq Var] [HasFresh Var] + +/-- Standard reduction is preserved by substitution. -/ +lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC N) (lc_N' : LC N') : + (M[x := N]) ⭢ₛ (M'[x := N']) := by + induction hM generalizing N N' + case fvar => + simp only [Term.subst_fvar] + split + · exact hN + · exact fvar _ + case app ihL ihM => exact app (ihL hN lc_N lc_N') (ihM hN lc_N lc_N') + case abs m m' _ _ ih => + apply abs <| free_union [fv] Var + grind + case rdx n m' _ lc_m lc_n cbn_m std_p ih => + rw [Term.subst_app] + have std_p_subst := ih hN lc_N lc_N' + rw [Term.subst_open x N n m' lc_N] at std_p_subst + exact rdx (subst_lc lc_m lc_N) (subst_lc lc_n lc_N) (CBN.steps_subst x cbn_m lc_N) std_p_subst + +/-- A single full β-step is a standard reduction. -/ +lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N := by + induction step + case base h_beta => grind [rdx, lc_refl] + case appL Z A B lc_Z _ ih => + cases lc_M + exact app (lc_refl Z lc_Z) (ih (by assumption)) + case appR Z A B lc_Z _ ih => + cases lc_M + exact app (ih (by assumption)) (lc_refl Z lc_Z) + case abs ih => + apply abs <| free_union [fv] Var + intro x hx + exact ih x (by grind) (Term.beta_lc lc_M (by constructor)) + +open FullBeta in +/-- Standard reduction is contained in full β-reduction. -/ +lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by + induction step + case fvar => rfl + case app step_L step_M ih_L ih_M => + exact .trans (redex_app_l_cong ih_L step_M.lc_l) (redex_app_r_cong ih_M step_L.lc_r) + case abs xs _ ih => exact FullBeta.redex_abs_cong xs ih + case rdx n m' _ lc_m lc_n cbn_m std_p ih => + have step1 := redex_app_l_cong (CBN.to_redex cbn_m) lc_n + have step2 : m'.abs.app n ↠βᶠ m' ^ n := .single (.base (.beta (CBN.steps_lc_r lc_m cbn_m) lc_n)) + exact .trans step1 (.trans step2 ih) + +/-- If a standard reduction reaches an abstraction, then its leading Call-by-Name + reduction reaches an abstraction that standardly reduces to the same target. -/ +lemma Standard.abs_inv (h : M ⭢ₛ N) (M' : Term Var) (eq : N = Term.abs M') : + ∃ M'', M ↠ₙ Term.abs M'' ∧ Term.abs M'' ⭢ₛ Term.abs M' := by + induction h generalizing M' + case fvar => trivial + case app => trivial + case abs m_body m_target xs h_body ih => + cases eq + exact ⟨m_body, .refl, .abs xs h_body⟩ + case rdx m1 n1 m1' p1 lc_m1 lc_n1 cbn_m1 _ ih => + have ⟨p'', cbn_body, std_p''⟩ := ih M' eq + have step1 : m1.app n1 ↠ₙ m1'.abs.app n1 := CBN.steps_app_l_cong cbn_m1 lc_n1 + have step2 : m1'.abs.app n1 ⭢ₙ m1' ^ n1 := .base (.beta (CBN.steps_lc_r lc_m1 cbn_m1) lc_n1) + exact ⟨p'', .trans step1 (.head step2 cbn_body), std_p''⟩ + +/-- Standard reduction of abstractions is preserved by opening. -/ +lemma Standard.abs_subst + (h_abs : Term.abs M ⭢ₛ Term.abs M') (hN : N ⭢ₛ N') (lc_N : LC N) (lc_N' : LC N') : + (M ^ N) ⭢ₛ (M' ^ N') := by + cases h_abs + case abs h_body => + have ⟨y, _⟩ := fresh_exists <| free_union [fv] Var + have := subst (h_body y (by grind)) hN y lc_N lc_N' + grind + +/-- A standard reduction followed by a full β-step is a standard reduction. -/ +lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by + induction h1 generalizing N + case fvar => contradiction + case rdx lc_L lc_M cbn _ ih => exact .rdx lc_L lc_M cbn (ih h2) + case abs p_body ih => + cases h2 + · grind + · apply abs <| free_union [fv] Var + grind + case app L' _ M _ std_L std_M ih_L ih_M => + cases h2 + case appL step_M => exact .app std_L (ih_M step_M) + case appR step_L _ => exact .app (ih_L step_L) std_M + case base h_beta => + cases h_beta + have ⟨L, cbn_L1, std_abs⟩ := abs_inv std_L _ rfl + have std_subst := std_abs.abs_subst std_M std_M.lc_l std_M.lc_r + have s1 : L'.app M ↠ₙ L.abs.app M := CBN.steps_app_l_cong cbn_L1 std_M.lc_l + have s2 : L.abs.app M ⭢ₙ L ^ M := .base (.beta (CBN.steps_lc_r std_L.lc_l cbn_L1) std_M.lc_l) + exact Standard.cbn_trans (.trans s1 (.single s2)) std_subst + +/-- A standard reduction followed by a full β-reduction is a standard reduction. -/ +lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N := by + induction h2 with + | refl => exact h1 + | tail _ step ih => exact trans_step ih step + +/-- Standard reduction is transitive. -/ +lemma Standard.trans (h1 : M ⭢ₛ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := + trans_redex h1 (to_redex h2) + +instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢βᶠ ·) (· ⭢ₛ ·) where + trans := Standard.trans_step + +instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ↠βᶠ ·) (· ⭢ₛ ·) where + trans := Standard.trans_redex + +instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢ₛ ·) (· ⭢ₛ ·) where + trans := Standard.trans + +/-- The standardization theorem: every full β-reduction is a standard reduction. -/ +theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ N := by + induction step with + | refl => exact lc_refl M lc_M + | tail _ h_step ih => exact ih.trans (of_beta_step h_step h_step.step_lc_l) + +/-- Standard reduction coincides with full β-reduction on locally closed terms. -/ +theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N := + ⟨to_redex, standardization lc_M⟩ + end LambdaCalculus.LocallyNameless.Untyped.Term end Cslib From 6d1e6398ca4554c9d77d0093e0e835a7191a5867 Mon Sep 17 00:00:00 2001 From: lyj Date: Thu, 9 Jul 2026 12:35:16 +0800 Subject: [PATCH 20/36] feat(LocallyNameless/Untyped): new theorem `lcAt_le` (#699) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If a term is locally closed at level `i` and `i ≤ j`, then it is also locally closed at level `j`. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- .../Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean index 72fce4895..539e92ff8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean @@ -125,4 +125,7 @@ lemma lcAt_openRec_above_lcAt (M N : Term Var) (i j : ℕ) (h : i ≤ j) (lc : L M⟦j ↝ N⟧ = M := by induction M generalizing i j <;> grind +lemma lcAt_le (M : Term Var) (i j : ℕ) (h : i ≤ j) (lc : LcAt i M) : LcAt j M := by + induction M generalizing i j <;> grind + end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term From 8db75361baf6086e1cc5f9ddd3be5a4a87258f06 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Sat, 11 Jul 2026 19:56:37 +0200 Subject: [PATCH 21/36] chore: update bench suite (#707) This PR refactors the cslib bench suite so it closely resembles mathlib's again, following leanprover-community/mathlib4#41587. --- scripts/bench/README.md | 17 +- scripts/bench/build/README.md | 13 +- scripts/bench/build/fake-root/bin/lean | 52 ++-- scripts/bench/build/lakeprof_measurements.py | 84 ++++++ scripts/bench/build/lakeprof_report_upload.py | 44 ++-- scripts/bench/build/run | 20 +- scripts/bench/combine.py | 83 ++++-- scripts/bench/measure.py | 248 ++++++++++++------ scripts/bench/repeatedly.py | 172 ++++++++++++ scripts/bench/run | 8 +- scripts/bench/size/run | 58 ++-- 11 files changed, 611 insertions(+), 188 deletions(-) create mode 100755 scripts/bench/build/lakeprof_measurements.py create mode 100755 scripts/bench/repeatedly.py diff --git a/scripts/bench/README.md b/scripts/bench/README.md index 2eca796a4..12285bbd0 100644 --- a/scripts/bench/README.md +++ b/scripts/bench/README.md @@ -5,13 +5,13 @@ It is built around [radar](github.com/leanprover/radar) and benchmark results can be viewed on the [Lean FRO radar instance](https://radar.lean-lang.org/repos/cslib). -To execute the entire suite, run `scripts/bench/run` in the repo root. -To execute an individual benchmark, run `scripts/bench//run` in the repo root. -All scripts output their measurements into the file `measurements.jsonl`. +To execute the benchmark suite, run `scripts/bench/run` from the repo root. +All measurements will be placed into `measurements.jsonl` in the repo root. Radar sums any duplicated measurements with matching metrics. -To post-process the `measurements.jsonl` file this way in-place, -run `scripts/bench/combine.py` in the repo root after executing the benchmark suite. +To post-process the `measurements.jsonl` file this way, +run `scripts/bench/combine.py measurements.jsonl -o measurements_combined.jsonl` +in the repo root after executing the benchmark suite. The `*.py` symlinks exist only so the python files are a bit nicer to edit in text editors that rely on the file ending. @@ -23,3 +23,10 @@ To add a benchmark to the suite, follow these steps: 1. Create a new folder containing a `run` script and a `README.md` file describing the benchmark, as well as any other files required for the benchmark. 2. Edit `scripts/bench/run` to call the `run` script of your new benchmark. + +The following environment variables are available to an individual benchmark's `run` script: + +- `ROOT_DIR`: absolute path to the root of the repo +- `BENCH_DIR`: absolute path to this directory (`scripts/bench`). +- `OUTPUT_FILE`: absolute path to the `measurements.jsonl` file + that benchmarks should append their measurements to diff --git a/scripts/bench/build/README.md b/scripts/bench/build/README.md index 5292e925d..7a37466b5 100644 --- a/scripts/bench/build/README.md +++ b/scripts/bench/build/README.md @@ -1,6 +1,6 @@ # The `build` benchmark -This benchmark executes a complete build of cslib and collects global and per-module metrics. +This benchmark executes a complete build and collects global and per-module metrics. The following metrics are collected by a wrapper around the entire build process: @@ -9,7 +9,7 @@ The following metrics are collected by a wrapper around the entire build process - `build//task-clock` - `build//wall-clock` -The following metrics are collected from `leanc --profile` and summed across all modules: +The following metrics are collected from `lean --profile` and summed across all modules: - `build/profile///wall-clock` @@ -18,10 +18,15 @@ The following metrics are collected from `lakeprof report`: - `build/lakeprof/longest build path//wall-clock` - `build/lakeprof/longest rebuild path//wall-clock` +The following metrics are collected from a combination of `lakeprof report` and the per-module instructions: + +- `build/lakeprof/longest build path//instructions` +- `build/lakeprof/longest rebuild path//instructions` + The following metrics are collected individually for each module: - `build/module///lines` - `build/module///instructions` -If the file `build_upload_lakeprof_report` is present in the repo root, -the lakeprof report will be uploaded once the benchmark run concludes. +If the `LAKEPROF_UPLOAD_URL` environment variable is set, +the lakeprof report will be uploaded to that URL prefix once the benchmark run concludes. diff --git a/scripts/bench/build/fake-root/bin/lean b/scripts/bench/build/fake-root/bin/lean index 8d2b778e6..2ce14c08b 100755 --- a/scripts/bench/build/fake-root/bin/lean +++ b/scripts/bench/build/fake-root/bin/lean @@ -2,22 +2,29 @@ import argparse import json +import os import re import subprocess import sys from pathlib import Path -NAME = "build" -REPO = Path() -BENCH = REPO / "scripts" / "bench" -OUTFILE = REPO / "measurements.jsonl" +# Global paths +BENCH_DIR = Path(os.environ["BENCH_DIR"]) +WRAPPER_OUT = Path(os.environ["WRAPPER_OUT"]) +WRAPPER_PREFIX = Path(os.environ["WRAPPER_PREFIX"]) +# Other config +BENCHMARK = "build" -def save_result(metric: str, value: float, unit: str | None = None) -> None: +sys.path.append(str(BENCH_DIR)) +import measure # noqa: E402 + + +def save_measurement(metric: str, value: float, unit: str | None = None) -> None: data = {"metric": metric, "value": value} if unit is not None: data["unit"] = unit - with open(OUTFILE, "a+") as f: + with open(WRAPPER_OUT, "a") as f: f.write(f"{json.dumps(data)}\n") @@ -27,15 +34,6 @@ def run(*command: str) -> None: sys.exit(result.returncode) -def run_stderr(*command: str) -> str: - result = subprocess.run(command, capture_output=True, encoding="utf-8") - if result.returncode != 0: - print(result.stdout, end="", file=sys.stdout) - print(result.stderr, end="", file=sys.stderr) - sys.exit(result.returncode) - return result.stderr - - def get_module(setup: Path) -> str: with open(setup) as f: return json.load(f)["name"] @@ -44,33 +42,33 @@ def get_module(setup: Path) -> str: def count_lines(module: str, path: Path) -> None: with open(path) as f: lines = sum(1 for _ in f) - save_result(f"{NAME}/module/{module}//lines", lines) + save_measurement(f"{BENCHMARK}/module/{module}//lines", lines) def run_lean(module: str) -> None: - stderr = run_stderr( - f"{BENCH}/measure.py", - *("-t", f"{NAME}/module/{module}"), - *("-m", "instructions"), - "--", - *("lean", "--profile", "-Dprofiler.threshold=9999999"), - *sys.argv[1:], + _, stderr = measure.main( + cmd=["lean", "--profile", "-Dprofiler.threshold=9999999", *sys.argv[1:]], + output=WRAPPER_OUT, + topics=[f"{BENCHMARK}/module/{module}"], + metrics={"instructions"}, + append=True, + capture=True, ) + # Output of `lean --profile` + # See timeit.cpp for the time format for line in stderr.splitlines(): - # Output of `lean --profile` - # See timeit.cpp for the time format if match := re.fullmatch(r"\t(.*) ([\d.]+)(m?s)", line): name = match.group(1) seconds = float(match.group(2)) if match.group(3) == "ms": seconds = seconds / 1000 - save_result(f"{NAME}/profile/{name}//wall-clock", seconds, "s") + save_measurement(f"{BENCHMARK}/profile/{name}//wall-clock", seconds, "s") def main() -> None: if sys.argv[1:] == ["--print-prefix"]: - print(Path(__file__).resolve().parent.parent) + print(WRAPPER_PREFIX) return if sys.argv[1:] == ["--githash"]: diff --git a/scripts/bench/build/lakeprof_measurements.py b/scripts/bench/build/lakeprof_measurements.py new file mode 100755 index 000000000..db97dcb3b --- /dev/null +++ b/scripts/bench/build/lakeprof_measurements.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 + +# Derives the `build/lakeprof/*` measurements from `lakeprof report` and the +# existing contents of the measurements file. The results are appended back onto +# the measurements file. +# +# Must be run from the src dir so that lakeprof can collect the metadata it +# needs. + +import argparse +import json +import re +import subprocess +import sys +from dataclasses import dataclass +from pathlib import Path + + +def save_measurement( + output: Path, metric: str, value: float, unit: str | None = None +) -> None: + data = {"metric": metric, "value": value} + if unit is not None: + data["unit"] = unit + with open(output, "a") as f: + f.write(f"{json.dumps(data)}\n") + + +def load_instructions_per_module(output: Path) -> dict[str, float]: + pattern = re.compile(r"build/module/(.*)//instructions") + instructions: dict[str, float] = {} + with open(output) as f: + for line in f: + data = json.loads(line) + if match := pattern.fullmatch(data["metric"]): + instructions[match.group(1)] = data["value"] + return instructions + + +@dataclass +class Row: + time: float + time_frac: float + cum_time: float + cum_time_frac: float + module: str + + +def lakeprof_report(*args: str) -> list[Row]: + result = subprocess.run( + ["lakeprof", "report", *args, "-j"], capture_output=True, encoding="utf-8" + ) + if result.returncode != 0: + print(result.stdout, end="", file=sys.stdout) + print(result.stderr, end="", file=sys.stderr) + sys.exit(result.returncode) + return [Row(*row) for row in json.loads(result.stdout)] + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("out", type=Path) + args = parser.parse_args() + out: Path = args.out + + instructions = load_instructions_per_module(out) + + for flag, name in [("-p", "longest build path"), ("-r", "longest rebuild path")]: + rows = lakeprof_report(flag) + + # Total wall-clock time, as reported by lakeprof + save_measurement( + out, f"build/lakeprof/{name}//wall-clock", rows[-1].cum_time, "s" + ) + + # Total instructions, computed from lakeprof's modules and our own measurements + total_instructions = sum(instructions.get(row.module, 0) for row in rows) + save_measurement( + out, f"build/lakeprof/{name}//instructions", total_instructions + ) + + +if __name__ == "__main__": + main() diff --git a/scripts/bench/build/lakeprof_report_upload.py b/scripts/bench/build/lakeprof_report_upload.py index e49627b62..c779115a4 100644 --- a/scripts/bench/build/lakeprof_report_upload.py +++ b/scripts/bench/build/lakeprof_report_upload.py @@ -1,16 +1,24 @@ #!/usr/bin/env python3 import json +import os import subprocess import sys from pathlib import Path +upload_url = os.environ.get("LAKEPROF_UPLOAD_URL") +if not upload_url: + sys.exit(0) +if upload_url.endswith("/"): + upload_url = upload_url[:-1] -def run(*args: str) -> None: - subprocess.run(args, check=True) +# Determine paths relative to the current file. +script_file = Path(__file__) +template_file = script_file.parent / "lakeprof_report_template.html" +root_dir = script_file.parent.parent.parent.parent -def run_stdout(*command: str, cwd: str | None = None) -> str: +def run_stdout(*command: str, cwd: Path | None = None) -> str: result = subprocess.run(command, capture_output=True, encoding="utf-8", cwd=cwd) if result.returncode != 0: print(result.stdout, end="", file=sys.stdout) @@ -19,26 +27,20 @@ def run_stdout(*command: str, cwd: str | None = None) -> str: return result.stdout -def main() -> None: - script_file = Path(__file__) - template_file = script_file.parent / "lakeprof_report_template.html" +sha = run_stdout("git", "rev-parse", "@", cwd=root_dir).strip() +base_url = f"{upload_url}/{sha}" +report = run_stdout("lakeprof", "report", "-prc", cwd=root_dir) - sha = run_stdout("git", "rev-parse", "@").strip() - base_url = f"https://speed.lean-lang.org/cslib-out/{sha}" - report = run_stdout("lakeprof", "report", "-prc") - with open(template_file) as f: - template = f.read() +template = template_file.read_text() +template = template.replace("__BASE_URL__", json.dumps(base_url)) +template = template.replace("__LAKEPROF_REPORT__", report) +(root_dir / "index.html").write_text(template) - template = template.replace("__BASE_URL__", json.dumps(base_url)) - template = template.replace("__LAKEPROF_REPORT__", report) - with open("index.html", "w") as f: - f.write(template) +def upload(file: Path) -> None: + subprocess.run(["curl", "-fT", file, f"{base_url}/{file.name}"], check=True) - run("curl", "-T", "index.html", f"{base_url}/index.html") - run("curl", "-T", "lakeprof.log", f"{base_url}/lakeprof.log") - run("curl", "-T", "lakeprof.trace_event", f"{base_url}/lakeprof.trace_event") - -if __name__ == "__main__": - main() +upload(root_dir / "index.html") +upload(root_dir / "lakeprof.log") +upload(root_dir / "lakeprof.trace_event") diff --git a/scripts/bench/build/run b/scripts/bench/build/run index 39d34b247..d20a8f700 100755 --- a/scripts/bench/build/run +++ b/scripts/bench/build/run @@ -1,23 +1,17 @@ #!/usr/bin/env bash set -euxo pipefail -BENCH="scripts/bench" - # Prepare build lake exe cache get # Run build -LAKE_OVERRIDE_LEAN=true LEAN=$(realpath "$BENCH/build/fake-root/bin/lean") \ - "$BENCH/measure.py" -t build \ - -m instructions -m maxrss -m task-clock -m wall-clock -- \ +LAKE_OVERRIDE_LEAN=true \ + LEAN="$BENCH_DIR/build/fake-root/bin/lean" \ + WRAPPER_OUT="$OUTPUT_FILE" \ + WRAPPER_PREFIX="$BENCH_DIR/build/fake-root" \ + "$BENCH_DIR/measure.py" -t build -d -a -o "$OUTPUT_FILE" -- \ lakeprof record lake build --no-cache # Analyze lakeprof data -lakeprof report -pj | jq -c '{metric: "build/lakeprof/longest build path//wall-clock", value: .[-1][2], unit: "s"}' >> measurements.jsonl -lakeprof report -rj | jq -c '{metric: "build/lakeprof/longest rebuild path//wall-clock", value: .[-1][2], unit: "s"}' >> measurements.jsonl - -# Upload lakeprof report -# Guarded to prevent accidental uploads (which wouldn't work anyways) during local runs. -if [ -f build_upload_lakeprof_report ]; then - python3 "$BENCH/build/lakeprof_report_upload.py" -fi +"$BENCH_DIR/build/lakeprof_measurements.py" "$OUTPUT_FILE" +python3 "$BENCH_DIR/build/lakeprof_report_upload.py" diff --git a/scripts/bench/combine.py b/scripts/bench/combine.py index 2a71f31b9..bf5e3b6dc 100755 --- a/scripts/bench/combine.py +++ b/scripts/bench/combine.py @@ -2,30 +2,79 @@ import argparse import json +import sys from pathlib import Path +from typing import Any -OUTFILE = Path() / "measurements.jsonl" -if __name__ == "__main__": +def add_measurement( + values: dict[str, float], + units: dict[str, str | None], + data: dict[str, Any], +) -> None: + metric = data["metric"] + values[metric] = values.get(metric, 0) + data["value"] + units[metric] = data.get("unit") + + +def format_measurement( + values: dict[str, float], + units: dict[str, str | None], + name: str, +) -> dict[str, Any]: + value = values[name] + unit = units.get(name) + + data: dict[str, Any] = {"metric": name, "value": value} + if unit is not None: + data["unit"] = unit + + return data + + +def main() -> None: parser = argparse.ArgumentParser( - description=f"Combine duplicated measurements in {OUTFILE.name} the way radar does, by summing their values." + description="Combine measurement files in the JSON Lines format, summing duplicated measurements like radar does.", + ) + parser.add_argument( + "input", + nargs="*", + default=[], + help="input files to read measurements from. If none are specified, measurements are read from stdin.", + ) + parser.add_argument( + "-o", + "--output", + type=Path, + help="output file to write measurements to. If not specified, the result is printed to stdout.", ) args = parser.parse_args() + inputs: list[Path] = args.input + output: Path | None = args.output + values: dict[str, float] = {} units: dict[str, str | None] = {} - with open(OUTFILE, "r") as f: - for line in f: - data = json.loads(line) - metric = data["metric"] - values[metric] = values.get(metric, 0) + data["value"] - units[metric] = data.get("unit") - - with open(OUTFILE, "w") as f: - for metric, value in values.items(): - unit = units.get(metric) - data = {"metric": metric, "value": value} - if unit is not None: - data["unit"] = unit - f.write(f"{json.dumps(data)}\n") + # Read measurements + if inputs: + for input in inputs: + with open(input, "r") as f: + for line in f: + add_measurement(values, units, json.loads(line)) + else: + for line in sys.stdin: + add_measurement(values, units, json.loads(line)) + + # Write measurements + if output: + with open(output, "w") as f: + for metric in sorted(values): + f.write(f"{json.dumps(format_measurement(values, units, metric))}\n") + else: + for metric in sorted(values): + print(json.dumps(format_measurement(values, units, metric))) + + +if __name__ == "__main__": + main() diff --git a/scripts/bench/measure.py b/scripts/bench/measure.py index 072f4cdde..c52b6e902 100755 --- a/scripts/bench/measure.py +++ b/scripts/bench/measure.py @@ -9,8 +9,7 @@ import tempfile from dataclasses import dataclass from pathlib import Path - -OUTFILE = Path() / "measurements.jsonl" +from typing import Tuple @dataclass @@ -27,10 +26,24 @@ class RusageMetric: unit: str | None = None +@dataclass +class Result: + category: str + value: float + unit: str | None + + def fmt(self, topic: str) -> str: + data = {"metric": f"{topic}//{self.category}", "value": self.value} + if self.unit is not None: + data["unit"] = self.unit + return json.dumps(data) + + PERF_METRICS = { "task-clock": PerfMetric("task-clock", factor=1e-9, unit="s"), "wall-clock": PerfMetric("duration_time", factor=1e-9, unit="s"), "instructions": PerfMetric("instructions"), + "cycles": PerfMetric("cycles"), } PERF_UNITS = { @@ -43,118 +56,201 @@ class RusageMetric: } ALL_METRICS = {**PERF_METRICS, **RUSAGE_METRICS} +DEFAULT_METRICS = {"instructions", "maxrss", "task-clock", "wall-clock"} -def measure_perf(cmd: list[str], events: list[str]) -> dict[str, tuple[float, str]]: - with tempfile.NamedTemporaryFile() as tmp: - cmd = [ - *["perf", "stat", "-j", "-o", tmp.name], - *[arg for event in events for arg in ["-e", event]], - *["--", *cmd], - ] +def resolve_metrics(metrics: set[str]) -> Tuple[set[str], set[str]]: + perf = set() + rusage = set() + unknown = set() - # Execute command - env = os.environ.copy() - env["LC_ALL"] = "C" # or else perf may output syntactically invalid json - result = subprocess.run(cmd, env=env) - if result.returncode != 0: - sys.exit(result.returncode) + for metric in metrics: + if metric in PERF_METRICS: + perf.add(metric) + elif metric in RUSAGE_METRICS: + rusage.add(metric) + else: + unknown.add(metric) - # Collect results - perf = {} - for line in tmp: - data = json.loads(line) - if "event" in data and "counter-value" in data: - perf[data["event"]] = float(data["counter-value"]), data["unit"] + if unknown: + raise SystemExit(f"unknown metrics: {', '.join(unknown)}") - return perf + return perf, rusage @dataclass -class Result: - category: str +class PerfResult: value: float - unit: str | None + unit: str - def fmt(self, topic: str) -> str: - metric = f"{topic}//{self.category}" - if self.unit is None: - return json.dumps({"metric": metric, "value": self.value}) - return json.dumps({"metric": metric, "value": self.value, "unit": self.unit}) +type PerfResults = dict[str, PerfResult] -def measure(cmd: list[str], metrics: list[str]) -> list[Result]: - # Check args - unknown_metrics = [] - for metric in metrics: - if metric not in RUSAGE_METRICS and metric not in PERF_METRICS: - unknown_metrics.append(metric) - if unknown_metrics: - raise Exception(f"unknown metrics: {', '.join(unknown_metrics)}") - # Prepare perf events - events: list[str] = [] - for metric in metrics: - if info := PERF_METRICS.get(metric): - events.append(info.event) +@dataclass +class MeasureResult: + perf: PerfResults + stdout: str + stderr: str + + +def measure_perf(cmd: list[str], events: set[str], capture: bool) -> MeasureResult: + with tempfile.NamedTemporaryFile() as tmp: + env = os.environ.copy() + env["LC_ALL"] = "C" # or perf may output syntactically invalid JSON + + # On NixOS, perf effectively prepends /usr/bin to the PATH, but in this + # test suite, we often use the PATH to specify the binaries under test. + # Hence, we reset the PATH inside of perf using env. + cmd = [ + *("perf", "stat", "-j", "-o", tmp.name), + *(arg for event in sorted(events) for arg in ["-e", event]), + "--", + *("env", f"PATH={env['PATH']}"), + *cmd, + ] - # Measure - perf = measure_perf(cmd, events) + # Execute command + result = subprocess.run(cmd, env=env, capture_output=capture, encoding="utf-8") + if result.returncode != 0: + if capture: + print(result.stdout, end="", file=sys.stdout) + print(result.stderr, end="", file=sys.stderr) + raise SystemExit(result.returncode) + + # Collect results + perf: PerfResults = {} + for line in tmp: + data = json.loads(line) + if "event" in data and "counter-value" in data: + perf[data["event"]] = PerfResult( + value=float(data["counter-value"]), + unit=data["unit"], + ) + + return MeasureResult( + perf=perf, + stdout=result.stdout or "", + stderr=result.stderr or "", + ) + + +def get_perf_result(perf: PerfResults, metric: str) -> Result: + info = PERF_METRICS[metric] + if info.event in perf: + result = perf[info.event] + else: + # Without the corresponding permissions, + # we only get access to the userspace versions of the counters. + result = perf[f"{info.event}:u"] + + value = result.value * PERF_UNITS.get(result.unit, info.factor) + return Result(category=metric, value=value, unit=info.unit) + + +def get_rusage_result(rusage: resource.struct_rusage, metric: str) -> Result: + info = RUSAGE_METRICS[metric] + value = getattr(rusage, info.name) * info.factor + return Result(category=metric, value=value, unit=info.unit) + + +def main( + cmd: list[str], + output: Path, + topics: list[str], + metrics: set[str], + append: bool = True, + capture: bool = False, +) -> tuple[str, str]: + perf_metrics, rusage_metrics = resolve_metrics(metrics) + perf_events = {PERF_METRICS[metric].event for metric in perf_metrics} + + measured = measure_perf(cmd, perf_events, capture=capture) + perf = measured.perf rusage = resource.getrusage(resource.RUSAGE_CHILDREN) - # Extract results results = [] - for metric in metrics: - if info := PERF_METRICS.get(metric): - if info.event in perf: - value, unit = perf[info.event] - else: - # Without the corresponding permissions, - # we only get access to the userspace versions of the counters. - value, unit = perf[f"{info.event}:u"] + for metric in perf_metrics: + results.append(get_perf_result(perf, metric)) + for metric in rusage_metrics: + results.append(get_rusage_result(rusage, metric)) - value *= PERF_UNITS.get(unit, info.factor) - results.append(Result(metric, value, info.unit)) + with open(output, "a" if append else "w") as f: + for result in results: + for topic in topics: + f.write(f"{result.fmt(topic)}\n") - if info := RUSAGE_METRICS.get(metric): - value = getattr(rusage, info.name) * info.factor - results.append(Result(metric, value, info.unit)) + return measured.stdout, measured.stderr - return results + +class Args: + topic: list[str] + metric: list[str] + default_metrics: bool + output: Path + append: bool + cmd: str + args: list[str] if __name__ == "__main__": parser = argparse.ArgumentParser( - description=f"Measure resource usage of a command using perf and rusage. The results are appended to {OUTFILE.name}.", + description="Measure resource usage of a command using perf and rusage.", + formatter_class=argparse.ArgumentDefaultsHelpFormatter, ) parser.add_argument( - "-t", "--topic", + "-t", action="append", default=[], help="topic prefix for the metrics", ) parser.add_argument( - "-m", "--metric", + "-m", action="append", default=[], help=f"metrics to measure. Can be specified multiple times. Available metrics: {', '.join(sorted(ALL_METRICS))}", ) + parser.add_argument( + "--default-metrics", + "-d", + action="store_true", + help=f"measure a default set of metrics: {', '.join(sorted(DEFAULT_METRICS))}", + ) + parser.add_argument( + "--output", + "-o", + type=Path, + default=Path() / "measurements.jsonl", + help="output file to write measurements to, in the JSON Lines format", + ) + parser.add_argument( + "--append", + "-a", + action="store_true", + help="append to the output file instead of overwriting it", + ) parser.add_argument( "cmd", - nargs="*", help="command to measure the resource usage of", ) - args = parser.parse_args() - - topics: list[str] = args.topic - metrics: list[str] = args.metric - cmd: list[str] = args.cmd - - results = measure(cmd, metrics) - - with open(OUTFILE, "a+") as f: - for result in results: - for topic in topics: - f.write(f"{result.fmt(topic)}\n") + parser.add_argument( + "args", + nargs="*", + default=[], + help="arguments to pass to the command", + ) + args = parser.parse_args(namespace=Args()) + + metrics = set(args.metric) + if args.default_metrics: + metrics |= DEFAULT_METRICS + + main( + cmd=[args.cmd] + args.args, + output=args.output, + topics=args.topic, + metrics=metrics, + append=args.append, + ) diff --git a/scripts/bench/repeatedly.py b/scripts/bench/repeatedly.py new file mode 100755 index 000000000..fae258cf0 --- /dev/null +++ b/scripts/bench/repeatedly.py @@ -0,0 +1,172 @@ +#!/usr/bin/env python3 + +import argparse +import json +import subprocess +import sys +from contextlib import contextmanager +from dataclasses import dataclass +from pathlib import Path + + +@dataclass +class Measurement: + metric: str + value: float + unit: str | None + + @classmethod + def from_json_str(cls, s: str) -> "Measurement": + data = json.loads(s.strip()) + return cls(data["metric"], data["value"], data.get("unit")) + + def to_json_str(self) -> str: + if self.unit is None: + return json.dumps({"metric": self.metric, "value": self.value}) + return json.dumps( + {"metric": self.metric, "value": self.value, "unit": self.unit} + ) + + +@contextmanager +def temporarily_move_outfile(outfile: Path): + outfile_tmp = outfile.with_name(outfile.name + ".repeatedly_tmp") + if outfile_tmp.exists(): + raise Exception(f"{outfile_tmp} already exists") + + outfile.touch() + outfile.rename(outfile_tmp) + try: + yield + finally: + outfile_tmp.rename(outfile) + + +def read_measurements_from_outfile(outfile: Path) -> list[Measurement]: + measurements = [] + with open(outfile, "r") as f: + for line in f: + measurements.append(Measurement.from_json_str(line)) + return measurements + + +def write_measurements_to_outfile( + outfile: Path, measurements: list[Measurement] +) -> None: + with open(outfile, "a") as f: + for measurement in measurements: + f.write(f"{measurement.to_json_str()}\n") + + +def run_once(cmd: list[str], outfile: Path) -> list[Measurement]: + with temporarily_move_outfile(outfile): + proc = subprocess.run(cmd) + if proc.returncode != 0: + sys.exit(proc.returncode) + + return read_measurements_from_outfile(outfile) + + +def sum_by_metric(measurements: list[Measurement]) -> dict[str, Measurement]: + totals: dict[str, Measurement] = {} + for measurement in measurements: + if existing := totals.get(measurement.metric): + measurement.value += existing.value + totals[measurement.metric] = measurement + return totals + + +def repeatedly( + cmd: list[str], + iterations: int, + outfile: Path, + drop_highest: int = 0, + drop_lowest: int = 0, +) -> list[Measurement]: + by_metric: dict[str, list[Measurement]] = {} + + for i in range(iterations): + for metric, measurement in sum_by_metric(run_once(cmd, outfile)).items(): + by_metric.setdefault(metric, []).append(measurement) + + if drop_highest + drop_lowest >= iterations: + raise ValueError( + f"drop_highest ({drop_highest}) + drop_lowest ({drop_lowest}) must be " + f"less than the number of iterations ({iterations})" + ) + + results = [] + for metric, measurements in by_metric.items(): + if drop_highest or drop_lowest: + measurements.sort(key=lambda m: m.value) + measurements = measurements[drop_lowest : len(measurements) - drop_highest] + if not measurements: + continue + unit = measurements[0].unit + value = sum(m.value for m in measurements) / len(measurements) + results.append(Measurement(metric, value, unit)) + + return results + + +class Args: + iterations: int + drop_highest: int + drop_lowest: int + outfile: Path + cmd: str + args: list[str] + + +if __name__ == "__main__": + parser = argparse.ArgumentParser( + description="Repeatedly run a command, averaging the measurements it writes.", + ) + parser.add_argument( + "-n", + "--iterations", + type=int, + default=5, + help="number of iterations", + ) + parser.add_argument( + "-H", + "--drop-highest", + type=int, + default=0, + help="drop the n highest values of each metric before averaging", + ) + parser.add_argument( + "-L", + "--drop-lowest", + type=int, + default=0, + help="drop the n lowest values of each metric before averaging", + ) + parser.add_argument( + "-o", + "--outfile", + type=Path, + default=Path("measurements.jsonl"), + help="measurements file the command under test writes to", + ) + parser.add_argument( + "cmd", + help="command to repeatedly run", + ) + parser.add_argument( + "args", + nargs="*", + default=[], + help="arguments to pass to the command", + ) + args = parser.parse_args(namespace=Args()) + + measurements = repeatedly( + [args.cmd] + args.args, + args.iterations, + args.outfile, + args.drop_highest, + args.drop_lowest, + ) + write_measurements_to_outfile(args.outfile, measurements) diff --git a/scripts/bench/run b/scripts/bench/run index 71af3550c..5e7eb4c32 100755 --- a/scripts/bench/run +++ b/scripts/bench/run @@ -1,10 +1,12 @@ #!/usr/bin/env bash set -euo pipefail -BENCH="scripts/bench" +export ROOT_DIR="$(realpath .)" +export BENCH_DIR="$ROOT_DIR/scripts/bench" +export OUTPUT_FILE="$ROOT_DIR/measurements.jsonl" echo "Running benchmark: build" -"$BENCH/build/run" +"$BENCH_DIR/build/run" echo "Running benchmark: size" -"$BENCH/size/run" +"$BENCH_DIR/size/run" diff --git a/scripts/bench/size/run b/scripts/bench/size/run index 437671149..38bea9581 100755 --- a/scripts/bench/size/run +++ b/scripts/bench/size/run @@ -1,40 +1,54 @@ #!/usr/bin/env python3 import json +import os from pathlib import Path +from typing import Generator -OUTFILE = Path() / "measurements.jsonl" +OUTFILE = Path(os.environ["OUTPUT_FILE"]) -def output_result(metric: str, value: float, unit: str | None = None) -> None: - data = {"metric": metric, "value": value} +def output_result( + topic: str, + category: str, + value: float, + unit: str | None = None, +) -> None: + data = {"metric": f"{topic}//{category}", "value": value} if unit is not None: data["unit"] = unit with open(OUTFILE, "a") as f: f.write(f"{json.dumps(data)}\n") -def measure_leans() -> None: - lean_files = 0 - lean_lines = 0 - for path in Path().glob("Cslib/**/*.lean"): - lean_files += 1 - with open(path) as f: - lean_lines += sum(1 for _ in f) - output_result("size/.lean//files", lean_files) - output_result("size/.lean//lines", lean_lines) +def find_lean_files() -> Generator[Path, None, None]: + for p in Path().iterdir(): + if p.name.startswith("."): + continue + elif p.is_dir(): + yield from p.glob("**/*.lean") + elif p.name.endswith(".lean"): + yield p -def measure_oleans() -> None: - olean_files = 0 - olean_bytes = 0 - for path in Path().glob(".lake/build/**/*.olean"): - olean_files += 1 - olean_bytes += path.stat().st_size - output_result("size/.olean//files", olean_files) - output_result("size/.olean//bytes", olean_bytes, "B") +def measure_lines(topic: str, *paths: Path) -> None: + for path in paths: + if path.is_file(): + lines = len(path.read_text().splitlines()) + output_result(topic, "lines", lines) + output_result(topic, "files", 1) + + +def measure_bytes(topic: str, *paths: Path) -> None: + for path in paths: + if path.is_file(): + bytes = path.stat().st_size + output_result(topic, "bytes", bytes, "B") + output_result(topic, "files", 1) if __name__ == "__main__": - measure_leans() - measure_oleans() + measure_lines("size/.lean", *find_lean_files()) + measure_bytes("size/.olean", *Path().glob(".lake/build/**/*.olean")) + measure_bytes("size/.olean.server", *Path().glob(".lake/build/**/*.olean.server")) + measure_bytes("size/.olean.private", *Path().glob(".lake/build/**/*.olean.private")) From 716047d8fbc507189c116db599866c8080897b4b Mon Sep 17 00:00:00 2001 From: lyj Date: Sun, 12 Jul 2026 06:07:11 +0800 Subject: [PATCH 22/36] fix(LocallyNameless): change multiApp to right-recursive (#708) - Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update related proofs Fixes #706 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- .../LocallyNameless/Stlc/StrongNorm.lean | 2 +- .../LocallyNameless/Untyped/MultiApp.lean | 38 +++++++++++++------ .../LocallyNameless/Untyped/StrongNorm.lean | 15 ++++---- 3 files changed, 35 insertions(+), 20 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index 783ec90ff..cb858529d 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -71,7 +71,7 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})] · grind · intro M N P _ _ _ s _ - grind [ih₂.multiApp M N (s :: P)] + grind [ih₂.multiApp M N (P ++ [s]), multiApp_tail] /-- The `entailsContext` predicate ensures that each variable in the context is mapped to a term in the corresponding semantic map. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean index d7016d7dc..877390646 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean @@ -28,7 +28,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term @[simp, scoped grind =] def multiApp (f : Term Var) : List (Term Var) → Term Var | [] => f -| a :: as => Term.app (multiApp f as) a +| a :: as => multiApp (app f a) as /-- A list of arguments performs a single reduction step @@ -45,18 +45,23 @@ inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where variable {M M' : Term Var} {Ns Ns' : List (Term Var)} +lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = (M.multiApp Ns).app N:= by + induction Ns generalizing M with + | nil => grind + | cons head tail ih => rw [List.cons_append]; apply ih + /-- A term resulting from a multi-application is locally closed if and only if the leftmost term and all arguments applied to it are locally closed -/ @[scoped grind ←] lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by - induction Ns with grind [cases LC] + induction Ns generalizing M with grind [cases LC] /-- Just like ordinary beta reduction, the left-hand side of a multi-application step is locally closed -/ @[scoped grind ←] lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by - induction Ns <;> grind + induction Ns generalizing M M' with grind /-- Congruence lemma for multi reduction of the left most term of a multi-application -/ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : @@ -66,12 +71,18 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : /-- Congruence lemma for single reduction of one of the arguments of a multi-application -/ @[scoped grind ←] lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by - induction steps <;> grind + induction steps generalizing M <;> grind /-- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/ lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by induction steps <;> grind +lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by + induction l using List.reverseRecOn generalizing Ns Ns' with grind + +lemma listFullBeta_cons_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by + induction h with grind + set_option linter.tacticAnalysis.verifyGrindOnly false in /-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then Q must be one of the following forms: @@ -86,16 +97,19 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var} (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨ (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨ (Q = multiApp (M ^ N) Ps) := by - induction Ps generalizing M N Q with + induction Ps using List.reverseRecOn generalizing M N Q with | nil => grind only [cases Xi, multiApp] - | cons P Ps ih => - generalize Heq : (M.abs.app N).multiApp Ps = Q' - have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind - rw [multiApp, Heq] at h_red + | append_singleton Ps P ih => + rw [multiApp_tail] at h_red cases h_red with - | base => cases Ps <;> grind - | appR => grind [→ ListFullBeta.cons] - | appL => grind + | @appL _ _ P' _ P_P' => + have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind + grind [multiApp_tail] + | appR _ h => + have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind) + grind [multiApp_tail] + | base => induction Ps using List.reverseRecOn with grind [multiApp_tail] + /-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index 66dd185ff..ea45ee0e8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -124,20 +124,21 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var} (sn_N : SN FullBeta N) (sn_MNPs : SN FullBeta (multiApp (M ^ N) Ps)) (lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) : SN FullBeta (multiApp (M.abs.app N) Ps) := by - induction Ps with + induction Ps using List.reverseRecOn with | nil => apply sn_app · grind [sn_abs] · exact sn_N · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps] - | cons P Ps ih => + | append_singleton Ps P ih => + rw [multiApp_tail] apply sn_app - · cases lc_MNPs with grind [sn_app_left] - · grind [sn_app_right] + · grind [cases LC, multiApp_tail, sn_app_left] + · grind [multiApp_tail, sn_app_right] · intro Q' P' hstep1 hstep2 have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1 rcases h_cases with h_P | ⟨h_st1, h_st2⟩ - · cases Ps' with grind + · induction Ps' using List.reverseRecOn with grind [multiApp_tail] · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by trans · exact steps_multiApp_r h_Ps_red (by grind) @@ -145,15 +146,15 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var} · apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc] · grind [multiApp_steps_lc] refine sn_steps ?_ sn_MNPs + rw [multiApp_tail] · calc ((M ^ N).multiApp Ps).app P _ ↠βᶠ ((M ^ N).multiApp Ps).app P' := by grind _ ↠βᶠ Q'.abs.app P' := redex_app_l_cong (.trans innerSteps h_st2) (by grind) _ ↠βᶠ Q' ^ P' := by rw [Relation.reflTransGen_iff_eq_or_transGen] at ⊢ innerSteps h_st2 right - cases lc_MNPs refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_)) - all_goals grind only [→ step_lc_r] + all_goals grind end LambdaCalculus.LocallyNameless.Untyped.Term From 7da2a13d2fe36cbb5c0690cb57ed0f8af412bf50 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 13 Jul 2026 04:15:39 -0700 Subject: [PATCH 23/36] feat(FLP): some technical machineries for reasoning about diamond and fairness properties (#612) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR contains some technical machineries for reasoning about diamond and fairness properties about the distributed algorithms introduced in #556: * `CanReachVia.lean` defines the notion of reachability via a subset of processes and proves some of its properties, including some diamond properties. * `FairScheduler.lean` contains a technical machinery for constructing fair executions, which will be used in formalizing some arguments which were either only hinted at or completely glossed over in Völzer's paper. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Impossibility.20of.20distributed.20consensus/with/592462001 --- Cslib.lean | 2 + .../Distributed/FLP/Algorithm.lean | 17 +- .../Distributed/FLP/CanReachVia.lean | 144 ++++++++++ .../Distributed/FLP/FairScheduler.lean | 250 ++++++++++++++++++ Cslib/Computability/Distributed/FLP/README.md | 16 +- 5 files changed, 417 insertions(+), 12 deletions(-) create mode 100644 Cslib/Computability/Distributed/FLP/CanReachVia.lean create mode 100644 Cslib/Computability/Distributed/FLP/FairScheduler.lean diff --git a/Cslib.lean b/Cslib.lean index 4f558680b..1ac2c6ad9 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -26,7 +26,9 @@ public import Cslib.Computability.Automata.NA.ToDA public import Cslib.Computability.Automata.NA.Total public import Cslib.Computability.Automata.Transducers.Transducer public import Cslib.Computability.Distributed.FLP.Algorithm +public import Cslib.Computability.Distributed.FLP.CanReachVia public import Cslib.Computability.Distributed.FLP.Consensus +public import Cslib.Computability.Distributed.FLP.FairScheduler public import Cslib.Computability.Distributed.FLP.ZeroConsensus public import Cslib.Computability.Languages.Congruences.BuchiCongruence public import Cslib.Computability.Languages.Congruences.RightCongruence diff --git a/Cslib/Computability/Distributed/FLP/Algorithm.lean b/Cslib/Computability/Distributed/FLP/Algorithm.lean index ccd90dbf6..8a858af0f 100644 --- a/Cslib/Computability/Distributed/FLP/Algorithm.lean +++ b/Cslib/Computability/Distributed/FLP/Algorithm.lean @@ -202,13 +202,16 @@ theorem tr_diamond {ps : Set P} {x1 x2 : Action P M} {s s1 s2 : State P M S} (hx1 : DestIn ps x1) (hs1 : a.lts.Tr s x1 s1) (hx2 : DestIn psᶜ x2) (hs2 : a.lts.Tr s x2 s2) : ∃ s', a.lts.Tr s1 x2 s' ∧ a.lts.Tr s2 x1 s' := by - cases x1 <;> cases x2 <;> try grind [Algorithm.lts] - case some m1 m2 => - have hd : m1.dest ≠ m2.dest := by grind [DestIn] - obtain ⟨h_m1, rfl⟩ := hs1 - obtain ⟨h_m2, rfl⟩ := hs2 - simp only [Algorithm.lts, exists_eq_right_right] - grind [recvMsg_comm (a := a) hd h_m1 h_m2] + cases x1 <;> cases x2 + · grind [Algorithm.lts] + · grind [Algorithm.lts] + · grind [Algorithm.lts] + · case some m1 m2 => + have hd : m1.dest ≠ m2.dest := by grind [DestIn] + obtain ⟨h_m1, rfl⟩ := hs1 + obtain ⟨h_m2, rfl⟩ := hs2 + simp only [Algorithm.lts, exists_eq_right_right] + grind [recvMsg_comm (a := a) hd h_m1 h_m2] /-- A message that is in-flight stays in-flight as long as it is not received (finite execution version). -/ diff --git a/Cslib/Computability/Distributed/FLP/CanReachVia.lean b/Cslib/Computability/Distributed/FLP/CanReachVia.lean new file mode 100644 index 000000000..44a538e7a --- /dev/null +++ b/Cslib/Computability/Distributed/FLP/CanReachVia.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Distributed.FLP.Algorithm + +/-! # Reachability via a subset of processes + +This file develops a theory of reachability via a subset of processes, that is, what happens +when only a subset of processes can receive messages and take steps. It culminates with two +"diamond properties" of this more refined reachability relation. + +## References + +* [Volzer2004] H. Völzer, A constructive proof for FLP. + Information Processing Letters 92(2), (October 2004) 83–87. +-/ + +@[expose] public section + +namespace Cslib.FLP + +open Function Set Sum Multiset + +variable {P M S : Type*} [DecidableEq P] [DecidableEq M] + +/-- `a.CanReachVia ps s1 s2` means that state `s2` is reachable from state `s1` via a finite +execution of algorithm `a` in which all messages received have destinations in `ps`. -/ +def Algorithm.CanReachVia (a : Algorithm P M S) (ps : Set P) (s1 s2 : State P M S) : Prop := + ∃ xs, a.lts.MTr s1 xs s2 ∧ xs.Forall (DestIn ps) + +/-- `InpEqOn ps inp1 inp2` means that inputs `inp1` and `inp2` agree on all processes in `ps`. -/ +def InpEqOn (ps : Set P) (inp1 inp2 : P → Bool) : Prop := + ∀ p, p ∈ ps → inp1 p = inp2 p + +namespace CanReachVia + +variable {a : Algorithm P M S} + +/-- `a.CanReachVia ps s s'` implies `a.lts.CanReach s s'` for any `ps`. -/ +theorem canReach {ps : Set P} {s s' : State P M S} + (h : a.CanReachVia ps s s') : a.lts.CanReach s s' := by + obtain ⟨xs, h_mtr, _⟩ := h + use xs + +/-- `a.CanReachVia ps s s` is true for any `ps`. -/ +theorem refl (ps : Set P) (s : State P M S) : + a.CanReachVia ps s s := by + use [] + simp + +/-- Extending `CanReachVia` on the left by one step. -/ +theorem stepL {ps : Set P} {x : Action P M} {s1 s2 s3 : State P M S} + (hx : DestIn ps x) (h1 : a.lts.Tr s1 x s2) (h2 : a.CanReachVia ps s2 s3) : + a.CanReachVia ps s1 s3 := by + obtain ⟨xs, _, _⟩ := h2 + use (x :: xs) + grind [LTS.MTr.stepL, List.forall_cons] + +private lemma diamond_helper + {ps : Set P} {x : Action P M} {s s1 s2 : State P M S} + (hx : DestIn ps x) (h1 : a.lts.Tr s x s1) (h2 : a.CanReachVia psᶜ s s2) : + ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.lts.Tr s2 x s' := by + obtain ⟨xs2, h_mtr2, h_via2⟩ := h2 + induction h_mtr2 generalizing s1 + case refl s => + use s1 + simp_all [refl] + case stepL s y t2 ys s2 h_tr2 h_mtr2 h_ind => + obtain ⟨h_y, h_ys⟩ := (List.forall_cons (DestIn psᶜ) y ys).mp h_via2 + obtain ⟨t1, h_tr1, h_tr21⟩ := Algorithm.tr_diamond hx h1 h_y h_tr2 + obtain ⟨s', h_crv1, h_tr2'⟩ := h_ind h_tr21 h_ys + use s', ?_, h_tr2' + exact stepL h_y h_tr1 h_crv1 + +/-- A diamond property for `CanReachVia`. This theorem formalizes Proposition 1 of [Volzer2004]. -/ +theorem diamond {ps : Set P} {s s1 s2 : State P M S} + (h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) : + ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s' := by + obtain ⟨xs1, h_mtr1, h_via1⟩ := h1 + induction h_mtr1 generalizing s2 + case refl s => + use s2 + simp_all [refl] + case stepL s x t1 xs s1 h_tr1 h_mtr1 h_ind => + obtain ⟨h_x, h_xs⟩ := (List.forall_cons (DestIn ps) x xs).mp h_via1 + obtain ⟨t2, h_crv, h_tr2⟩:= diamond_helper h_x h_tr1 h2 + obtain ⟨s', h_crv1, h_crv2⟩ := h_ind h_crv h_xs + use s', h_crv1 + exact stepL h_x h_tr2 h_crv2 + +/-- If inputs `inp1` and `inp2` agree on all processes in `ps` and state `s` is reachable from +the initial state determined by `inp1` by receiving messages with destinations in `ps` only, +then there exists a state `s2` that agrees with `s` on the states of all processes and is +reachable from the initial state determined by `inp2` by receiving messages with destinations +in `ps` only. This theorem is implicitly used in the proof of Lemma 1 of [Volzer2004]. -/ +theorem subset_inp [Fintype P] {ps : Set P} {inp1 inp2 : P → Bool} {s1 : State P M S} + (he : InpEqOn ps inp1 inp2) (hr : a.CanReachVia ps (a.start inp1) s1) : + ∃ s2, a.CanReachVia ps (a.start inp2) s2 ∧ s2.proc = s1.proc := by + obtain ⟨xs, h_mtr, h_xs⟩ := hr + obtain ⟨ss, _, h_ss0, _, _⟩ := LTS.Execution.of_mTr h_mtr + suffices h_inv : ∀ k, (_ : k ≤ xs.length) → + ∃ s2, a.lts.MTr (a.start inp2) (xs.take k) s2 ∧ s2.proc = ss[k].proc ∧ + ∀ m, m.dest ∈ ps → s2.msgs.count m = ss[k].msgs.count m by + obtain ⟨s2, _⟩ := h_inv xs.length (by simp) + use s2, ?_, by grind + use xs, by grind + intro k h_k + induction k + case zero => + use a.start inp2, by grind [LTS.MTr], by grind [Algorithm.start] + intro m h_m + simp only [h_ss0, Algorithm.start, count_map, Message.ext_iff] + congr + grind [InpEqOn] + case succ k h_ind => + obtain ⟨s2, h_mtr, h_proc, h_msgs⟩ := h_ind (by grind) + obtain (_ | ⟨m, h_m⟩) := Option.eq_none_or_eq_some xs[k] + · use s2, ?_, ?_, ?_ + · have h_tr : a.lts.Tr s2 xs[k] s2 := by grind [Algorithm.lts] + grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr] + · grind [Algorithm.tr_none] + · grind [Algorithm.tr_none] + · obtain ⟨_, h_k1⟩ : m ∈ ss[k].msgs ∧ ss[k + 1] = a.recvMsg m ss[k] := by grind [Algorithm.lts] + use a.recvMsg m s2, ?_, ?_, ?_ + · have := List.forall_mem_iff_forall_getElem.mp <| List.forall_iff_forall_mem.mp h_xs + have h_tr : a.lts.Tr s2 xs[k] (a.recvMsg m s2) := by + grind [Algorithm.lts, DestIn, one_le_count_iff_mem] + grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr] + · grind [Algorithm.recvMsg] + · intro m1 h_m1 + by_cases h1 : m1 = m + · simp [h_k1, Algorithm.recvMsg, h_proc, h1, count_erase_self] + grind + · simp [h_k1, Algorithm.recvMsg, h_proc, count_erase_of_ne h1] + grind + +end CanReachVia + +end Cslib.FLP diff --git a/Cslib/Computability/Distributed/FLP/FairScheduler.lean b/Cslib/Computability/Distributed/FLP/FairScheduler.lean new file mode 100644 index 000000000..9e9d622c5 --- /dev/null +++ b/Cslib/Computability/Distributed/FLP/FairScheduler.lean @@ -0,0 +1,250 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Distributed.FLP.Consensus +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Mathlib.Data.List.ReduceOption + +/-! # Machinery for constructing infinite fair executions + +The main goal of this file is to define a `fairScheduler` that, given a function `d` +of type `DeliverMsg`, a state predicate `q`, and a state `s0` of an algorithm `a`, +constructs an infinite execution of `a` starting from state `s0` in which all processes +from a set `ps` are fair and `q` is true infinitely often. With additional assumptions, +we may also want to require that all actions in the infinite execution satisfy an action +predicate `r`. +-/ + +@[expose] public section + +namespace Cslib.FLP + +open Function Set Multiset Filter ωSequence + +variable {P M S : Type*} [DecidableEq P] [DecidableEq M] + +/-- Given a state `s` and a message `m`, a function `d` of type `DeliverMsg` is supposed to +return `(xs, t)` where `xs` is a finite execution from `s` to `t` in which `m` is delivered. -/ +def DeliverMsg P M S := State P M S → Message P M → List (Action P M) × State P M S + +/-- `d.ForallActions r` requires that all actions returned by `d` satisfy `r`. -/ +def DeliverMsg.ForallActions (d : DeliverMsg P M S) (r : Action P M → Prop) : Prop := + ∀ s m, (d s m).fst.Forall r + +/-- `d.foldList s ml ms` uses `d` to deliver all messages that are in `ml` but not in `ms` from +state `s`. Note that if a message `m` in `ml` is delivered during the delivery of an earlier +message, `m` is added to `ms` so that it is not processed again. -/ +def DeliverMsg.foldList (d : DeliverMsg P M S) (s : State P M S) : + List (Message P M) → Finset (Message P M) → List (Action P M) × State P M S + | [], _ => ([], s) + | m :: ml, ms => + if m ∈ ms then + d.foldList s ml ms + else + let (xl1, s1) := d s m + let ms' := ms ∪ xl1.reduceOption.toFinset + let (xl2, s2) := d.foldList s1 ml ms' + (xl1 ++ xl2, s2) + +open scoped Classical in +/-- `d.scheduleMsgs ps s` schedules and delivers all messages which are in-flight in state `s` +and have destinations in `ps` in some order (as determined by choice). If no such message exists, +then the the stuttering step is taken. -/ +noncomputable def DeliverMsg.scheduleMsgs (d : DeliverMsg P M S) (ps : Set P) + (s : State P M S) : List (Action P M) × State P M S := + let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps) + if ms = 0 then + ([none], s) + else + d.foldList s ms.toList ∅ + +namespace DeliverMsg + +variable {d : DeliverMsg P M S} + +/-- If `d.ForallActions r`, then `d.foldList s ml ms` can only use actions satisfying `r`. -/ +theorem foldList_forallActions {r : Action P M → Prop} + (s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M)) + (h : d.ForallActions r) : (d.foldList s ml ms).fst.Forall r := by + induction ml generalizing s ms <;> + grind [DeliverMsg.foldList, DeliverMsg.ForallActions, List.Forall, List.forall_append] + +end DeliverMsg + +/-- Starting from state `s0`, `a.fairSchedular d ps s0` constructs an infinite sequence of +finite executions of `a` by repeatedly applying `d.scheduleMsgs ps`. -/ +noncomputable def Algorithm.fairScheduler (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P) + (s0 : State P M S) : ℕ → List (Action P M) × State P M S + | 0 => ([], s0) + | k + 1 => d.scheduleMsgs ps (a.fairScheduler d ps s0 k).snd + +/-- The infinite sequence of states forming the end states of the finite executions constructed +by `Algorithm.fairScheduler`. -/ +noncomputable def Algorithm.fairSegEnds (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (s0 : State P M S) : ωSequence (State P M S) := + ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).snd) + +/-- The infinite sequence of finite action sequences from the finite executions constructed +by `Algorithm.fairScheduler`. -/ +noncomputable def Algorithm.fairSegActions (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (s0 : State P M S) : ωSequence (List (Action P M)) := + (ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).fst)).tail + +/-- `a.FairDeliverMsg d ps q` says that for any state `s` of `a` satisfying `q` and +any message `m` which is in-flight in `s` and whose destination is in `ps`, `d s m` +produces a legal finite execution of `a` in which `m` is delivered and which ends in +a state satisfying `q` again. -/ +def Algorithm.FairDeliverMsg (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (q : State P M S → Prop) : Prop := + ∀ s m, m ∈ s.msgs ∧ m.dest ∈ ps ∧ q s → + let (xl, t) := d s m + a.lts.MTr s xl t ∧ some m ∈ xl ∧ q t + +namespace FairScheduler + +variable {a : Algorithm P M S} + +/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of +`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/ +theorem fairScheduler_init {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) : + a.fairSegEnds d ps s0 0 = s0 := by + grind [Algorithm.fairScheduler, Algorithm.fairSegEnds] + +/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of +`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/ +theorem fairScheduler_step {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) (k : ℕ) : + d.scheduleMsgs ps (a.fairSegEnds d ps s0 k) = + (a.fairSegActions d ps s0 k, a.fairSegEnds d ps s0 (k + 1)) := by + grind [Algorithm.fairScheduler, Algorithm.fairSegEnds, Algorithm.fairSegActions] + +/-- If `d.ForallActions r`, then `a.fairSegActions d ps s0` can only use actions satisfying `r`. -/ +theorem fairSeg_forallActions {d : DeliverMsg P M S} {r : Action P M → Prop} + (ps : Set P) (s0 : State P M S) (k : ℕ) (ha : d.ForallActions r) (hn : r none) : + (a.fairSegActions d ps s0 k).Forall r := by + grind [fairScheduler_step (a := a) (d := d) ps s0 k, + DeliverMsg.scheduleMsgs, DeliverMsg.foldList_forallActions, List.Forall] + +/-- The correctness of `d.foldList s ml ms` under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fairDeliverMsg_foldList {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} + (hd : a.FairDeliverMsg d ps q) (s : State P M S) + (ml : List (Message P M)) (ms : Finset (Message P M)) + (hs : q s ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → m ∈ s.msgs ∧ m.dest ∈ ps) : + let (xl, t) := d.foldList s ml ms + a.lts.MTr s xl t ∧ q t ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → some m ∈ xl := by + induction ml generalizing s ms + case nil => grind [DeliverMsg.foldList, LTS.MTr] + case cons m ml h_ind => + by_cases h_m : m ∈ ms + · grind [DeliverMsg.foldList] + · let xl1 := (d s m).fst + let s1 := (d s m).snd + let ms' := ms ∪ xl1.reduceOption.toFinset + have (m' : Message P M) : m' ∈ xl1.reduceOption.toFinset ↔ some m' ∈ xl1 := by + simp [List.mem_toFinset, List.reduceOption_mem_iff] + have (m' : Message P M) : m' ∈ ml → ¬ m' ∈ ms' → m' ∈ s1.msgs := by + grind [Algorithm.FairDeliverMsg, Algorithm.mTr_notRcvd_enabled] + grind [DeliverMsg.foldList, Algorithm.FairDeliverMsg, LTS.MTr.comp] + +/-- The correctness of `d.scheduleMsgs ps s` under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fairDeliverMsg_scheduleMsgs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} + (hd : a.FairDeliverMsg d ps q) (s : State P M S) (hs : q s) : + let xl := (d.scheduleMsgs ps s).fst + let t := (d.scheduleMsgs ps s).snd + q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m, m ∈ s.msgs → m.dest ∈ ps → some m ∈ xl := by + classical + intro xl t + let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps) + by_cases h_ms : ms = 0 + · have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs] + simp [ms, eq_zero_iff_forall_notMem] at h_ms + simp only [h1, hs, List.length_cons, List.length_nil, zero_add, Order.lt_one_iff, true_and] + split_ands + · apply LTS.MTr.single + grind [Algorithm.lts] + · grind + · have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by + grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])] + obtain ⟨m, _⟩ := exists_mem_of_ne_zero h_ms + have : some m ∈ xl := by grind [mem_toList] + split_ands <;> grind [mem_toList, mem_filter] + +/-- The correctness of `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` +under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fair_fairSegs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} + (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) : + let ts := a.fairSegEnds d ps s0 + let xls := a.fairSegActions d ps s0 + ∀ k, q (ts k) ∧ a.lts.MTr (ts k) (xls k) (ts (k + 1)) ∧ (xls k).length > 0 ∧ + ∀ m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k := by + classical + intro ts xls k + induction k <;> grind [fairScheduler_init, fairScheduler_step, fairDeliverMsg_scheduleMsgs] + +/-- Given an infinite sequence of non-empty finite executions of algorithm `a`, +if all messages with destinations in `ps` that are in-flight at the beginning of each +finite execution are delivered in that finite execution, then those finite executions can +be concatenated into an infinite execution of `a` in which every process in `ps` is fair. -/ +theorem flatten_fairSegs {ps : Set P} + {ts : ωSequence (State P M S)} {xls : ωSequence (List (Action P M))} + (hmtr : ∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1))) + (hpos : ∀ k, (xls k).length > 0) + (hsch : ∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) : + ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧ + ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by + obtain ⟨ss, h_omega, h_ts⟩ := LTS.OmegaExecution.flatten_mTr hmtr hpos + use ss, h_omega, h_ts + rintro p h_m m ⟨rfl⟩ + by_contra! ⟨k, h_k, h_k'⟩ + have h_xls : ∃ᶠ n in atTop, n ∈ xls.cumLen '' univ := by + apply frequently_iff_strictMono.mpr + use xls.cumLen + grind [cumLen_strictMono] + obtain ⟨j, _, h_j⟩ : ∃ j, k ≤ xls.cumLen j ∧ m ∈ (ts j).msgs := by + obtain ⟨n, _, j, _, _⟩ := frequently_atTop.mp h_xls k + grind [Algorithm.omega_notRcvd_enabled h_omega h_k h_k'] + obtain ⟨i, _, _⟩ := List.getElem_of_mem <| hsch j m h_j h_m + grind [extract_flatten hpos j] + +/-- Under the assumption `a.FairDeliverMsg d ps q`, the infinite sequence of finite executions +of `a` represented by `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` can be concatenated +into an infinite execution of `a` in which every process in `ps` is fair and `q` is true at +the ends of all those finite executions. -/ +theorem fair_omegaExecution {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} + (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) : + let ts := a.fairSegEnds d ps s0 + let xls := a.fairSegActions d ps s0 + ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ + ss 0 = s0 ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧ + (∀ k, q (ss (xls.cumLen k))) ∧ (∀ k, (xls k).length > 0) ∧ + ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by + intro ts xls + obtain ⟨h_q, hmtr, hpos, hsch⟩ : + (∀ k, q (ts k)) ∧ + (∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1))) ∧ + (∀ k, (xls k).length > 0) ∧ + (∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) := by + grind [fair_fairSegs hd s0 hs0] + obtain ⟨ss, _, _, _⟩ := flatten_fairSegs hmtr hpos hsch + have : ss 0 = s0 := by grind [fairScheduler_init] + use ss + grind + +/-- If `d.ForallActions r`, then the concatenation of all `a.fairSegActions d ps s0` segments +can only use actions satisfying `r`. -/ +theorem omega_forall_actions {d : DeliverMsg P M S} {ps : Set P} + {q : State P M S → Prop} {r : Action P M → Prop} + (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) + (ha : d.ForallActions r) (hn : r none) : + ∀ k, r ((a.fairSegActions d ps s0).flatten k) := by + have hpos : ∀ k, (a.fairSegActions d ps s0 k).length > 0 := by grind [fair_fairSegs hd s0 hs0] + simp only [forall_flatten_iff hpos] + grind [fairSeg_forallActions] + +end FairScheduler + +end Cslib.FLP diff --git a/Cslib/Computability/Distributed/FLP/README.md b/Cslib/Computability/Distributed/FLP/README.md index 309a8325a..90b64b249 100644 --- a/Cslib/Computability/Distributed/FLP/README.md +++ b/Cslib/Computability/Distributed/FLP/README.md @@ -1,8 +1,14 @@ -# Impossibility of distributed consensus +
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+
+ +# Impossibility of asynchronous distributed consensus This directory contains a formalization of Völzer's proof [Volzer2004] of the famous result in -distributed computing, first proved by Fischer, Lynch and Paterson [FLP1985], that distributed -consensus is impossible in the presence of even a single crash fault. +distributed computing, first proved by Fischer, Lynch and Paterson [FLP1985], that asynchronous +distributed consensus is impossible in the presence of even a single crash fault. ## Lean files @@ -12,8 +18,6 @@ consensus is impossible in the presence of even a single crash fault. 2. `Consensus.lean` defines what it means for a distributed algorithm to solve the consensus problem in a fault-tolerant way and proves some basic properties. -*The following files will appear in future PRs:* - 3. `FairScheduler.lean` contains a technical machinery for constructing "fair executions", which is used in the proof of `PseudoConsensus.of_consensus` in `PseudoConsensus.lean` and in the proof of `OnePseudoConsensus.fair_nonUniform` in `Impossibility.lean`. @@ -21,6 +25,8 @@ consensus is impossible in the presence of even a single crash fault. 4. `CanReachVia.lean` defines the notion of reachability via a subset of processes and proves some of its properties. +*The following files will appear in future PRs:* + 5. `PseudoConsensus.lean` defines the notion of a fault-tolerant "pseudo-consensus" algorithm, which is central to Völzer's proof, and proves that every `f`-tolerant consensus algorithm is also a `f`-tolerant pseudo-consensus algorithm. From 19f6420ceccec2ada39e08941e1ab04dd0afc927 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Mon, 13 Jul 2026 20:46:28 +0200 Subject: [PATCH 24/36] chore: bump toolchain to v4.32.0 (#717) --- lake-manifest.json | 20 ++++++++++---------- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4457b0aef..6fbd09a09 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d52d26fc2f36d4af5215e91892b33c96dc33915a", + "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "d52d26fc2f36d4af5215e91892b33c96dc33915a", + "inputRev": "81a5d257c8e410db227a6665ed08f64fea08e997", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "77d3cc514f987c1f42f2bbd8a8d56855012dc115", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0-rc1", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lakefile.toml b/lakefile.toml index 817e16581..16a3a0045 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "d52d26fc2f36d4af5215e91892b33c96dc33915a" +rev = "81a5d257c8e410db227a6665ed08f64fea08e997" [[lean_lib]] name = "Cslib" diff --git a/lean-toolchain b/lean-toolchain index 2694eb767..94b9f495b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0-rc1 +leanprover/lean4:v4.32.0 From da9c47c4385474ef4995345708f58cbef96052a7 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Mon, 13 Jul 2026 20:47:25 +0200 Subject: [PATCH 25/36] chore: tweak bench suite (#715) This tweak brings the bench suite more in line with the other repos. It should not affect functionality. Follow-up to #707. --- scripts/bench/build/lakeprof_report_upload.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/scripts/bench/build/lakeprof_report_upload.py b/scripts/bench/build/lakeprof_report_upload.py index c779115a4..450887df8 100644 --- a/scripts/bench/build/lakeprof_report_upload.py +++ b/scripts/bench/build/lakeprof_report_upload.py @@ -12,10 +12,9 @@ if upload_url.endswith("/"): upload_url = upload_url[:-1] -# Determine paths relative to the current file. -script_file = Path(__file__) -template_file = script_file.parent / "lakeprof_report_template.html" -root_dir = script_file.parent.parent.parent.parent +# Determine paths +template_file = Path(__file__).with_name("lakeprof_report_template.html") +root_dir = Path(os.environ["ROOT_DIR"]) def run_stdout(*command: str, cwd: Path | None = None) -> str: From ee41a3d98e085057a6cdb866a681581704edcf35 Mon Sep 17 00:00:00 2001 From: VitaliPath <168389478+VitaliPath@users.noreply.github.com> Date: Mon, 13 Jul 2026 18:43:05 -0400 Subject: [PATCH 26/36] fix(Foundations): add noWs guard to well-formed postfix notation (#675) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses #638. Converts the global well-formed notation to a macro with a `noWs` whitespace guard. This explicitly prevents the postfix parser from greedily consuming the `✓` token across line breaks, resolving the syntax collision with TimeM's prefix tick notation when both modules are imported simultaneously. --------- Co-authored-by: Sean Stoneburner Co-authored-by: Chris Henson --- Cslib/Foundations/Syntax/HasWellFormed.lean | 2 +- CslibTests.lean | 1 + CslibTests/HasWellFormed.lean | 26 +++++++++++++++++++++ 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 CslibTests/HasWellFormed.lean diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index 94ca81629..1dd2a6330 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -20,6 +20,6 @@ class HasWellFormed (α : Type u) where wf (x : α) : Prop /-- Notation for well-formedness. -/ -notation x:max "✓" => HasWellFormed.wf x +macro x:term:max noWs "✓" : term => `(HasWellFormed.wf $x) end Cslib diff --git a/CslibTests.lean b/CslibTests.lean index 90903a188..b26f3aa5d 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -7,6 +7,7 @@ import CslibTests.GrindLint import CslibTests.HML import CslibTests.HasFresh import CslibTests.HasSubstitution +import CslibTests.HasWellFormed import CslibTests.ImportWithMathlib import CslibTests.LTS import CslibTests.LambdaCalculus diff --git a/CslibTests/HasWellFormed.lean b/CslibTests/HasWellFormed.lean new file mode 100644 index 000000000..e408cb3d2 --- /dev/null +++ b/CslibTests/HasWellFormed.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2026 Sean D. Stoneburner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sean D. Stoneburner +-/ +import Cslib.Algorithms.Lean.TimeM +import Cslib.Foundations.Syntax.HasWellFormed + +open Cslib.Algorithms.Lean + +/-! +# Syntax Collision Test +This file tests that the `✓` prefix macro from `TimeM` does not collide with +the `✓` postfix notation from `HasWellFormed` across line breaks. +-/ + +def testParserCollision (n : Nat) : TimeM Nat Nat := do + let m := n + ✓ return m + +-- Ensure the postfix notation still functions correctly when attached without whitespace +variable {α : Type*} [Cslib.HasWellFormed α] (x : α) + +/-- info: Cslib.HasWellFormed.wf x : Prop -/ +#guard_msgs in +#check x✓ From 2e0ac2eebde8d07120b920a7dbbd8d52fec35108 Mon Sep 17 00:00:00 2001 From: Chi-Yun Hsu <116553435+chiyunhsu@users.noreply.github.com> Date: Wed, 15 Jul 2026 20:34:56 -0700 Subject: [PATCH 27/36] feat(Computability/Languages): languages matching regular expressions are regular (#720) Prove languages matching regular expressions are regular in IsRegular.regex. The proof uses existing theorems IsRegular.add, IsRegular.mul, and IsRegular.kstar. Prove remaining key ingredient that the language containing only the one character string is regular in IsRegular.char. Implemented collaboratively by Brooke Gill and Chi-Yun Hsu --------- Co-authored-by: Chi-Yun Hsu Co-authored-by: Brooke Gill <96643991+brooke-gill@users.noreply.github.com> --- Cslib/Computability/Languages/Language.lean | 4 +++ .../Languages/RegularLanguage.lean | 28 +++++++++++++++++++ 2 files changed, 32 insertions(+) diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index 0824cb165..c9bd66234 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -41,6 +41,10 @@ theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) theorem le_one_iff_eq : l ≤ 1 ↔ l = 0 ∨ l = 1 := subset_singleton_iff_eq +@[simp, scoped grind =] +theorem mem_singleton (x y : List α) : x ∈ ({y} : Language α) ↔ x = y := + Iff.rfl + @[simp, scoped grind =] theorem mem_sub_one (x : List α) : x ∈ (l - 1) ↔ x ∈ l ∧ x ≠ [] := Iff.rfl diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index 6e1bbcc8e..07745dd34 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -13,6 +13,7 @@ public import Cslib.Computability.Automata.NA.Concat public import Cslib.Computability.Automata.NA.Loop public import Cslib.Computability.Automata.NA.ToDA public import Mathlib.Computability.DFA +public import Mathlib.Computability.RegularExpressions public import Mathlib.Data.Finite.Sum public import Mathlib.Data.Set.Card @@ -184,4 +185,31 @@ theorem IsRegular.congr_fin_index {Symbol : Type} use Quotient c.eq, inferInstance, ⟨c.toDA, {a}⟩ exact DA.FinAcc.congr_language_eq +/-- The language containing only the one character string `a` is regular. -/ +@[simp] +theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by + rw [IsRegular.iff_dfa] + classical + let flts := FLTS.mk (fun (s : Fin 3) (x : Symbol) ↦ if (s = 0 ∧ x = a) then 1 else 2) + use Fin 3, inferInstance, ⟨DA.mk flts 0, {1}⟩ + ext xs + induction xs using List.reverseRec with + | nil => grind [Accepts, Language.mem_singleton] + | append_singleton xs x ih => + simp only [mem_language, Accepts, Language.mem_singleton, FLTS.mtr_concat_eq] at ih ⊢ + constructor + · induction xs using List.reverseRec <;> grind + · simp_all [flts, List.append_eq_cons_iff] + +/-- Languages matching regular expressions are regular. -/ +theorem IsRegular.regex [Inhabited Symbol] {r : RegularExpression Symbol} : + r.matches'.IsRegular := by + induction r with + | zero => simp + | epsilon => simp + | char a => simp [IsRegular.char a] + | plus P Q hP hQ => grind [RegularExpression.matches', IsRegular.add] + | comp P Q hP hQ => grind [RegularExpression.matches', IsRegular.mul] + | star P hP => grind [RegularExpression.matches', IsRegular.kstar] + end Cslib.Language From ae6113e1339fce6b68de84a37173ffcc6e13e55d Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Wed, 15 Jul 2026 21:07:13 -0700 Subject: [PATCH 28/36] chore: add the consequences of an empty alphabet type on Language and OmegaLanguage (#722) This PR proves some consequences of an empty alphabet type (denoted by `Symbol`) on Language and OmegaLanguage: (1) The only possible languages over an empty alphabet are {} and {[]}. (2) The only possible omega-language over an empty alphabet is {}. Furthermore, (1) enables the assumption `[Inhabited Symbol]` to be removed from the regular language closure properties `IsRegular.mul` and `IsRegular.kstar`. Now no closure property for regular languages has that assumption. --- Cslib/Computability/Automata/NA/Pair.lean | 2 +- Cslib/Computability/Languages/Language.lean | 22 ++++++++++++ .../Languages/OmegaLanguage.lean | 6 ++++ .../Languages/RegularLanguage.lean | 35 +++++++++++-------- .../Foundations/Data/OmegaSequence/Init.lean | 3 ++ 5 files changed, 53 insertions(+), 15 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean index 45beb89d7..e5c2c82f4 100644 --- a/Cslib/Computability/Automata/NA/Pair.lean +++ b/Cslib/Computability/Automata/NA/Pair.lean @@ -50,7 +50,7 @@ theorem LTS.mem_pairViaLang {lts : LTS State Symbol} {via : Set State} /-- `LTS.pairViaLang via s t` is a regular language if there are only finitely many states. -/ @[simp] -theorem LTS.pairViaLang_regular [Inhabited Symbol] [Finite State] {lts : LTS State Symbol} +theorem LTS.pairViaLang_regular [Finite State] {lts : LTS State Symbol} {via : Set State} {s t : State} : (lts.pairViaLang via s t).IsRegular := by apply IsRegular.iSup grind [Language.IsRegular.mul, LTS.pairLang_regular] diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index c9bd66234..2ff6f64ee 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -18,6 +18,17 @@ as defined and developed in `Mathlib.Computability.Language`. @[expose] public section +namespace List + +variable {α : Type*} + +/-- `[]` is the only list over an empty type. -/ +theorem eq_nil_ofIsEmpty [IsEmpty α] (xl : List α) : xl = [] := by + have hu := List.uniqueOfIsEmpty (α := α) + simp [Unique.eq_default] + +end List + namespace Language open Set List @@ -25,6 +36,17 @@ open scoped Computability variable {α : Type*} {l m : Language α} +/-- `0` and `1` are the only possible languages over an empty type. -/ +theorem eq_zero_or_one_ofIsEmpty [IsEmpty α] (l : Language α) : l = 0 ∨ l = 1 := by + by_cases h : l = 0 + · simp [h] + · right + ext xl + obtain ⟨yl, _⟩ := nonempty_iff_ne_empty.mpr h + obtain ⟨rfl⟩ := eq_nil_ofIsEmpty xl + obtain ⟨rfl⟩ := eq_nil_ofIsEmpty yl + simpa + @[simp] theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) : (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i := diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index 8b5fbb45c..78483c036 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -98,6 +98,12 @@ def equiv : ωLanguage α ≃ Set (ωSequence α) where instance : CompleteAtomicBooleanAlgebra (ωLanguage α) := equiv.completeAtomicBooleanAlgebra +/-- `⊥` is the only possible ω-language over an empty type. -/ +theorem eq_bot_ofIsEmpty [IsEmpty α] (p : ωLanguage α) : p = ⊥ := by + ext xs + exfalso + exact IsEmpty.false xs + set_option linter.tacticAnalysis.verifyGrindOnly false in instance : SetLike (ωLanguage α) (ωSequence α) where coe := ωLanguage.toSet diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index 07745dd34..745696183 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -154,27 +154,34 @@ theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy open NA.FinAcc Sum in /-- The concatenation of two regular languages is regular. -/ @[simp] -theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol} +theorem IsRegular.mul {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular := by - rw [IsRegular.iff_nfa] at h1 h2 ⊢ - obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1 - obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2 - use Option State1 ⊕ Option State2, inferInstance, - ⟨finConcat nfa1 nfa2, inr '' (some '' nfa2.accept)⟩ - exact finConcat_language_eq + obtain (he | hne) := isEmpty_or_nonempty Symbol + · obtain (rfl | rfl) := Language.eq_zero_or_one_ofIsEmpty l1 <;> + obtain (rfl | rfl) := Language.eq_zero_or_one_ofIsEmpty l2 <;> simp + · have := Classical.inhabited_of_nonempty hne + rw [IsRegular.iff_nfa] at h1 h2 ⊢ + obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1 + obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2 + use Option State1 ⊕ Option State2, inferInstance, + ⟨finConcat nfa1 nfa2, inr '' (some '' nfa2.accept)⟩ + exact finConcat_language_eq -- TODO: fix proof to work with backward.isDefEq.respectTransparency set_option backward.isDefEq.respectTransparency false in open NA.FinAcc Sum in /-- The Kleene star of a regular language is regular. -/ @[simp] -theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol} +theorem IsRegular.kstar {l : Language Symbol} (h : l.IsRegular) : (l∗).IsRegular := by - by_cases h_l : l = 0 - · simp [h_l] - · rw [IsRegular.iff_nfa] at h ⊢ - obtain ⟨State, h_fin, nfa, rfl⟩ := h - use Unit ⊕ Option State, inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l + obtain (he | hne) := isEmpty_or_nonempty Symbol + · obtain (rfl | rfl) := Language.eq_zero_or_one_ofIsEmpty l <;> simp + · have := Classical.inhabited_of_nonempty hne + by_cases h_l : l = 0 + · simp [h_l] + · rw [IsRegular.iff_nfa] at h ⊢ + obtain ⟨State, h_fin, nfa, rfl⟩ := h + use Unit ⊕ Option State, inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l /-- If a right congruence is of finite index, then each of its equivalence classes is regular. -/ @[simp] @@ -202,7 +209,7 @@ theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by · simp_all [flts, List.append_eq_cons_iff] /-- Languages matching regular expressions are regular. -/ -theorem IsRegular.regex [Inhabited Symbol] {r : RegularExpression Symbol} : +theorem IsRegular.regex {r : RegularExpression Symbol} : r.matches'.IsRegular := by induction r with | zero => simp diff --git a/Cslib/Foundations/Data/OmegaSequence/Init.lean b/Cslib/Foundations/Data/OmegaSequence/Init.lean index 3d6d71252..0013a221a 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Init.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Init.lean @@ -32,6 +32,9 @@ variable (m n : ℕ) (x y : List α) (a b : ωSequence α) instance [Inhabited α] : Inhabited (ωSequence α) := ⟨ωSequence.const default⟩ +instance [h : IsEmpty α] : IsEmpty (ωSequence α) where + false xs := IsEmpty.false (xs 0) + @[simp, scoped grind =] protected theorem eta (s : ωSequence α) : head s ::ω tail s = s := by apply DFunLike.ext From 30f8d3c0f51e98d0bd0e325ad59288c32f30f8d2 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Thu, 16 Jul 2026 10:06:53 +0200 Subject: [PATCH 29/36] chore: bump toolchain to v4.33.0-rc1 (#723) Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] Co-authored-by: mathlib4-bot Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison Co-authored-by: Chris Henson Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou Co-authored-by: Alexandre Rademaker Co-authored-by: Fabrizio Montesi --- Cslib/Computability/Automata/NA/Pair.lean | 2 +- .../Computability/Languages/MyhillNerode.lean | 4 ++-- .../Languages/OmegaLanguage.lean | 9 ++++++--- .../Turing/SingleTape/Deterministic.lean | 3 +-- Cslib/Computability/URM/StandardForm.lean | 5 +++-- .../LocallyNameless/Fsub/Typing.lean | 2 +- .../Logics/LinearLogic/CLL/EtaExpansion.lean | 7 ++----- .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 2 +- Cslib/Probability/PMF.lean | 2 +- CslibTests/DFA.lean | 4 ++-- lake-manifest.json | 20 +++++++++---------- lakefile.toml | 2 +- lean-toolchain | 2 +- 13 files changed, 32 insertions(+), 32 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean index e5c2c82f4..fa233e806 100644 --- a/Cslib/Computability/Automata/NA/Pair.lean +++ b/Cslib/Computability/Automata/NA/Pair.lean @@ -15,7 +15,7 @@ public import Cslib.Computability.Languages.RegularLanguage namespace Cslib -open Language Automata Acceptor +open Cslib.Language Automata Acceptor variable {Symbol : Type*} {State : Type} diff --git a/Cslib/Computability/Languages/MyhillNerode.lean b/Cslib/Computability/Languages/MyhillNerode.lean index 87a3a61a7..f22fe8646 100644 --- a/Cslib/Computability/Languages/MyhillNerode.lean +++ b/Cslib/Computability/Languages/MyhillNerode.lean @@ -74,7 +74,7 @@ variable {l : Language α} theorem nerodeCongruenceDA_language_eq (l : Language α) : language (l.NerodeCongruenceDA) = l := by ext x - simp only [NerodeCongruenceDA, language, Acceptor.Accepts, congr_mtr_eq, Set.mem_image] + simp only [NerodeCongruenceDA, language, Acceptor.Accepts, congr_mtr_eq] constructor · rintro ⟨y, hy, heq⟩ have h1 := Quotient.eq.mp heq [] @@ -161,7 +161,7 @@ end Language namespace Cslib.Automata.DA.FinAcc -open Cslib Language Automata DA FinAcc Acceptor +open Cslib Cslib.Language Automata DA FinAcc Acceptor open scoped RightCongruence /-- The minimal DFA accepting `l` has the same number of states as the number of equivalence classes diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index 78483c036..cd17e2101 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -284,7 +284,8 @@ theorem hmul_bot : l * (⊥ : ωLanguage α) = ⊥ := by @[simp, scoped grind =] theorem one_hmul : (1 : Language α) * p = p := by - simp [hmul_def, Language.one_def, Language.toSet] + simp [hmul_def] + simp [Language.one_def, Language.toSet] theorem hmul_sup : l * (p ⊔ q) = l * p ⊔ l * q := by ext : 1 @@ -464,8 +465,10 @@ theorem omegaLim_zero : (0 : Language α)↗ω = ⊥ := by simp [omegaLim_def, bot_def] @[simp, scoped grind =] -theorem map_id (p : ωLanguage α) : map id p = p := - by simp [map] +theorem map_id (p : ωLanguage α) : map id p = p := by + unfold map + change { toSet := id '' p.toSet } = p + simp @[scoped grind =] theorem map_map (g : β → γ) (f : α → β) (p : ωLanguage α) : map g (map f p) = map (g ∘ f) p := by diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean index 79c4ae530..29f379d5a 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean @@ -318,8 +318,7 @@ private theorem map_toCompCfg_right_step : cases cfg2 with | mk state BiTape => cases state with - | none => - simp only [step, toCompCfg_right, Option.map_none, compComputer] + | none => rfl | some q => generalize hM : tm2.tr q BiTape.head = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result diff --git a/Cslib/Computability/URM/StandardForm.lean b/Cslib/Computability/URM/StandardForm.lean index f1abcf344..51a288b6b 100644 --- a/Cslib/Computability/URM/StandardForm.lean +++ b/Cslib/Computability/URM/StandardForm.lean @@ -217,8 +217,9 @@ theorem eval_toStandardForm {p : Program} {inputs : List ℕ} : · simp only [Part.map_Dom] exact Halts.toStandardForm_iff · intro hp hq - simp only [Part.map_get, Function.comp_apply, Regs.output, - evalState_toStandardForm_regs hp hq] + have := Part.map_get (fun x : State => x.regs.output) (evalState p inputs) hp + have := Part.map_get (fun x : State => x.regs.output) (evalState p.toStandardForm inputs) hq + simp_all [Function.comp_def, evalState_toStandardForm_regs hp hq] /-- A program is equivalent to its standard form. -/ theorem toStandardForm_equiv (p : Program) : p.toStandardForm ≈ p := diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index b983ddb55..1e0be09d1 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -30,7 +30,7 @@ variable {Var : Type*} [DecidableEq Var] [HasFresh Var] namespace LambdaCalculus.LocallyNameless.Fsub -open Term Ty Ty.Wf Env.Wf Sub Context List Binding +open Term Ty Ty.Wf Env.Wf Fsub.Sub Context List Binding /-- The typing relation. -/ inductive Typing : Env Var → Term Var → Ty Var → Prop diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean index 9aa98ab04..1148ef3ef 100644 --- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean +++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean @@ -109,11 +109,8 @@ private lemma Proof.expand_onlyAtomicAxioms_dual {a : Proposition Atom} : induction a with | one => simp +contextual [dual, expand, onlyAtomicAxioms] | bot => - intro h - rw [←h] - congr 1 - · grind - · simp [dual, expand, rwConclusion, Logic.InferenceSystem.rwConclusion] + #adaptation_note /-- see https://github.com/leanprover/lean4/pull/13484/ -/ + grind [expand, dual.eq_def] | _ => grind [Proposition.expand, Proposition.dual_inj] open Proposition Proof in diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index 25cd8138e..fbb2fe840 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -679,7 +679,7 @@ lemma valid_with {G H : Fact P} : (G & H).IsValid ↔ G.IsValid ∧ H.IsValid := end Fact -open Fact +open PhaseSpace.Fact /-! ## Interpretation of propositions -/ diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index d20be22be..8393eb229 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -39,7 +39,7 @@ the Mathlib module instead. namespace Cslib.Probability.PMF -open PMF ENNReal +open ENNReal universe u v variable {α : Type u} {β : Type v} diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean index 09ccd69d7..c48ee1c1b 100644 --- a/CslibTests/DFA.lean +++ b/CslibTests/DFA.lean @@ -15,12 +15,12 @@ open Cslib.Automata inductive Floor where | one | two -deriving DecidableEq, Fintype +deriving DecidableEq inductive Direction where | up | down -deriving DecidableEq, Fintype +deriving DecidableEq def elevator : DA Floor Direction where tr diff --git a/lake-manifest.json b/lake-manifest.json index 6fbd09a09..30ae49d4f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", + "rev": "79d0395a1825a6264ad5d269e35e60537518955e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "81a5d257c8e410db227a6665ed08f64fea08e997", + "inputRev": "79d0395a1825a6264ad5d269e35e60537518955e", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", + "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "rev": "57d3325be72a842920813bcb40f96a6f7393c185", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "rev": "31a49105f960721073a9adfc82b261f5d0f2ce1e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.33.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lakefile.toml b/lakefile.toml index 16a3a0045..90255cbb4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "81a5d257c8e410db227a6665ed08f64fea08e997" +rev = "79d0395a1825a6264ad5d269e35e60537518955e" [[lean_lib]] name = "Cslib" diff --git a/lean-toolchain b/lean-toolchain index 94b9f495b..fd85b262b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0 +leanprover/lean4:v4.33.0-rc1 From 2de9c55ae44f96c3768988253ff9631f33eac034 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 17 Jul 2026 07:19:59 +0200 Subject: [PATCH 30/36] feat: add READMEs to main directories (#714) This PR adds README files to some of the main source code directories, covering explanations on principles and vision for CSLib that I've found myself repeating often in private and public conversations. --------- Co-authored-by: Fabrizio Montesi --- Cslib/Algorithms/README.md | 31 +++++++++++++++++++++++ Cslib/Computability/README.md | 35 ++++++++++++++++++++++++++ Cslib/Crypto/README.md | 26 ++++++++++++++++++++ Cslib/Foundations/README.md | 32 ++++++++++++++++++++++++ Cslib/Languages/README.md | 29 ++++++++++++++++++++++ Cslib/Logics/README.md | 46 +++++++++++++++++++++++++++++++++++ ORGANISATION.md | 4 ++- 7 files changed, 202 insertions(+), 1 deletion(-) create mode 100644 Cslib/Algorithms/README.md create mode 100644 Cslib/Computability/README.md create mode 100644 Cslib/Crypto/README.md create mode 100644 Cslib/Foundations/README.md create mode 100644 Cslib/Languages/README.md create mode 100644 Cslib/Logics/README.md diff --git a/Cslib/Algorithms/README.md b/Cslib/Algorithms/README.md new file mode 100644 index 000000000..9d946c476 --- /dev/null +++ b/Cslib/Algorithms/README.md @@ -0,0 +1,31 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Clark Barrett, Swarat Chaudhuri, Jim Grundy, Fabrizio Montesi, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
+
+ +# Algorithms + +This directory hosts **algorithms and their properties**. These properties concern functional correctness, complexity, and other relevant results. The directory also includes dedicated facilities for reasoning about algorithms written in Lean. + +The broader aim is to develop a library of verified algorithms, both in Lean and in other languages formalised in CSLib. Accordingly, it is in scope to study algorithms implemented as Lean programs as well as algorithms expressed inside one of CSLib's [Languages](../Languages), depending on the purpose of the development. +All algorithms sit in a language-specific subdirectory depending on the language they are written in, like `Boole`, `Lean`, etc. + +## Principles + +### Synergies with languages and logics + +Important synergies are expected with both [Languages](../Languages) and [Logics](../Logics). Languages provide settings in which algorithms can be written and studied under formal semantics, while logics provide tools for specifying and proving their properties. + +One long-term aim is to support principled reasoning pipelines where algorithms are defined in a language, specified through logical notions, and verified inside shared semantic frameworks. + +### Dealing with optimisation + +Optimising an algorithm can make it harder to reason about it. When this happens, one can prove a relation (e.g., functional or behavioural) to a simpler, less optimised version, and then work by transferring results from it. +In doing this, we expect contributions to leverage Lean's and CSLib's common infrastructures whenever reasonable. + +## Plans and notes + +- We aim at developing a comprehensive library of verified algorithms, covering both Lean implementations and algorithms represented in other languages. +- We plan on expanding the infrastructure for proving properties of Lean algorithms, including correctness, complexity, and other forms of analysis. +- Reusable mathematical and semantic infrastructure should live elsewhere in CSLib when it is more general-purpose, so developments in this directory should integrate well with [Foundations](../Foundations), [Languages](../Languages), and [Logics](../Logics). diff --git a/Cslib/Computability/README.md b/Cslib/Computability/README.md new file mode 100644 index 000000000..f2ab58842 --- /dev/null +++ b/Cslib/Computability/README.md @@ -0,0 +1,35 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+ +# Computability + +This directory hosts **formal developments in computability and neighbouring areas**. Its scope includes automata, complexity classes, formal languages over finite and infinite words, and other machine models. + +## Principles + +### Multiple computational models + +There is a plethora of computational models in the literature, some of which are very near to each other (e.g., Turing machines and Wang B-machines). Depending on the aim, one can be more convenient than the other. +In general, computability can be studied through different kinds of objects. + +These representations can coexist when they serve different purposes. A central goal is to make their tradeoffs explicit and to connect them where possible. + +### Reuse of common infrastructure + +The [Foundations](../Foundations) directory offers abstractions that are directly useful for computability-theoretic developments and should be reused as much as possible. Examples already present in this directory include the use of labelled transition systems for automata and distributed algorithms, tape structures for Turing machines, and general relation-theoretic tools for machine semantics. + +This approach enables: +1. Reusing and transferring constructions and results across different models. +2. Applying CSLib's [logics](../Logics) to reason about computational models. +3. Developing connections between computability models and other areas (like the constructions of automata based on transition systems). + +### Separation from languages + +Some of the developments here are close to [Languages](../Languages), but are placed here instead because the emphasis is on formal languages over words and models typically linked to computability studies. + +## Plans and notes + +- We plan on expanding this directory with more machine models and associated results, including equivalence results, closure properties, and other metatheory. +- We plan on clarifying and formalising connections between language-theoretic, automata-theoretic, machine-based, and distributed perspectives on computation. diff --git a/Cslib/Crypto/README.md b/Cslib/Crypto/README.md new file mode 100644 index 000000000..75ffac536 --- /dev/null +++ b/Cslib/Crypto/README.md @@ -0,0 +1,26 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+ +# Crypto + +This directory hosts **cryptographic definitions, primitives, protocol models, and related security metatheory**. Its scope includes both basic cryptographic notions and larger developments such as security protocols. + +We aim at supporting both abstract security reasoning and concrete protocol developments, while making explicit the relations between them. To this end, this part of CSLib has very important relationships with [Languages](../Languages) and [Logics](../Logics), explained in the remainder. + +## Principles + +### Integration with languages + +Whenever appropriate, cryptographic primitives should be developed so that they compose well with CSLib's [languages](../Languages) that offer a way to integrate a computational substrate. This is common, for example, in choreographic programming languages and many process calculi. + +The aim is to build end-to-end models where cryptographic operations appear inside larger communicating or computational systems. + +To this end, we expect to leverage the combination of `Crypto` and [Languages](../Languages) to define and formally reason about security protocols. CSLib's common semantics APIs connecting [Languages](../Languages) and [Logics](../Logics) should enable such reasoning. + +## Plans and notes + +- We plan on developing applied calculi and logics for modelling and reasoning about security protocols. +- We plan on developing a comprehensive library of primitives and foundational protocols, together with their proofs of correctness. +- We plan on supporting downstream efforts on the development of secure digital infrastructures (including implementation of complex secure applications and systems). diff --git a/Cslib/Foundations/README.md b/Cslib/Foundations/README.md new file mode 100644 index 000000000..c99a262fd --- /dev/null +++ b/Cslib/Foundations/README.md @@ -0,0 +1,32 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+ +# Foundations + +This directory covers **common foundations** for the rest of CSLib and downstream developments. As such, it acts as its fulcrum of integration through common concepts and APIs. This directory includes also additional results about foundational data objects defined in Mathlib, such as `Nat` and `Set`. + +Please browse the subdirectories for details. + +The foundational approach to semantics spans multiple directories and has a large role; it is explained below. + +## Semantics + +A recurring aspect that cuts across different areas is semantics. Examples of such areas include concurrency theory, computational models, logics, modelling languages, programming languages, and security protocols. + +Most of the APIs for semantics provided in `Foundations` are in the [Semantics](Semantics) directory. An example of an exception is the [Relation](Relation) directory, which sits at the top level. + +The vision is to provide common abstractions that can be reused throughout CSLib. Beyond providing reusable definitions, having common APIs for semantics is important for multiple reasons. The next list covers some illustrative examples. + +- The modular use of modal and dynamic logics to reason about programs. +- The sharing of semantic metatheory, such as behavioural equivalences for labelled transition systems (bisimulation, trace equivalence, etc.) and common definitions like confluence. +- The development of provably-correct compilers between languages based on these abstractions, supporting for example proofs of bisimilarity or full abstraction. +- The elicitation of connections between different domains, including computability, crypto, logic, programming languages, etc. + +### Plans + +- Many modules are still missing, for example facilities for probabilistic operational semantics, derivatives and antiderivatives for transition systems, logical relations, etc. We plan to develop develop a comprehensive library. +- We plan on building general frameworks that give important metatheoretical properties about the semantics of objects that respect certain properties (e.g., rule formats, GSOS) for free (or at least in principled ways rather than doing it from scratch). +- We plan both on developing constructions that embed different semantic models into each other and to prove separation results between them. +- We plan on pushing towards building formal connections between different domains based on a semantic approach. diff --git a/Cslib/Languages/README.md b/Cslib/Languages/README.md new file mode 100644 index 000000000..eb6722ccd --- /dev/null +++ b/Cslib/Languages/README.md @@ -0,0 +1,29 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+ +# Languages + +This directory hosts **modelling and programming languages** formalised in CSLib and their properties. Their components can include syntax, semantics, typing and other reasoning disciplines, execution facilities (compilers, interpreters, etc.), behavioural theories, supporting metatheory, etc. +We are interested in many kinds of languages, from foundational calculi to applied programming frameworks. + +The focus is not only on individual languages in isolation, but also on exposing them through reusable abstractions from [Foundations](../Foundations), such as contexts, substitution, congruence, reduction systems, and labelled transition systems. + +## Principles + +### Reuse of common infrastructure + +The [Foundations](../Foundations) directory offers useful modules for language development, which should be used as much as possible. +These modules include support for syntax (like contexts and congruence relations), semantics (like transition systems), compiler correctness (like behavioural relations), and more. + +### Multiple representations are welcome + +Different representations can coexist when they serve different purposes. For example `LambdaCalculus` currently contains both named and locally nameless developments. The goal is to make tradeoffs explicit and to connect them where possible. + +## Plans and notes + +- We expect this directory to grow with many more languages, as well as connections between languages, logics, and other reasoning techniques. +- A recurring issue is how to handle binders. We still need to develop general facilities for this. Leveraging multiple representations of languages, we also plan on formally exploring the connection between standard pen & paper definitions and convenient formal representations, for example the relation between α-equivalence and techniques based on de Brujin indices. +- We aim at providing reusable infrastructure for defining languages and provably-correct compilers. +- Some topics that are often associated with languages also appear elsewhere in CSLib when a more general placement is preferrable. For example, automata and formal languages over words are in [Computability](../Computability), while reusable semantic infrastructure lives in [Foundations](../Foundations). diff --git a/Cslib/Logics/README.md b/Cslib/Logics/README.md new file mode 100644 index 000000000..5837889a0 --- /dev/null +++ b/Cslib/Logics/README.md @@ -0,0 +1,46 @@ +
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+ +# Logic + +CSLib offers **formal logics** for defining specifications and reasoning about programs and systems. Each subdirectory focuses on a specific logic or framework. + +Shared foundations can be found in [Foundations/Logic](../Foundations/Logic). + +## Principles + +### Operators + +Please instantiate and use the typeclasses for logical operators (connectives, modalities, etc.) found in [Foundations/Logic](../Foundations/Logic). + +### Inference system and logical equivalence + +We adopt a unified approach to proof systems and semantics, whereby they instantiate `InferenceSystem`. See [linear logic](LinearLogic) and [modal logic](Modal) for examples. + +When defining logical equivalence for a given inference system, instantiate `LogicalEquivalence`. This class also acts as a check that you use the correct APIs. + +### Proof relevance in proof systems + +A recurring choice when defining a proof system (like a sequent calculus) is whether they should go into `Prop` (proof irrelevance) or a `Type` (proof relevance). +The default choice is to use a `Type` -- at the appropriate universe level, polymorphic if it has type parameters. This makes it easy to define computations on derivations, e.g., to compute their height, display them, or make tools that show how they can be transformed. + +### Fragments + +To define a fragment of a proof system, you can use a predicate. See [MLL](LinearLogic/CLL/MLL.lean) for an example. + +### Notation for judgements + +To avoid notation clashes in the notation for judgements, use a wrapper tag that clearly describes the logic. For example, in modal logic this is `Modal[m,w ⊨ φ]`. + +## Plans and notes + +### Logical equivalence + +We plan on leveraging the common infrastructure of `InferenceSystem`, `LogicalEquivalence`, and similar to build common interfaces for manipulating proofs. +If any of these APIs do not suit your needs, we are interested in expanding them or creating new ones that can cover your use cases. + +### Notation + +We will explore alternative approaches to dealing with notation clashes. An example of a current shortcoming is the necessity of prefixing dynamic logic modalities with a `d`, because they use common notation such as `[...]`. One way of doing this could be to establish typeclasses/syntax also for judgemental notation, such as `m,w ⊨ φ`, and make it accessible within a tag like `Logic`, giving for example `Logic[m,w ⊨ φ]`. This would then scope the notation for propositions only to `φ`. diff --git a/ORGANISATION.md b/ORGANISATION.md index a2c4edfca..33e522ef9 100644 --- a/ORGANISATION.md +++ b/ORGANISATION.md @@ -1,6 +1,8 @@ # Code organisation -This document gives an overview of how the codebase is structured, in terms of directories. +This document gives an overview of how the codebase is structured, in terms of directories. + +For more details about the high-level principles that govern these directories, please refer to their internal `README.md` files when present. **Note** that this organisation is still under active discussion and is subject to change. From 4c4f2e3d424f6e44fb44547c33ab534bae212b17 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Date: Sat, 18 Jul 2026 02:19:32 +0100 Subject: [PATCH 31/36] chore: bump mathlib to d99d52c, fix breaking changes (#728) Bump `mathlib` dependency to [d99d52c](https://github.com/leanprover-community/mathlib4/commit/d99d52c36bea862ef9499bfaef386d0bcba9ea48): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Previously at: [79d0395](https://github.com/leanprover-community/mathlib4/commit/79d0395a1825a6264ad5d269e35e60537518955e): chore: bump toolchain to v4.33.0-rc1 (#41779) (2026-07-16) Closes #727 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29592162806/artifacts/8412435005) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`d99d52c`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/29610863999)._ --------- Co-authored-by: mathlib-nightly-testing[bot] Co-authored-by: Chris Henson --- Cslib/Computability/Automata/NA/Hist.lean | 2 +- Cslib/Foundations/Data/Nat/Segment.lean | 6 ++-- .../Data/OmegaSequence/Flatten.lean | 2 +- Cslib/Foundations/Data/Set/Saturation.lean | 2 +- .../LocallyNameless/Stlc/StrongNorm.lean | 3 +- .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 19 +++-------- Cslib/Logics/Modal/Basic.lean | 7 ++-- Cslib/Logics/Modal/Cube.lean | 8 ++--- Cslib/MachineLearning/PACLearning/Defs.lean | 4 +-- .../PACLearning/VersionSpace.lean | 33 +++---------------- lake-manifest.json | 8 ++--- lakefile.toml | 2 +- 12 files changed, 27 insertions(+), 69 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Hist.lean b/Cslib/Computability/Automata/NA/Hist.lean index ed2137efe..716b76f9f 100644 --- a/Cslib/Computability/Automata/NA/Hist.lean +++ b/Cslib/Computability/Automata/NA/Hist.lean @@ -57,7 +57,7 @@ theorem hist_run_exists {xs : ωSequence Symbol} {ss : ωSequence State} use ⟨fun n ↦ (ss n, makeHist start' tr' xs ss n)⟩ constructor · simp only [addHist] - grind only [Run, usr Set.mem_setOf_eq, = get_fun, = LTS.OmegaExecution, makeHist] + grind only [Run, usr Set.mem_ofPred_eq, = get_fun, = LTS.OmegaExecution, makeHist] · grind end Cslib.Automata.NA diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index 01ec8fae8..ebb139383 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -45,7 +45,7 @@ theorem infinite_strictMono {ns : Set ℕ} (h : ns.Infinite) : /-- There is a gap between two successive occurrences of a predicate `p : ℕ → Prop`, assuming `p` (as a set) is infinite. -/ -theorem nth_succ_gap {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) : +theorem nth_succ_gap {p : ℕ → Prop} (hf : (ofPred p).Infinite) (n : ℕ) : ∀ k < nth p (n + 1) - nth p n, k > 0 → ¬ p (k + nth p n) := by classical intro k h_k1 h_k0 h_p_k @@ -222,12 +222,12 @@ theorem segment'_eq_segment (hm : StrictMono f) : ({x ∈ Finset.range (k + 1) | x ∈ range f}) by grind [BijOn.finsetCard_eq, Finset.coe_filter] refine ⟨fun n ↦ n + f 0, ?_, ?_, ?_⟩ - · intro n; simp only [mem_range, Finset.mem_range, mem_setOf_eq] + · intro n; simp only [mem_range, Finset.mem_range] rintro ⟨h_n, i, rfl⟩ have := StrictMono.monotone hm <| zero_le i refine ⟨?_, i, ?_⟩ <;> omega · grind [injOn_of_injective, Injective] - · intro n; simp only [mem_range, Finset.mem_range, mem_setOf_eq, mem_image] + · intro n; simp only [mem_range, Finset.mem_range, mem_ofPred_eq, mem_image] rintro ⟨h_n, i, rfl⟩ have := StrictMono.monotone hm <| zero_le i grind diff --git a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean index 4d7a6f76c..0d69869e8 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean @@ -88,7 +88,7 @@ theorem cumLen_segment_one_add {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k) symm apply Set.BijOn.finsetCard_eq (fun n ↦ n + (ls 0).length) refine ⟨?_, by grind [injOn_of_injective, Injective], ?_⟩ <;> - ( intro k; simp only [Set.mem_range, Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq, + ( intro k; simp only [Set.mem_range, Finset.coe_filter, Finset.mem_range, Set.mem_ofPred_eq, le_add_iff_nonneg_left, _root_.zero_le, and_true] ) · rintro ⟨h_k, i, rfl⟩ refine ⟨?_, 1 + i, ?_⟩ <;> grind [cumLen_one_add_drop] diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean index 32e9806db..c502ef193 100644 --- a/Cslib/Foundations/Data/Set/Saturation.lean +++ b/Cslib/Foundations/Data/Set/Saturation.lean @@ -38,7 +38,7 @@ theorem saturates_compl (hs : Saturates f s) : Saturates f sᶜ := by theorem saturates_eq_biUnion (hs : Saturates f s) (hc : ⋃ i, f i = univ) : s = ⋃ i ∈ {i | (f i ∩ s).Nonempty}, f i := by ext x - simp only [mem_setOf_eq, mem_iUnion, exists_prop] + simp only [mem_iUnion] constructor · intro h_x obtain ⟨i, _⟩ := mem_iUnion.mp <| univ_subset_iff.mpr hc <| mem_univ x diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index cb858529d..b55058f31 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -58,7 +58,6 @@ def semanticMap : Ty Base → Set (Term Var) | .base _ => { t | SN FullBeta t ∧ LC t } | .arrow τ₁ τ₂ => { t | ∀ s, s ∈ semanticMap τ₁ → app t s ∈ semanticMap τ₂ } -set_option linter.tacticAnalysis.verifyGrindOnly false in /-- The sets constructed by semanticMap are saturated -/ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := by induction τ with @@ -67,7 +66,7 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := constructor · let x : Var := fresh {} have := ih₁.neutal_lc (fvar x) (.fvar x) (.fvar x) - grind only [semanticMap, usr Set.mem_setOf_eq, cases LC] + grind [cases LC] · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})] · grind · intro M N P _ _ _ s _ diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index fbb2fe840..c5233c24c 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -196,14 +196,8 @@ lemma coe_mk {X : Set P} {h : isFact X} : ((⟨X, h⟩ : Fact P) : Set P) = X := @[simp] lemma closed (F : Fact P) : isFact (F : Set P) := F.property /-- In any phase space, `{1}⫠ = ⊥`. -/ -lemma orth_one_eq_bot : - ({(1 : P)} : Set P)⫠ = (PhaseSpace.bot : Set P) := by - ext m; constructor - · intro hm - simpa [orthogonal, mem_setOf, mul_one] using hm 1 (by simp) - · intro hm x hx - rcases hx with rfl - simpa [orthogonal, mem_setOf, mul_one] using hm +lemma orth_one_eq_bot : ({(1 : P)} : Set P)⫠ = (PhaseSpace.bot : Set P) := by + simp_all /-- The fact given by the dual of G. -/ @[simps!] def dualFact (G : Set P) : Fact P := Fact.mkDual (G⫠) G rfl @@ -638,14 +632,9 @@ lemma par_semi_distrib_plus : ((G ⅋ H) ⊕ (G ⅋ K) : Fact P) ≤ G ⅋ (H @[simp] lemma top_par : (⊤ ⅋ G : Fact P) = ⊤ := by refine SetLike.coe_injective ?_ - rw [coe_top] - rw [Set.eq_univ_iff_forall] - intro x - simp only [parr, dualFact, mkDual, mkSubset, coe_mk, coe_top] - rw [PhaseSpace.orthogonal_def, Set.mem_setOf_eq] - intro w hw + rw [coe_top, Set.eq_univ_iff_forall] + intro x w hw rcases Set.mem_mul.mp hw with ⟨y, hy, z, hz, rfl⟩ - rw [PhaseSpace.orthogonal_def, Set.mem_setOf_eq] at hy rw [mul_left_comm] exact hy (x * z) (Set.mem_univ _) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index cefa5bece..abb22afba 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -208,11 +208,8 @@ theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → /-- 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, - -- = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true] + grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_ofPred_eq, = impl_iff_impl, + =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall] /-- 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/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean index 98e825014..8c5e57960 100644 --- a/Cslib/Logics/Modal/Cube.lean +++ b/Cslib/Logics/Modal/Cube.lean @@ -97,16 +97,16 @@ open scoped Proposition open Set theorem k_subset_d : K World Atom ⊆ D World Atom := by - grind only [subset_def, D, K, = setOf_true, = logic, mem_setOf_eq, = Proposition.valid] + grind only [subset_def, D, K, = ofPred_true, = logic, mem_ofPred_eq, = Proposition.valid] theorem k_subset_b : K World Atom ⊆ B World Atom := by - grind only [subset_def, B, K, = setOf_true, = logic, mem_setOf_eq, = Proposition.valid] + grind only [subset_def, B, K, = ofPred_true, = logic, mem_ofPred_eq, = Proposition.valid] theorem k_subset_four : K World Atom ⊆ Four World Atom := by - grind only [subset_def, Four, K, = setOf_true, = logic, mem_setOf_eq, = Proposition.valid] + grind only [subset_def, Four, K, = ofPred_true, = logic, mem_ofPred_eq, = Proposition.valid] theorem k_subset_five : K World Atom ⊆ Five World Atom := by - grind only [subset_def, Five, K, = setOf_true, = logic, mem_setOf_eq, = Proposition.valid] + grind only [subset_def, Five, K, = ofPred_true, = logic, mem_ofPred_eq, = Proposition.valid] open scoped Relation in theorem d_subset_t : D World Atom ⊆ T World Atom := by diff --git a/Cslib/MachineLearning/PACLearning/Defs.lean b/Cslib/MachineLearning/PACLearning/Defs.lean index 084079f4b..2bbb32303 100644 --- a/Cslib/MachineLearning/PACLearning/Defs.lean +++ b/Cslib/MachineLearning/PACLearning/Defs.lean @@ -516,9 +516,7 @@ theorem error_map_eq_hypothesisError (P : Measure α) (h c : Set α) (measurable_to_bool (by convert hc using 1; ext x; simp [decide_eq_true_eq])) rw [Measure.map_apply_of_aemeasurable hf.aemeasurable] · congr 1; ext x - simp only [Set.mem_preimage, Set.mem_setOf_eq, symmDiff_def, sup_eq_union, - Set.mem_union, Set.mem_sdiff] - by_cases hx : x ∈ h <;> by_cases hcx : x ∈ c <;> simp_all + by_cases hx : x ∈ h <;> simp_all [symmDiff_def] · convert (hh.prod (measurableSet_singleton false)).union (hh.compl.prod (measurableSet_singleton true)) using 1 ext ⟨x, b⟩; cases b <;> simp diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index 37f8072cf..5d5f1d178 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -153,31 +153,8 @@ theorem mem_versionSpace_iff_empiricalError_zero unfold empiricalError empiricalMeasure error rcases Nat.eq_zero_or_pos m with hm | hm · subst hm - rw [dif_pos rfl] - simp only [Measure.coe_zero, Pi.zero_apply] - exact iff_of_true (fun i => i.elim0) trivial - · have hm_ne : m ≠ 0 := Nat.pos_iff_ne_zero.mp hm - have hm_inv_ne : (m : ℝ≥0∞)⁻¹ ≠ 0 := - ENNReal.inv_ne_zero.mpr (ENNReal.natCast_ne_top m) - rw [dif_neg hm_ne, Measure.smul_apply, Measure.finsetSum_apply] - simp only [Measure.dirac_apply, Set.indicator, Set.mem_setOf_eq, Pi.one_apply, - smul_eq_mul] - rw [mul_eq_zero] - constructor - · intro hh - right - apply Finset.sum_eq_zero - intro i _ - rw [if_neg] - intro hne - exact hne (hh i) - · rintro (h1 | h2) - · exact absurd h1 hm_inv_ne - · intro i - have hi := (Finset.sum_eq_zero_iff.mp h2) i (Finset.mem_univ i) - by_contra hne - rw [if_pos hne] at hi - exact one_ne_zero hi + simp_all + · simp_all [Nat.pos_iff_ne_zero] /-- The empirical 0-1 error equals the empirical miscount divided by the sample size. -/ @@ -189,8 +166,7 @@ theorem empiricalError_eq_div [DecidableEq β] have hm_ne : m ≠ 0 := hm.ne' unfold empiricalError empiricalMeasure error empiricalMiscount rw [dif_neg hm_ne, Measure.smul_apply, Measure.finsetSum_apply] - simp only [Measure.dirac_apply, Set.indicator, Set.mem_setOf_eq, Pi.one_apply, - smul_eq_mul] + simp only [Measure.dirac_apply, Set.indicator, Set.mem_ofPred_eq, Pi.one_apply, smul_eq_mul] rw [Finset.sum_boole, ← ENNReal.div_eq_inv_mul] /-! ### Consistent Learners -/ @@ -299,8 +275,7 @@ theorem ae_mem_versionSpace_of_realizable have hsub : {S : Fin m → α × β | ¬ c ∈ VersionSpace C S} ⊆ (Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ := by intro S hS hcontra - simp only [Set.mem_pi, Set.mem_univ, true_implies, Set.mem_setOf_eq] at hcontra - exact hS ⟨hc, fun i => (hcontra i).symm⟩ + exact hS ⟨hc, by simp_all⟩ have hcompl : (Measure.pi (fun _ : Fin m => P.map (fun x : α => (x, c x)))) ((Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1}))ᶜ) = 0 := by rw [prob_compl_eq_one_sub (MeasurableSet.univ_pi fun _ => hG), diff --git a/lake-manifest.json b/lake-manifest.json index 30ae49d4f..8fd55030d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79d0395a1825a6264ad5d269e35e60537518955e", + "rev": "d99d52c36bea862ef9499bfaef386d0bcba9ea48", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "79d0395a1825a6264ad5d269e35e60537518955e", + "inputRev": "d99d52c36bea862ef9499bfaef386d0bcba9ea48", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "31a49105f960721073a9adfc82b261f5d0f2ce1e", + "rev": "45337c634fbcb2bb22fb45c9847faaa10d4d1b67", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 90255cbb4..c21fc9f16 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "79d0395a1825a6264ad5d269e35e60537518955e" +rev = "d99d52c36bea862ef9499bfaef386d0bcba9ea48" [[lean_lib]] name = "Cslib" From bb3fc4c45275e4fd15314808a52cd6bd682e78b0 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Sun, 19 Jul 2026 06:20:17 +0200 Subject: [PATCH 32/36] chore: fix (all) `backward.isDefEq.respectTransparency` exceptions (#729) --- Cslib/Computability/Languages/OmegaRegularLanguage.lean | 6 ++---- Cslib/Computability/Languages/RegularLanguage.lean | 2 -- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 75e89deff..644d181d1 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -190,8 +190,6 @@ theorem IsRegular.omegaPow [Inhabited Symbol] {l : Language Symbol} use Unit ⊕ State, inferInstance, ⟨na.loop, {inl ()}⟩ exact NA.Buchi.loop_language_eq --- TODO: fix proof to work with backward.isDefEq.respectTransparency -set_option backward.isDefEq.respectTransparency false in /-- An ω-language is regular iff it is the finite union of ω-languages of the form `L * M^ω`, where all `L`s and `M`s are regular languages. -/ theorem IsRegular.eq_fin_iSup_hmul_omegaPow [Inhabited Symbol] (p : ωLanguage Symbol) : @@ -214,8 +212,8 @@ theorem IsRegular.eq_fin_iSup_hmul_omegaPow [Inhabited Symbol] (p : ωLanguage S refine ⟨?_, by grind⟩ rintro ⟨s, h_s, t, h_t, h_mem⟩ use eq.invFun (⟨s, h_s⟩, ⟨t, h_t⟩) - -- The following `simp` is where the `set_option` above is needed. - simpa [mem_def] + have := Equiv.apply_symm_apply eq + simp_all · rintro ⟨n, l, m, _, rfl⟩ rw [← iSup_univ] apply IsRegular.iSup diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index 745696183..f97e124b8 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -167,8 +167,6 @@ theorem IsRegular.mul {l1 l2 : Language Symbol} ⟨finConcat nfa1 nfa2, inr '' (some '' nfa2.accept)⟩ exact finConcat_language_eq --- TODO: fix proof to work with backward.isDefEq.respectTransparency -set_option backward.isDefEq.respectTransparency false in open NA.FinAcc Sum in /-- The Kleene star of a regular language is regular. -/ @[simp] From 549d50c7b59fdd6c2ffcead98dfb5257b684101f Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Date: Mon, 20 Jul 2026 21:03:41 +0000 Subject: [PATCH 33/36] chore: bump mathlib to 169c26b, fix breaking changes (#733) Bump `mathlib` dependency to [169c26b](https://github.com/leanprover-community/mathlib4/commit/169c26b52a38b704fad2c009372d76844a059bdf): refactor: rename restrict to domRestrict (#25980) (2026-07-20) Previously at: [d99d52c](https://github.com/leanprover-community/mathlib4/commit/d99d52c36bea862ef9499bfaef386d0bcba9ea48): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Closes #732 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29755881109/artifacts/8467297013) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`169c26b`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/29776447755)._ --------- Co-authored-by: mathlib-nightly-testing[bot] Co-authored-by: Chris Henson --- Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean | 6 ++---- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- 3 files changed, 6 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean index 17f1bb30f..6d0712db9 100644 --- a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean +++ b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean @@ -29,12 +29,10 @@ open Function Set theorem infinite_pigeonhole_principle {X Y : Type*} [Finite Y] (f : X → Y) {s : Set X} (h_inf : s.Infinite) : ∃ y, ∃ t, t.Infinite ∧ t ⊆ s ∧ ∀ x ∈ t, f x = y := by have := h_inf.to_subtype - obtain ⟨y, h_inf'⟩ := Finite.exists_infinite_fiber (s.restrict f) + obtain ⟨y, h_inf'⟩ := Finite.exists_infinite_fiber (s.domRestrict f) have h_inf_iff := Equiv.infinite_iff <| Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ s) (fun x ↦ f x = y) - simp only [coe_eq_subtype, mem_preimage, restrict_apply, mem_singleton_iff, h_inf_iff] at h_inf' - have h_inf'' := (infinite_coe_iff (s := { x | x ∈ s ∧ f x = y })).mp h_inf' - use y, {x | x ∈ s ∧ f x = y} + use y, {x | x ∈ s ∧ f x = y}, infinite_coe_iff.mp <| h_inf_iff.mp h_inf' grind /-- An `InfVSet` consists of a set of vertices and a proof that the set is infinite. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 8fd55030d..7f68c0042 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d99d52c36bea862ef9499bfaef386d0bcba9ea48", + "rev": "169c26b52a38b704fad2c009372d76844a059bdf", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "d99d52c36bea862ef9499bfaef386d0bcba9ea48", + "inputRev": "169c26b52a38b704fad2c009372d76844a059bdf", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "45337c634fbcb2bb22fb45c9847faaa10d4d1b67", + "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index c21fc9f16..a1fe432a2 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "d99d52c36bea862ef9499bfaef386d0bcba9ea48" +rev = "169c26b52a38b704fad2c009372d76844a059bdf" [[lean_lib]] name = "Cslib" From b5a1ef69c2de76d398ce1f429a574b6dd0839d57 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 22 Jul 2026 14:16:47 +0200 Subject: [PATCH 34/36] fix grind? issue --- Cslib/Logics/Modal/Basic.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index abb22afba..fb172c8fa 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -208,8 +208,10 @@ theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → /-- The dual axiom, valid for all models. -/ theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by - grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_ofPred_eq, = impl_iff_impl, - =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall] + simp only [Satisfies.iff_iff_iff] + constructor + · grind + · grind only [= not_iff_not, = diamond_iff_exists, = box_iff_forall] /-- The T axiom, valid for all reflexive models. -/ theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World} From 8cbaec9789f33304c1026cd78fac37c1d95a3a9d Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 22 Jul 2026 14:23:44 +0200 Subject: [PATCH 35/36] instance refactor --- Cslib/Logics/Modal/Basic.lean | 14 +++++++------- Cslib/Logics/Propositional/Defs.lean | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index fb172c8fa..a53f69f5e 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -47,9 +47,9 @@ inductive Proposition (Atom : Type u) : Type u where /-- Possibility. -/ | diamond (φ : Proposition Atom) -instance : HasNot (Proposition Atom) := {not := Proposition.not} -instance : HasAnd (Proposition Atom) := {and := Proposition.and} -instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} +instance : HasNot (Proposition Atom) := ⟨.not⟩ +instance : HasAnd (Proposition Atom) := ⟨.and⟩ +instance : HasDiamond (Proposition Atom) := ⟨.diamond⟩ @[scoped grind =] lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl @@ -63,7 +63,7 @@ lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := /-- Disjunction. -/ def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) -instance : HasOr (Proposition Atom) := {or := Proposition.or} +instance : HasOr (Proposition Atom) := ⟨Proposition.or⟩ @[scoped grind =] lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl @@ -71,7 +71,7 @@ lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ /-- Implication. -/ def Proposition.imp (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ -instance : HasImp (Proposition Atom) := {imp := Proposition.imp} +instance : HasImp (Proposition Atom) := ⟨.imp⟩ @[scoped grind =] lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl @@ -79,7 +79,7 @@ lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = ( /-- Bi-implication. -/ def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -instance : HasIff (Proposition Atom) := {iff := Proposition.iff} +instance : HasIff (Proposition Atom) := ⟨.iff⟩ @[scoped grind =] lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) : @@ -88,7 +88,7 @@ lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) : /-- Necessity. -/ def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ -instance : HasBox (Proposition Atom) := {box := Proposition.box} +instance : HasBox (Proposition Atom) := ⟨.box⟩ @[scoped grind =] lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index cea4c2362..a68d4c53a 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -70,10 +70,10 @@ instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.imp ⊥ ⊥ := rfl -instance : HasAnd (Proposition Atom) := {and := Proposition.and} -instance : HasOr (Proposition Atom) := {or := Proposition.or} -instance : HasImp (Proposition Atom) := {imp := Proposition.imp} -instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg} +instance : HasAnd (Proposition Atom) := ⟨.and⟩ +instance : HasOr (Proposition Atom) := ⟨.or⟩ +instance : HasImp (Proposition Atom) := ⟨.imp⟩ +instance [Bot Atom] : HasNot (Proposition Atom) := ⟨.neg⟩ omit [DecidableEq Atom] in @[grind =] From 552d40e17027bf069a629d057e41449bd9a56e4e Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 22 Jul 2026 14:52:12 +0200 Subject: [PATCH 36/36] dynamic syntax docstring fix --- Cslib/Foundations/Logic/Operators.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index 6ae461927..fc9f3bb2a 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -88,14 +88,14 @@ Here we need to use the prefix `d` to distinguish our notation from the normal ` A refactoring that makes this unnecessary would be welcome. -/ -/-- The type `α` has a dynamic box modality with action type `β` (`[a]φ`). -/ +/-- The type `α` has a dynamic box modality with action type `β` (`d[a]φ`). -/ class HasDynamicBox (α β : Type*) where /-- `b` is necessarily valid after `a`. -/ dynBox (a : β) (b : α) : α @[inherit_doc] scoped notation "d[" a "]" φ => HasDynamicBox.dynBox a φ -/-- The type `α` has a dynamic diamond modality with action type `β` (`[a]φ`). -/ +/-- The type `α` has a dynamic diamond modality with action type `β` (`d⟨a⟩φ`). -/ class HasDynamicDiamond (α β : Type*) where /-- `b` is possibly valid after `a`. -/ dynDiamond (a : β) (b : α) : α