From 4ab77e088df40d5acbfcb757b1ceb83224c12c2a Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 30 Mar 2026 12:33:45 +0200 Subject: [PATCH 01/18] feat: Heterogeneous behavioural equivalences (#460) Generalises current behavioural equivalences (bisimulation and weak variants, simulation, and trace equivalence) to states in different LTSs, rather than assuming that the states being compared are in the same LTS. The convenience of homogeneous relations is retained via abbreviations (e.g., `HomBisimilarity`) and backwards-compatible notation. The aim of this PR is to facilitate proving the correctness of compilers, where states usually are in different languages. --- Cslib/Foundations/Data/Relation.lean | 4 + .../Semantics/LTS/Bisimulation.lean | 628 +++++++++--------- .../Foundations/Semantics/LTS/Simulation.lean | 135 ++-- Cslib/Foundations/Semantics/LTS/TraceEq.lean | 104 +-- Cslib/Languages/CCS/BehaviouralTheory.lean | 10 +- Cslib/Logics/HML/Basic.lean | 10 +- CslibTests/Bisimulation.lean | 2 +- CslibTests/HML.lean | 2 +- CslibTests/LTS.lean | 2 +- 9 files changed, 476 insertions(+), 421 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index ed3f7e76ae..22a3d67874 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -33,6 +33,10 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou namespace Relation +/-- The empty (heterogeneous) relation, which always returns `False`. -/ +@[nolint unusedArguments] +def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False + attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := by diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index d41eafe71b..f048e19747 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -15,9 +15,9 @@ public import Cslib.Foundations.Semantics.LTS.TraceEq /-! # Bisimulation and Bisimilarity -A bisimulation is a binary relation on the states of an `LTS`, which establishes a tight semantic -correspondence. More specifically, if two states `s1` and `s2` are related by a bisimulation, then -`s1` can mimic all transitions of `s2` and vice versa. Furthermore, the derivatives reaches through +A bisimulation is a binary relation on the states of two `LTS`s, which establishes a tight semantic +correspondence. More specifically, if two states `s₁` and `s₂` are related by a bisimulation, then +`s₁` can mimic all transitions of `s₂` and vice versa. Furthermore, the derivatives reaches through these transitions remain related by the bisimulation. Bisimilarity is the largest bisimulation: given an `LTS`, it relates any two states that are related @@ -45,8 +45,8 @@ we prove to be sound and complete. ## Notations -- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the LTS `lts`. -- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the LTS `lts`. +- `s₁ ~[lts] s₂`: the states `s₁` and `s₂` are bisimilar in the LTS `lts`. +- `s₁ ≈[lts] s₂`: the states `s₁` and `s₂` are weakly bisimilar in the LTS `lts`. ## Main statements @@ -68,115 +68,119 @@ equivalence coincide. namespace Cslib.LTS -universe u v - section Bisimulation -variable {State : Type u} {Label : Type v} {lts : LTS State Label} - -/-- A relation is a bisimulation if, whenever it relates two states in an lts, +/-- A relation is a bisimulation if, whenever it relates two states, the transitions originating from these states mimic each other and the reached derivatives are themselves related. -/ @[scoped grind =] -def IsBisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2') +def IsBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂') ) +/-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ +abbrev IsHomBisimulation (lts : LTS State Label) := IsBisimulation lts lts + /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_fst - (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') : - ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (htr : lts₁.Tr s₁ μ s₁') : + ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂' := (hb hr μ).1 _ htr /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_snd - (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') : - ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (htr : lts₂.Tr s₂ μ s₂') : + ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂' := (hb hr μ).2 _ htr /-- Two states are bisimilar if they are related by some bisimulation. -/ @[scoped grind =] -def Bisimilarity (lts : LTS State Label) : State → State → Prop := - fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsBisimulation r +def Bisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := + fun s₁ s₂ => ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsBisimulation lts₁ lts₂ r /-- Notation for bisimilarity. -Differently from standard pen-and-paper presentations, we require the lts to be mentioned +Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly. -/ -notation s:max " ~[" lts "] " s':max => Bisimilarity lts s s' +scoped notation s:max " ~[" lts₁ "," lts₂ "] " s':max => Bisimilarity lts₁ lts₂ s s' -open LTS in -/-- Bisimilarity is reflexive. -/ +/-- Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same. -/ +abbrev HomBisimilarity (lts : LTS State Label) := Bisimilarity lts lts + +/-- Notation for homogeneous bisimilarity. -/ +scoped notation s:max " ~[" lts "] " s':max => HomBisimilarity lts s s' + +/-- Homogeneous bisimilarity is reflexive. -/ @[scoped grind ., refl] -theorem Bisimilarity.refl (s : State) : s ~[lts] s := by +theorem HomBisimilarity.refl (s : State) : s ~[lts] s := by exists Eq grind /-- The inverse of a bisimulation is a bisimulation. -/ @[scoped grind →] -theorem IsBisimulation.inv (h : lts.IsBisimulation r) : - lts.IsBisimulation (flip r) := by grind [flip] +theorem IsBisimulation.inv (h : IsBisimulation lts₁ lts₂ r) : + IsBisimulation lts₂ lts₁ (flip r) := by grind [flip] open scoped IsBisimulation in /-- Bisimilarity is symmetric. -/ @[scoped grind →, symm] -theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := by +theorem Bisimilarity.symm {s₁ s₂ : State} (h : s₁ ~[lts₁,lts₂] s₂) : s₂ ~[lts₂,lts₁] s₁ := by grind [flip] /-- The composition of two bisimulations is a bisimulation. -/ @[scoped grind .] theorem IsBisimulation.comp - (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) : - lts.IsBisimulation (Relation.Comp r1 r2) := by grind [Relation.Comp] + (h1 : IsBisimulation lts₁ lts₂ r1) (h2 : IsBisimulation lts₂ lts₃ r2) : + IsBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by grind [Relation.Comp] -open LTS in /-- Bisimilarity is transitive. -/ @[scoped grind →] theorem Bisimilarity.trans - (h1 : s1 ~[lts] s2) (h2 : s2 ~[lts] s3) : - s1 ~[lts] s3 := by + (h1 : s₁ ~[lts₁,lts₂] s₂) (h2 : s₂ ~[lts₂,lts₃] s₃) : + s₁ ~[lts₁,lts₃] s₃ := by obtain ⟨r1, _, _⟩ := h1 obtain ⟨r2, _, _⟩ := h2 exists Relation.Comp r1 r2 grind [Relation.Comp] -/-- Bisimilarity is an equivalence relation. -/ -theorem Bisimilarity.eqv : - Equivalence (Bisimilarity lts) := { - refl := Bisimilarity.refl +/-- Homogeneous bisimilarity is an equivalence relation. -/ +theorem HomBisimilarity.eqv : + Equivalence (HomBisimilarity lts) := { + refl := HomBisimilarity.refl symm := Bisimilarity.symm trans := Bisimilarity.trans } -instance : IsEquiv State (Bisimilarity lts) where - refl := Bisimilarity.refl +instance : IsEquiv State (HomBisimilarity lts) where + refl := HomBisimilarity.refl symm _ _ := Bisimilarity.symm trans _ _ _ := Bisimilarity.trans /-- The union of two bisimulations is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.union (hrb : lts.IsBisimulation r) (hsb : lts.IsBisimulation s) : - lts.IsBisimulation (r ⊔ s) := by - intro s1 s2 hrs μ +theorem IsBisimulation.sup (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) : + IsBisimulation lts₁ lts₂ (r ⊔ s) := by + intro s₁ s₂ hrs μ cases hrs case inl h => constructor - · intro s1' htr - obtain ⟨s2', htr', hr'⟩ := hrb.follow_fst h htr - exists s2' + · intro s₁' htr + obtain ⟨s₂', htr', hr'⟩ := hrb.follow_fst h htr + exists s₂' constructor · assumption · simp only [max, SemilatticeSup.sup] left exact hr' - · intro s2' htr - obtain ⟨s1', htr', hr'⟩ := hrb.follow_snd h htr - exists s1' + · intro s₂' htr + obtain ⟨s₁', htr', hr'⟩ := hrb.follow_snd h htr + exists s₁' constructor · assumption · simp only [max, SemilatticeSup.sup] @@ -184,99 +188,104 @@ theorem Bisimulation.union (hrb : lts.IsBisimulation r) (hsb : lts.IsBisimulatio exact hr' case inr h => constructor - · intro s1' htr - obtain ⟨s2', htr', hs'⟩ := hsb.follow_fst h htr - exists s2' + · intro s₁' htr + obtain ⟨s₂', htr', hs'⟩ := hsb.follow_fst h htr + exists s₂' constructor · assumption · simp only [max, SemilatticeSup.sup] right exact hs' - · intro s2' htr - obtain ⟨s1', htr', hs'⟩ := hsb.follow_snd h htr - exists s1' + · intro s₂' htr + obtain ⟨s₁', htr', hs'⟩ := hsb.follow_snd h htr + exists s₁' constructor · assumption · simp only [max, SemilatticeSup.sup] right exact hs' -open LTS in /-- Bisimilarity is a bisimulation. -/ @[scoped grind .] -theorem Bisimilarity.is_bisimulation : lts.IsBisimulation (Bisimilarity lts) := by grind +theorem Bisimilarity.is_bisimulation : IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind /-- Bisimilarity is the largest bisimulation. -/ @[scoped grind →] -theorem Bisimilarity.largest_bisimulation (h : lts.IsBisimulation r) : - Subrelation r (Bisimilarity lts) := by - intro s1 s2 hr +theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ r) : + Subrelation r (Bisimilarity lts₁ lts₂) := by + intro s₁ s₂ hr exists r /-- The union of bisimilarity with any bisimulation is bisimilarity. -/ @[scoped grind =, simp] -theorem Bisimilarity.gfp (r : State → State → Prop) (h : lts.IsBisimulation r) : - (Bisimilarity lts) ⊔ r = Bisimilarity lts := by - funext s1 s2 - simp only [max, SemilatticeSup.sup, eq_iff_iff, or_iff_left_iff_imp] - apply Bisimilarity.largest_bisimulation h +theorem Bisimilarity.gfp (r : State₁ → State₂ → Prop) (h : IsBisimulation lts₁ lts₂ r) : + (Bisimilarity lts₁ lts₂) ⊔ r = Bisimilarity lts₁ lts₂ := by + funext s₁ s₂ + simp only [max, SemilatticeSup.sup] + grind /-- `calc` support for bisimilarity. -/ -instance : Trans (Bisimilarity lts) (Bisimilarity lts) (Bisimilarity lts) where +instance : Trans (Bisimilarity lts₁ lts₂) (Bisimilarity lts₂ lts₃) (Bisimilarity lts₁ lts₃) where trans := Bisimilarity.trans section Order /-! ## Order properties -/ -instance : Max {r // lts.IsBisimulation r} where - max r s := ⟨r.1 ⊔ s.1, Bisimulation.union r.2 s.2⟩ +instance : Max {r // IsBisimulation lts₁ lts₂ r} where + max r s := ⟨r.1 ⊔ s.1, IsBisimulation.sup r.2 s.2⟩ /-- Bisimulations equipped with union form a join-semilattice. -/ -instance : SemilatticeSup {r // lts.IsBisimulation r} where +instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where sup r s := r ⊔ s le_sup_left r s := by simp only [LE.le] - intro s1 s2 hr + intro s₁ s₂ hr simp only [max, SemilatticeSup.sup] left exact hr le_sup_right r s := by simp only [LE.le] - intro s1 s2 hs + intro s₁ s₂ hs simp only [max, SemilatticeSup.sup] right exact hs sup_le r s t := by intro h1 h2 simp only [LE.le, max, SemilatticeSup.sup] - intro s1 s2 h + intro s₁ s₂ h cases h case inl h => apply h1 _ _ h case inr h => apply h2 _ _ h -/-- The empty relation is a bisimulation. -/ +/-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.emptyRelation_bisimulation : lts.IsBisimulation emptyRelation := by - intro s1 s2 hr +theorem IsBisimulation.bot : IsBisimulation lts₁ lts₂ Relation.emptyHRelation := by + intro s₁ s₂ hr cases hr +instance : Bot {r // IsBisimulation lts₁ lts₂ r} := + ⟨Relation.emptyHRelation, IsBisimulation.bot⟩ + +instance : Top {r // IsBisimulation lts₁ lts₂ r} := + ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ + /-- In the inclusion order on bisimulations: - The empty relation is the bottom element. - Bisimilarity is the top element. -/ -instance : BoundedOrder {r // lts.IsBisimulation r} where - top := ⟨Bisimilarity lts, Bisimilarity.is_bisimulation⟩ - bot := ⟨emptyRelation, Bisimulation.emptyRelation_bisimulation⟩ +instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where + top := ⊤ + bot := ⊥ le_top r := by - intro s1 s2 - simp only [LE.le] - apply Bisimilarity.largest_bisimulation r.2 + intro s₁ s₂ + simp only [LE.le, Top.top] + grind bot_le r := by - intro s1 s2 + intro s₁ s₂ simp only [LE.le] intro hr cases hr @@ -285,92 +294,100 @@ end Order /-! ## Bisimulation up-to -/ -/-- A relation `r` is a bisimulation up to bisimilarity if, whenever it relates two +/-- Lifts a relation `r` to homogeneous bisimilarities on its types. -/ +def UpToHomBisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : State₁ → State₂ → Prop := + Relation.Comp (HomBisimilarity lts₁) (Relation.Comp r (HomBisimilarity lts₂)) + +/-- A relation `r` is a bisimulation up to homogeneous bisimilarity if, whenever it relates two states in an lts, the transitions originating from these states mimic each other and the reached derivatives are themselves related by `r` up to bisimilarity. -/ @[scoped grind] -def IsBisimulationUpTo (lts : LTS State Label) (r : State → State → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2') +def IsBisimulationUpTo (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s₁' s₂') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s₁' s₂') ) /-- Any bisimulation up to bisimilarity is a bisimulation. -/ @[scoped grind →] -theorem IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) : - lts.IsBisimulation (Relation.UpTo r (Bisimilarity lts)) := by - intro s1 s2 hr μ - rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩ +theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ r) : + IsBisimulation lts₁ lts₂ (UpToHomBisimilarity lts₁ lts₂ r) := by + intro s₁ s₂ hr μ + rcases hr with ⟨s₁b, hr1b, s₂b, hrb, hr2b⟩ obtain ⟨r1, hr1, hr1b⟩ := hr1b obtain ⟨r2, hr2, hr2b⟩ := hr2b constructor case left => - intro s1' htr1 - obtain ⟨s1b', hs1b'tr, hs1b'r⟩ := (hr1b hr1 μ).1 s1' htr1 - obtain ⟨s2b', hs2b'tr, hs2b'r⟩ := (h hrb μ).1 s1b' hs1b'tr - obtain ⟨s2', hs2btr, hs2br⟩ := (hr2b hr2 μ).1 _ hs2b'tr - exists s2' + intro s₁' htr1 + obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := (hr1b hr1 μ).1 s₁' htr1 + obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (h hrb μ).1 s₁b' hs₁b'tr + obtain ⟨s₂', hs₂btr, hs₂br⟩ := (hr2b hr2 μ).1 _ hs₂b'tr + exists s₂' constructor case left => - exact hs2btr + exact hs₂btr case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs2b'r + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r constructor constructor - · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b hs1b'r) + · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b hs₁b'r) hsmidb · exists smid2 constructor · exact hsmidr · apply Bisimilarity.trans hsmidrb - apply Bisimilarity.largest_bisimulation hr2b hs2br + apply Bisimilarity.largest_bisimulation hr2b hs₂br case right => - intro s2' htr2 - obtain ⟨s2b', hs2b'tr, hs2b'r⟩ := (hr2b hr2 μ).2 s2' htr2 - obtain ⟨s1b', hs1b'tr, hs1b'r⟩ := (h hrb μ).2 s2b' hs2b'tr - obtain ⟨s1', hs1btr, hs1br⟩ := (hr1b hr1 μ).2 _ hs1b'tr - exists s1' + intro s₂' htr2 + obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (hr2b hr2 μ).2 s₂' htr2 + obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := (h hrb μ).2 s₂b' hs₂b'tr + obtain ⟨s₁', hs₁btr, hs₁br⟩ := (hr1b hr1 μ).2 _ hs₁b'tr + exists s₁' constructor case left => - exact hs1btr + exact hs₁btr case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs1b'r + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r constructor constructor · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b _) hsmidb - · exact hs1br + · exact hs₁br · exists smid2 constructor · exact hsmidr · apply Bisimilarity.trans hsmidrb apply Bisimilarity.largest_bisimulation hr2b _ - exact hs2b'r + exact hs₂b'r /-- If two states are related by a bisimulation, they can mimic each other's multi-step transitions. -/ -theorem Bisimulation.bisim_trace - (hb : lts.IsBisimulation r) (hr : r s1 s2) : - ∀ μs s1', lts.MTr s1 μs s1' → ∃ s2', lts.MTr s2 μs s2' ∧ r s1' s2' := by +theorem IsBisimulation.bisim_trace + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) : + ∀ μs s₁', lts₁.MTr s₁ μs s₁' → ∃ s₂', lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂' := by intro μs - induction μs generalizing s1 s2 + induction μs generalizing s₁ s₂ case nil => - intro s1' hmtr1 - exists s2 + intro s₁' hmtr1 + exists s₂ cases hmtr1 constructor constructor exact hr case cons μ μs' ih => - intro s1' hmtr1 + intro s₁' hmtr1 cases hmtr1 - case stepL s1'' htr hmtr => + case stepL s₁'' htr hmtr => specialize hb hr μ - have hf := hb.1 s1'' htr - obtain ⟨s2'', htr2, hb2⟩ := hf - specialize ih hb2 s1' hmtr - obtain ⟨s2', hmtr2, hr'⟩ := ih - exists s2' + have hf := hb.1 s₁'' htr + obtain ⟨s₂'', htr2, hb2⟩ := hf + specialize ih hb2 s₁' hmtr + obtain ⟨s₂', hmtr2, hr'⟩ := ih + exists s₂' constructor case left => constructor @@ -384,28 +401,28 @@ theorem Bisimulation.bisim_trace /-- Any bisimulation implies trace equivalence. -/ @[scoped grind =>] theorem IsBisimulation.traceEq - (hb : lts.IsBisimulation r) (hr : r s1 s2) : - s1 ~tr[lts] s2 := by + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) : + s₁ ~tr[lts₁,lts₂] s₂ := by funext μs simp only [eq_iff_iff] constructor case mp => intro h - obtain ⟨s1', h⟩ := h - obtain ⟨s2', hmtr⟩ := Bisimulation.bisim_trace hb hr μs s1' h - exists s2' + obtain ⟨s₁', h⟩ := h + obtain ⟨s₂', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s₁' h + exists s₂' exact hmtr.1 case mpr => intro h - obtain ⟨s2', h⟩ := h - obtain ⟨s1', hmtr⟩ := Bisimulation.bisim_trace hb.inv hr μs s2' h - exists s1' + obtain ⟨s₂', h⟩ := h + obtain ⟨s₁', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s₂' h + exists s₁' exact hmtr.1 /-- Bisimilarity is included in trace equivalence. -/ @[scoped grind .] -theorem Bisimilarity.le_traceEq : Bisimilarity lts ≤ TraceEq lts := by - intro s1 s2 h +theorem Bisimilarity.le_traceEq : Bisimilarity lts₁ lts₂ ≤ TraceEq lts₁ lts₂ := by + intro s₁ s₂ h obtain ⟨r, hr, hb⟩ := h apply hb.traceEq hr @@ -424,9 +441,9 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where /-- In general, trace equivalence is not a bisimulation (extra conditions are needed, see for example `Bisimulation.deterministic_trace_eq_is_bisim`). -/ -theorem Bisimulation.traceEq_not_bisim : +theorem IsBisimulation.traceEq_not_bisim : ∃ (State : Type) (Label : Type) (lts : LTS State Label), - ¬(lts.IsBisimulation (TraceEq lts)) := by + ¬(IsHomBisimulation lts (HomTraceEq lts)) := by exists ℕ exists Char let lts := LTS.mk BisimMotTr @@ -435,7 +452,7 @@ theorem Bisimulation.traceEq_not_bisim : -- specialize h 1 5 have htreq : (1 ~tr[lts] 5) := by simp [TraceEq] - have htraces1 : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by + have htraces₁ : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -484,7 +501,7 @@ theorem Bisimulation.traceEq_not_bisim : · apply BisimMotTr.one2two · apply MTr.single apply BisimMotTr.two2four - have htraces2 : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by + have htraces₂ : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -545,16 +562,16 @@ theorem Bisimulation.traceEq_not_bisim : · apply BisimMotTr.five2eight · apply MTr.single; apply BisimMotTr.eight2nine - simp [htraces1, htraces2] + simp [htraces₁, htraces₂] specialize h htreq specialize h 'a' obtain ⟨h1, h2⟩ := h specialize h1 2 (by constructor) - obtain ⟨s2', htr5, cih⟩ := h1 + obtain ⟨s₂', htr5, cih⟩ := h1 cases htr5 case five2six => simp [TraceEq] at cih - have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by + have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -619,7 +636,7 @@ theorem Bisimulation.traceEq_not_bisim : grind case five2eight => simp only [TraceEq] at cih - have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by + have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -681,7 +698,7 @@ theorem Bisimulation.traceEq_not_bisim : simp at h simp [h] repeat constructor - rw [htraces2, htraces8] at cih + rw [htraces₂, htraces8] at cih apply Set.ext_iff.1 at cih specialize cih ['b'] obtain ⟨cih1, cih2⟩ := cih @@ -693,50 +710,54 @@ theorem Bisimulation.traceEq_not_bisim : /-- In general, bisimilarity and trace equivalence are distinct. -/ theorem Bisimilarity.bisimilarity_neq_traceEq : - ∃ (State : Type) (Label : Type) (lts : LTS State Label), Bisimilarity lts ≠ TraceEq lts := by - obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim + ∃ (State : Type) (Label : Type) (lts : LTS State Label), + HomBisimilarity lts ≠ HomTraceEq lts := by + obtain ⟨State, Label, lts, h⟩ := IsBisimulation.traceEq_not_bisim exists State; exists Label; exists lts intro heq - have hb := Bisimilarity.is_bisimulation (lts := lts) + have hb := Bisimilarity.is_bisimulation (lts₁ := lts) (lts₂ := lts) + simp only [HomBisimilarity] at heq rw [heq] at hb contradiction /-- In any deterministic LTS, trace equivalence is a bisimulation. -/ -theorem Bisimulation.deterministic_traceEq_is_bisim - [lts.Deterministic] : - (lts.IsBisimulation (TraceEq lts)) := by +theorem IsBisimulation.deterministic_traceEq_isBisimulation + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [lts₁.Deterministic] [lts₂.Deterministic] : + (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by simp only [IsBisimulation] - intro s1 s2 hteq μ + intro s₁ s₂ hteq μ constructor case left => - apply TraceEq.deterministic_sim lts s1 s2 hteq + apply TraceEq.deterministic_isSimulation s₁ s₂ hteq case right => - intro s2' htr + intro s₂' htr apply TraceEq.symm at hteq - have h := TraceEq.deterministic_sim lts s2 s1 hteq μ s2' htr - obtain ⟨s1', h⟩ := h - exists s1' + have h := TraceEq.deterministic_isSimulation s₂ s₁ hteq μ s₂' htr + obtain ⟨s₁', h⟩ := h + exists s₁' constructor case left => exact h.1 case right => apply h.2.symm -/-- In any deterministic LTS, trace equivalence implies bisimilarity. -/ -theorem Bisimilarity.deterministic_traceEq_bisim - [lts.Deterministic] (h : s1 ~tr[lts] s2) : - (s1 ~[lts] s2) := by - exists TraceEq lts +/-- In deterministic LTSs, trace equivalence implies bisimilarity. -/ +theorem Bisimilarity.deterministic_traceEq_bisim {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [lts₁.Deterministic] [lts₂.Deterministic] (h : s₁ ~tr[lts₁,lts₂] s₂) : + (s₁ ~[lts₁,lts₂] s₂) := by + exists TraceEq lts₁ lts₂ constructor case left => exact h case right => - apply Bisimulation.deterministic_traceEq_is_bisim + apply IsBisimulation.deterministic_traceEq_isBisimulation -/-- In any deterministic LTS, bisimilarity and trace equivalence coincide. -/ -theorem Bisimilarity.deterministic_bisim_eq_traceEq [lts.Deterministic] : - Bisimilarity lts = TraceEq lts := by - funext s1 s2 +/-- In deterministic LTSs, bisimilarity and trace equivalence coincide. -/ +theorem Bisimilarity.deterministic_bisim_eq_traceEq + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [lts₁.Deterministic] [lts₂.Deterministic] : Bisimilarity lts₁ lts₂ = TraceEq lts₁ lts₂ := by + funext s₁ s₂ simp only [eq_iff_iff] constructor case mp => @@ -746,37 +767,33 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq [lts.Deterministic] : /-! ## Relation to simulation -/ -open LTS in /-- Any bisimulation is also a simulation. -/ -theorem Bisimulation.is_simulation {lts : LTS State Label} {r : State → State → Prop} : - lts.IsBisimulation r → Simulation lts r := by - grind [Simulation] +theorem IsBisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulation lts₁ lts₂ r := by + grind [IsSimulation] -open LTS in /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ -theorem Bisimulation.simulation_iff {lts : LTS State Label} {r : State → State → Prop} : - lts.IsBisimulation r ↔ (Simulation lts r ∧ Simulation lts (flip r)) := by - have _ (s1 s2) : r s1 s2 → flip r s2 s1 := id - grind [Simulation, flip] - -open LTS in -/-- Bisimilarity can also be characterized through symmetric simulations. -/ -theorem Bisimilarity.symm_simulation {lts : LTS State Label} : - Bisimilarity lts = - fun s1 s2 => ∃ r, r s1 s2 ∧ Std.Symm r ∧ Simulation lts r := by - funext s1 s2 +theorem IsBisimulation.isSimulation_iff : + IsBisimulation lts₁ lts₂ r ↔ (IsSimulation lts₁ lts₂ r ∧ IsSimulation lts₂ lts₁ (flip r)) := by + have _ (s₁ s₂) : r s₁ s₂ → flip r s₂ s₁ := id + grind [IsSimulation, flip] + +/-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/ +theorem HomBisimilarity.symm_simulation : + HomBisimilarity lts = + fun s₁ s₂ => ∃ r, r s₁ s₂ ∧ Std.Symm r ∧ IsHomSimulation lts r := by + funext s₁ s₂ apply Iff.eq apply Iff.intro · intro h - have bisim : Bisimilarity lts s1 s2 ∧ Std.Symm (Bisimilarity lts) - ∧ Simulation lts (Bisimilarity lts) := by - grind [Std.Symm, Bisimilarity.symm, Bisimulation.is_simulation] + have bisim : HomBisimilarity lts s₁ s₂ ∧ Std.Symm (HomBisimilarity lts) + ∧ IsHomSimulation lts (HomBisimilarity lts) := by + grind [Std.Symm, Bisimilarity.symm, IsBisimulation.isSimulation] grind · intro ⟨r, hr, hsymm, hsim⟩ have : r = (flip r) := by grind [flip, Std.Symm] - have : lts.IsBisimulation r := by - grind [Bisimulation.simulation_iff] + have : IsHomBisimulation lts r := by + grind [IsBisimulation.isSimulation_iff] grind end Bisimulation @@ -786,207 +803,220 @@ section WeakBisimulation /-! ## Weak bisimulation and weak bisimilarity -/ /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do -internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTS. -/ -def IsWeakBisimulation [HasTau Label] (lts : LTS State Label) - (r : State → State → Prop) := - lts.saturate.IsBisimulation r +internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTSs. -/ +def IsWeakBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) := + IsBisimulation (lts₁.saturate) (lts₂.saturate) r + +/-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ +abbrev IsHomWeakBisimulation [HasTau Label] (lts : LTS State Label) := IsWeakBisimulation lts lts /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/ -def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := - fun s1 s2 => - ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r +def WeakBisimilarity [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + State₁ → State₂ → Prop := + fun s₁ s₂ => + ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsWeakBisimulation lts₁ lts₂ r /-- Notation for weak bisimilarity. -/ -notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s' +scoped notation s:max " ≈[" lts₁ "," lts₂ "] " s':max => WeakBisimilarity lts₁ lts₂ s s' + +/-- Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same. -/ +abbrev HomWeakBisimilarity [HasTau Label] (lts : LTS State Label) := WeakBisimilarity lts lts + +/-- Notation for homogeneous bisimilarity. -/ +scoped notation s:max " ≈[" lts "] " s':max => HomWeakBisimilarity lts s s' /-- An `SWBisimulation` is a more convenient definition of weak bisimulation, because the challenge is a single transition. We prove later that this technique is sound, following a strategy inspired by [Sangiorgi2011]. -/ -def IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.STr s2 μ s2' ∧ r s1' s2') +def IsSWBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.STr s₂ μ s₂' ∧ r s₁' s₂') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.STr s1 μ s1' ∧ r s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.STr s₁ μ s₁' ∧ r s₁' s₂') ) /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (first component). -/ -theorem SWBisimulation.follow_internal_fst - [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s1 s1') : - ∃ s2', lts.τSTr s2 s2' ∧ r s1' s2' := by - induction hstr - case refl => - exists s2 - constructor; constructor - exact hr - case tail sb hrsb htrsb ih1 ih2 => - obtain ⟨sb2, htrsb2, hrb⟩ := ih2 - have h := (hswb hrb HasTau.τ).left _ ih1 - obtain ⟨sb2', htrsb2', hrb'⟩ := h - exists sb2' - constructor - · simp only [sTr_τSTr] at htrsb htrsb2' - exact Relation.ReflTransGen.trans htrsb2 htrsb2' - · exact hrb' +theorem IsSWBisimulation.follow_internal_fst + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (hstr : lts₁.τSTr s₁ s₁') : + ∃ s₂', lts₂.τSTr s₂ s₂' ∧ r s₁' s₂' := by + induction hstr + case refl => + exists s₂ + constructor; constructor + exact hr + case tail sb hrsb htrsb ih1 ih2 => + obtain ⟨sb2, htrsb2, hrb⟩ := ih2 + have h := (hswb hrb HasTau.τ).left _ ih1 + obtain ⟨sb2', htrsb2', hrb'⟩ := h + exists sb2' + constructor + · simp only [sTr_τSTr] at htrsb htrsb2' + exact Relation.ReflTransGen.trans htrsb2 htrsb2' + · exact hrb' /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (second component). -/ -theorem SWBisimulation.follow_internal_snd - [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s2 s2') : - ∃ s1', lts.τSTr s1 s1' ∧ r s1' s2' := by - induction hstr - case refl => - exists s1 - constructor; constructor - exact hr - case tail sb hrsb htrsb ih1 ih2 => - obtain ⟨sb2, htrsb2, hrb⟩ := ih2 - have h := (hswb hrb HasTau.τ).right _ ih1 - obtain ⟨sb2', htrsb2', hrb'⟩ := h - exists sb2' - constructor - · simp only [sTr_τSTr] at htrsb htrsb2' - exact Relation.ReflTransGen.trans htrsb2 htrsb2' - · exact hrb' - +theorem IsSWBisimulation.follow_internal_snd + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (hstr : lts₂.τSTr s₂ s₂') : + ∃ s₁', lts₁.τSTr s₁ s₁' ∧ r s₁' s₂' := by + induction hstr + case refl => + exists s₁ + constructor; constructor + exact hr + case tail sb hrsb htrsb ih1 ih2 => + obtain ⟨sb2, htrsb2, hrb⟩ := ih2 + have h := (hswb hrb HasTau.τ).right _ ih1 + obtain ⟨sb2', htrsb2', hrb'⟩ := h + exists sb2' + constructor + · simp only [sTr_τSTr] at htrsb htrsb2' + exact Relation.ReflTransGen.trans htrsb2 htrsb2' + · exact hrb' /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. This formalises lemma 4.2.10 in [Sangiorgi2011]. -/ theorem isWeakBisimulation_iff_isSWBisimulation - [HasTau Label] {lts : LTS State Label} : - lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} : + IsWeakBisimulation lts₁ lts₂ r ↔ IsSWBisimulation lts₁ lts₂ r := by apply Iff.intro case mp => - intro h s1 s2 hr μ + intro h s₁ s₂ hr μ apply And.intro case left => - intro s1' htr + intro s₁' htr specialize h hr μ - have h' := h.1 s1' (STr.single lts htr) - obtain ⟨s2', htr2, hr2⟩ := h' - exists s2' + have h' := h.1 s₁' (STr.single lts₁ htr) + obtain ⟨s₂', htr2, hr2⟩ := h' + exists s₂' case right => - intro s2' htr + intro s₂' htr specialize h hr μ - have h' := h.2 s2' (STr.single lts htr) - obtain ⟨s1', htr1, hr1⟩ := h' - exists s1' + have h' := h.2 s₂' (STr.single lts₂ htr) + obtain ⟨s₁', htr1, hr1⟩ := h' + exists s₁' case mpr => - intro h s1 s2 hr μ + intro h s₁ s₂ hr μ apply And.intro case left => - intro s1' hstr + intro s₁' hstr cases hstr case refl => - exists s2 + exists s₂ constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => rw [←sTr_τSTr] at hstr1 hstr2 simp only [sTr_τSTr] at hstr1 hstr2 - obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1 + obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_fst h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr - obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2 + obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b - exists s1' + exists s₁' constructor - · exact STr.comp lts hstr1b hstr1b' hstr1' + · exact STr.comp lts₂ hstr1b hstr1b' hstr1' · exact hrb2 case right => - intro s2' hstr + intro s₂' hstr cases hstr case refl => - exists s1 + exists s₁ constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => rw [←sTr_τSTr] at hstr1 hstr2 simp only [sTr_τSTr] at hstr1 hstr2 - obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_snd h hr hstr1 + obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_snd h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr - obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2 + obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b - exists s1' + exists s₁' constructor - · exact STr.comp lts hstr1b hstr1b' hstr1' + · exact STr.comp lts₁ hstr1b hstr1b' hstr1' · exact hrb2 -theorem WeakBisimulation.toSwBisimulation - [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) : - lts.IsSWBisimulation r := isWeakBisimulation_iff_isSWBisimulation.1 h +theorem IsWeakBisimulation.isSwBisimulation + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} + (h : IsWeakBisimulation lts₁ lts₂ r) : + IsSWBisimulation lts₁ lts₂ r := isWeakBisimulation_iff_isSWBisimulation.1 h -theorem SWBisimulation.toWeakBisimulation - [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) : - lts.IsWeakBisimulation r := isWeakBisimulation_iff_isSWBisimulation.2 h +theorem IsSWBisimulation.isWeakBisimulation + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} + (h : IsSWBisimulation lts₁ lts₂ r) : + IsWeakBisimulation lts₁ lts₂ r := isWeakBisimulation_iff_isSWBisimulation.2 h /-- Weak bisimilarity can also be characterized through sw-bisimulations. -/ @[scoped grind =] -theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : LTS State Label) : - WeakBisimilarity lts = - fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsSWBisimulation r := by +theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] + (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + WeakBisimilarity lts₁ lts₂ = + fun s₁ s₂ => ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsSWBisimulation lts₁ lts₂ r := by grind [WeakBisimilarity, isWeakBisimulation_iff_isSWBisimulation.1, isWeakBisimulation_iff_isSWBisimulation.2] -/-- Weak bisimilarity is reflexive. -/ -theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : +/-- Homogeneous weak bisimilarity is reflexive. -/ +theorem HomWeakBisimilarity.refl [HasTau Label] {lts : LTS State Label} (s : State) : s ≈[lts] s := by - rw [WeakBisimilarity.weakBisim_eq_swBisim lts] + simp only [HomWeakBisimilarity] + rw [WeakBisimilarity.weakBisim_eq_swBisim lts lts] exists Eq grind [IsSWBisimulation, STr.single] /-- The inverse of a weak bisimulation is a weak bisimulation. -/ -theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label) - (r : State → State → Prop) (h : lts.IsWeakBisimulation r) : - lts.IsWeakBisimulation (flip r) := by - grind [WeakBisimulation.toSwBisimulation, IsSWBisimulation, - flip, SWBisimulation.toWeakBisimulation] +theorem IsWeakBisimulation.inv [HasTau Label] + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (r : State₁ → State₂ → Prop) (h : IsWeakBisimulation lts₁ lts₂ r) : + IsWeakBisimulation lts₂ lts₁ (flip r) := by + grind [IsWeakBisimulation.isSwBisimulation, IsSWBisimulation, + flip, IsSWBisimulation.isWeakBisimulation] /-- Weak bisimilarity is symmetric. -/ -theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈[lts] s2) : - s2 ≈[lts] s1 := by +theorem WeakBisimilarity.symm [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (h : s₁ ≈[lts₁,lts₂] s₂) : s₂ ≈[lts₂,lts₁] s₁ := by obtain ⟨r, hr, hrh⟩ := h exists (flip r) - grind [WeakBisimulation.inv, flip] + grind [IsWeakBisimulation.inv, flip] /-- The composition of two weak bisimulations is a weak bisimulation. -/ -theorem WeakBisimulation.comp - [HasTau Label] - (lts : LTS State Label) - (r1 r2 : State → State → Prop) - (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) : - lts.IsWeakBisimulation (Relation.Comp r1 r2) := by +theorem IsWeakBisimulation.comp + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : IsWeakBisimulation lts₁ lts₂ r1) (h2 : IsWeakBisimulation lts₂ lts₃ r2) : + IsWeakBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by simp_all only [IsWeakBisimulation] exact h1.comp h2 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/ -theorem SWBisimulation.comp - [HasTau Label] - (lts : LTS State Label) - (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) : - lts.IsSWBisimulation (Relation.Comp r1 r2) := by +theorem IsSWBisimulation.comp + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : IsSWBisimulation lts₁ lts₂ r1) (h2 : IsSWBisimulation lts₂ lts₃ r2) : + IsSWBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by simp_all only [isWeakBisimulation_iff_isSWBisimulation.symm] - apply WeakBisimulation.comp lts r1 r2 h1 h2 + apply IsWeakBisimulation.comp h1 h2 /-- Weak bisimilarity is transitive. -/ -theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} - (lts : LTS State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by +theorem WeakBisimilarity.trans [HasTau Label] + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : s₁ ≈[lts₁,lts₂] s₂) (h2 : s₂ ≈[lts₂,lts₃] s₃) : s₁ ≈[lts₁,lts₃] s₃ := by obtain ⟨r1, hr1, hr1b⟩ := h1 obtain ⟨r2, hr2, hr2b⟩ := h2 exists Relation.Comp r1 r2 constructor case left => - exists s2 + exists s₂ case right => - apply WeakBisimulation.comp lts r1 r2 hr1b hr2b - -/-- Weak bisimilarity is an equivalence relation. -/ -theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : - Equivalence (WeakBisimilarity lts) where - refl := WeakBisimilarity.refl lts - symm := WeakBisimilarity.symm lts - trans := WeakBisimilarity.trans lts + apply IsWeakBisimulation.comp hr1b hr2b + +/-- Homogeneous weak bisimilarity is an equivalence relation. -/ +theorem HomWeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : + Equivalence (HomWeakBisimilarity lts) where + refl := HomWeakBisimilarity.refl + symm := WeakBisimilarity.symm + trans := WeakBisimilarity.trans end WeakBisimulation diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index 3c894ae95b..f39cf449f4 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -10,33 +10,36 @@ public import Cslib.Foundations.Semantics.LTS.Basic @[expose] public section -/-! # Simulation and Similarity +/-! # IsSimulation and Similarity -A simulation is a binary relation on the states of an `LTS`: if two states `s1` and `s2` are -related by a simulation, then `s2` can mimic all transitions of `s1`. Furthermore, the derivatives -reaches through these transitions remain related by the simulation. +A simulation is a binary relation on the states of two `LTS`s: if two states `s₁` and `s2` are +related by a simulation, then `s2` can mimic all transitions of `s₁` in their respective LTSs. +Furthermore, the derivatives reaches through these transitions remain related by the simulation. Similarity is the largest simulation: given an `LTS`, it relates any two states that are related by a simulation for that LTS. +The module provides abbreviations for the homogeneous case of comparing states in the same LTS. + For an introduction to theory of simulation, we refer to [Sangiorgi2011]. ## Main definitions -- `Simulation lts r`: the relation `r` on the states of the LTS `lts` is a simulation. -- `Similarity lts` is the binary relation on the states of `lts` that relates any two states -related by some simulation on `lts`. -- `SimulationEquiv lts` is the binary relation on the states of `lts` that relates any two states -similar to each other. +- `IsSimulation lts₁ lts₂ r`: the relation `r` on the states of `lts₁` and `lts₂` is a simulation. +- `Similarity lts₁ lts₂` is the binary relation that relates any two states related by some +simulation on `lts₁` and `lts₂`. +- `SimulationEquiv lts₁ lts₂` is the binary relation on the states of `lts₁` and `lts₂` that relates +any two states similar to each other. ## Notations -- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the LTS `lts`. -- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the LTS `lts`. +- `s₁ ≤[lts₁, lts₂] s₂`: the states `s₁` and `s2` are similar under `lts₁` and `lts₂`. +- `s₁ ≤≥[lts₁, lts₂] s2`: the states `s₁` and `s2` are simulation equivalent under `lts₁` and +`lts₂`. ## Main statements -- `SimulationEquiv.eqv`: simulation equivalence is an equivalence relation. +- `HomSimulationEquiv.eqv`: homogeneous simulation equivalence is an equivalence relation. -/ @@ -46,18 +49,20 @@ universe u v section Simulation -variable {State : Type u} {Label : Type v} (lts : LTS State Label) - /-- A relation is a simulation if, whenever it relates two states in an lts, any transition originating from the first state is mimicked by a transition from the second state and the reached derivatives are themselves related. -/ -def Simulation (lts : LTS State Label) (r : State → State → Prop) : Prop := - ∀ s1 s2, r s1 s2 → ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' +def IsSimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : + Prop := + ∀ s₁ s2, r s₁ s2 → ∀ μ s₁', lts₁.Tr s₁ μ s₁' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s₁' s2' + +/-- A homogeneous simulation is a simulation where the underlying LTSs are the same. -/ +abbrev IsHomSimulation (lts : LTS State Label) := IsSimulation lts lts /-- Two states are similar if they are related by some simulation. -/ -def Similarity (lts : LTS State Label) : State → State → Prop := - fun s1 s2 => - ∃ r : State → State → Prop, r s1 s2 ∧ Simulation lts r +def Similarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := + fun s₁ s2 => + ∃ r : State₁ → State₂ → Prop, r s₁ s2 ∧ IsSimulation lts₁ lts₂ r /-- Notation for similarity. @@ -65,33 +70,42 @@ Notation for similarity. Differently from standard pen-and-paper presentations, we require the lts to be mentioned explicitly. -/ -notation s:max " ≤[" lts "] " s':max => Similarity lts s s' +scoped notation s:max " ≤[" lts₁ "," lts₂ "] " s':max => Similarity lts₁ lts₂ s s' + +/-- Homogeneous similarity is similarity where the underlying LTSs are the same. -/ +abbrev HomSimilarity (lts : LTS State Label) := Similarity lts lts -/-- Similarity is reflexive. -/ -theorem Similarity.refl (s : State) : s ≤[lts] s := by +/-- Notation for homogeneous similarity. -/ +scoped notation s:max " ≤[" lts "] " s':max => HomSimilarity lts s s' + +/-- Homogeneous similarity is reflexive. -/ +theorem HomSimilarity.refl (s : State) : s ≤[lts] s := by exists Eq - grind [Simulation] + grind [IsSimulation] /-- The composition of two simulations is a simulation. -/ -theorem Simulation.comp - (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : - Simulation lts (Relation.Comp r1 r2) := by - simp_all only [Simulation] - intro s1 s2 hrc μ s1' htr +theorem IsSimulation.comp + (r1 : State₁ → State₂ → Prop) + (r2 : State₂ → State₃ → Prop) + (h1 : IsSimulation lts₁ lts₂ r1) (h2 : IsSimulation lts₂ lts₃ r2) : + IsSimulation lts₁ lts₃ (Relation.Comp r1 r2) := by + simp_all only [IsSimulation] + intro s₁ s2 hrc μ s₁' htr rcases hrc with ⟨sb, hr1, hr2⟩ - specialize h1 s1 sb hr1 μ + specialize h1 s₁ sb hr1 μ specialize h2 sb s2 hr2 μ - have h1' := h1 s1' htr - obtain ⟨s1'', h1'tr, h1'⟩ := h1' - have h2' := h2 s1'' h1'tr + have h1' := h1 s₁' htr + obtain ⟨s₁'', h1'tr, h1'⟩ := h1' + have h2' := h2 s₁'' h1'tr obtain ⟨s2'', h2'tr, h2'⟩ := h2' exists s2'' constructor · exact h2'tr - · exists s1'' + · exists s₁'' /-- Similarity is transitive. -/ -theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lts] s3 := by +theorem Similarity.trans (h1 : s₁ ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,lts₃] s₃) : + s₁ ≤[lts₁,lts₃] s₃ := by obtain ⟨r1, hr1, hr1s⟩ := h1 obtain ⟨r2, hr2, hr2s⟩ := h2 exists Relation.Comp r1 r2 @@ -99,47 +113,52 @@ theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lt case left => exists s2 case right => - apply Simulation.comp lts r1 r2 hr1s hr2s + apply IsSimulation.comp r1 r2 hr1s hr2s -/-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts] s2` and -`s2 ≤[lts] s1`. -/ -def SimulationEquiv (lts : LTS State Label) : State → State → Prop := - fun s1 s2 => - s1 ≤[lts] s2 ∧ s2 ≤[lts] s1 +/-- Simulation equivalence relates all states `s₁` and `s2` such that `s₁ ≤[lts₁ lts₂] s2` and +`s2 ≤[lts₂ lts₁] s₁`. -/ +def SimulationEquiv (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + State₁ → State₂ → Prop := + fun s₁ s2 => + s₁ ≤[lts₁, lts₂] s2 ∧ s2 ≤[lts₂, lts₁] s₁ /-- Notation for simulation equivalence. -/ -notation s:max " ≤≥[" lts "] " s':max => SimulationEquiv lts s s' +scoped notation s:max " ≤≥[" lts₁ "," lts₂ "] " s':max => SimulationEquiv lts₁ lts₂ s s' + +/-- Homogeneous simulation equivalence. -/ +abbrev HomSimulationEquiv (lts : LTS State Label) := SimulationEquiv lts lts + +/-- Notation for homogeneous simulation equivalence. -/ +scoped notation s:max " ≤≥[" lts "] " s':max => HomSimulationEquiv lts s s' -/-- Simulation equivalence is reflexive. -/ -theorem SimulationEquiv.refl (s : State) : s ≤≥[lts] s := by - grind [SimulationEquiv, Similarity.refl] +/-- Homogeneous simulation equivalence is reflexive. -/ +theorem HomSimulationEquiv.refl (s : State) : s ≤≥[lts] s := by + grind [SimulationEquiv, HomSimilarity.refl] /-- Simulation equivalence is symmetric. -/ -theorem SimulationEquiv.symm {s1 s2 : State} (h : s1 ≤≥[lts] s2) : s2 ≤≥[lts] s1 := by +theorem SimulationEquiv.symm {s₁ s2 : State} (h : s₁ ≤≥[lts₁,lts₂] s2) : s2 ≤≥[lts₂, lts₁] s₁ := by grind [SimulationEquiv] /-- Simulation equivalence is transitive. -/ -theorem SimulationEquiv.trans {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 : s2 ≤≥[lts] s3) : - s1 ≤≥[lts] s3 := by +theorem SimulationEquiv.trans (h1 : s₁ ≤≥[lts₁,lts₂] s2) (h2 : s2 ≤≥[lts₂,lts₃] s₃) : + s₁ ≤≥[lts₁,lts₃] s₃ := by grind [SimulationEquiv, Similarity.trans] -/-- Simulation equivalence is an equivalence relation. -/ -theorem SimulationEquiv.eqv (lts : LTS State Label) : - Equivalence (SimulationEquiv lts) := { - refl := SimulationEquiv.refl lts - symm := SimulationEquiv.symm lts - trans := SimulationEquiv.trans lts - } +/-- Homogeneous simulation equivalence is an equivalence relation. -/ +theorem HomSimulationEquiv.eqv : Equivalence (· ≤≥[lts] ·) where + refl := HomSimulationEquiv.refl + symm := SimulationEquiv.symm + trans := SimulationEquiv.trans /-- `calc` support for simulation equivalence. -/ instance : Trans - (SimulationEquiv lts) - (SimulationEquiv lts) - (SimulationEquiv lts) where - trans := SimulationEquiv.trans lts + (SimulationEquiv lts₁ lts₂) + (SimulationEquiv lts₂ lts₃) + (SimulationEquiv lts₁ lts₃) where + trans := SimulationEquiv.trans end Simulation diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index f4036ec209..913372a664 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -7,6 +7,7 @@ Authors: Fabrizio Montesi module public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.LTS.Simulation @[expose] public section @@ -18,11 +19,11 @@ Definitions and results on trace equivalence for `LTS`s. ## Main definitions - `LTS.traces`: the set of traces of a state. -- `TraceEq s1 s2`: `s1` and `s2` are trace equivalent, i.e., they have the same sets of traces. +- `TraceEq s₁ s₂`: `s₁` and `s₂` are trace equivalent, i.e., they have the same sets of traces. ## Notations -- `s1 ~tr[lts] s2`: the states `s1` and `s2` are trace equivalent in `lts`. +- `s₁ ~tr[lts] s₂`: the states `s₁` and `s₂` are trace equivalent in `lts`. ## Main statements @@ -33,70 +34,71 @@ Definitions and results on trace equivalence for `LTS`s. namespace Cslib.LTS -universe u v - -variable {State : Type u} {Label : Type v} (lts : LTS State Label) - /-- The traces of a state `s` is the set of all lists of labels `μs` such that there is a multi-step transition labelled by `μs` originating from `s`. -/ -def traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } +def traces (lts : LTS State Label) (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } /-- If there is a multi-step transition from `s` labelled by `μs`, then `μs` is in the traces of `s`. -/ -theorem traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : - μs ∈ lts.traces s := by - exists s' +theorem traces_in {lts : LTS State Label} (h : lts.MTr s μs s') : μs ∈ lts.traces s := by exists s' /-- Two states are trace equivalent if they have the same set of traces. -/ -def TraceEq (s1 s2 : State) := lts.traces s1 = lts.traces s2 +def TraceEq (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (s₁ : State₁) (s₂ : State₂) := + lts₁.traces s₁ = lts₂.traces s₂ /-- Notation for trace equivalence. -Differently from standard pen-and-paper presentations, we require the lts to be mentioned +Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly. -/ -notation s " ~tr[" lts "] " s' => TraceEq lts s s' +scoped notation s " ~tr[" lts₁ "," lts₂ "] " s' => TraceEq lts₁ lts₂ s s' + +/-- Homogeneous trace equivalence compares states on the same LTS. -/ +abbrev HomTraceEq (lts : LTS State Label) := TraceEq lts lts + +/-- Notation for homogeneous trace equivalence. -/ +scoped notation s:max " ~tr[" lts "] " s':max => HomTraceEq lts s s' -/-- Trace equivalence is reflexive. -/ -theorem TraceEq.refl (s : State) : s ~tr[lts] s := by +/-- Homogeneous trace equivalence is reflexive. -/ +theorem HomTraceEq.refl (s : State) : s ~tr[lts] s := by simp only [TraceEq] /-- Trace equivalence is symmetric. -/ -theorem TraceEq.symm (lts : LTS State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) : - s2 ~tr[lts] s1 := by +theorem TraceEq.symm (h : s₁ ~tr[lts₁,lts₂] s₂) : s₂ ~tr[lts₂,lts₁] s₁ := by simp only [TraceEq] at h simp only [TraceEq] rw [h] /-- Trace equivalence is transitive. -/ -theorem TraceEq.trans {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts] s3) : - s1 ~tr[lts] s3 := by +theorem TraceEq.trans (h1 : s₁ ~tr[lts₁,lts₂] s₂) (h2 : s₂ ~tr[lts₂,lts₃] s₃) : + s₁ ~tr[lts₁,lts₃] s₃ := by simp only [TraceEq] at * rw [h1, h2] -/-- Trace equivalence is an equivalence relation. -/ -theorem TraceEq.eqv (lts : LTS State Label) : Equivalence (TraceEq lts) where - refl := TraceEq.refl lts - symm := TraceEq.symm lts - trans := TraceEq.trans lts +/-- Homogeneous trace equivalence is an equivalence relation. -/ +theorem HomTraceEq.eqv : Equivalence (· ~tr[lts] ·) where + refl := HomTraceEq.refl + symm := TraceEq.symm + trans := TraceEq.trans /-- `calc` support for simulation equivalence. -/ -instance : Trans (TraceEq lts) (TraceEq lts) (TraceEq lts) where - trans := TraceEq.trans lts - -/-- In a deterministic LTS, trace equivalence is a simulation. -/ -theorem TraceEq.deterministic_sim - (lts : LTS State Label) [hdet : lts.Deterministic] (s1 s2 : State) (h : s1 ~tr[lts] s2) : - ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2' := by - intro μ s1' htr1 - have hmtr1 := MTr.single lts htr1 - have hin := traces_in lts s1 [μ] s1' hmtr1 +instance : Trans (TraceEq lts₁ lts₂) (TraceEq lts₂ lts₃) (TraceEq lts₁ lts₃) where + trans := TraceEq.trans + +/-- In deterministic LTSs, trace equivalence is a simulation. -/ +theorem TraceEq.deterministic_isSimulation {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] : + IsSimulation lts₁ lts₂ (TraceEq lts₁ lts₂) := by + intro s₁ s₂ h μ s₁' htr1 + have hmtr1 := MTr.single lts₁ htr1 + have hin := traces_in hmtr1 rw [h] at hin - obtain ⟨s2', hmtr2⟩ := hin - exists s2' + obtain ⟨s₂', hmtr2⟩ := hin + exists s₂' constructor - · apply MTr.single_invert lts _ _ _ hmtr2 + · apply MTr.single_invert lts₂ _ _ _ hmtr2 · simp only [TraceEq, traces] funext μs' simp only [eq_iff_iff] @@ -104,31 +106,31 @@ theorem TraceEq.deterministic_sim constructor case mp => intro hmtr1' - obtain ⟨s1'', hmtr1'⟩ := hmtr1' - have hmtr1comp := MTr.comp lts hmtr1 hmtr1' - have hin := traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp + obtain ⟨s₁'', hmtr1'⟩ := hmtr1' + have hmtr1comp := MTr.comp lts₁ hmtr1 hmtr1' + have hin := traces_in hmtr1comp rw [h] at hin obtain ⟨s', hmtr2'⟩ := hin cases hmtr2' - case stepL s2'' htr2 hmtr2' => + case stepL s₂'' htr2 hmtr2' => exists s' - have htr2' := MTr.single_invert lts _ _ _ hmtr2 - have hdets2 := hdet.deterministic s2 μ s2' s2'' htr2' htr2 - rw [hdets2] + have htr2' := MTr.single_invert lts₂ _ _ _ hmtr2 + have hdets₂ := hdet₂.deterministic s₂ μ s₂' s₂'' htr2' htr2 + rw [hdets₂] exact hmtr2' case mpr => intro hmtr2' - obtain ⟨s2'', hmtr2'⟩ := hmtr2' - have hmtr2comp := MTr.comp lts hmtr2 hmtr2' - have hin := traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp + obtain ⟨s₂'', hmtr2'⟩ := hmtr2' + have hmtr2comp := MTr.comp lts₂ hmtr2 hmtr2' + have hin := traces_in hmtr2comp rw [← h] at hin obtain ⟨s', hmtr1'⟩ := hin cases hmtr1' - case stepL s1'' htr1 hmtr1' => + case stepL s₁'' htr1 hmtr1' => exists s' - have htr1' := MTr.single_invert lts _ _ _ hmtr1 - have hdets1 := hdet.deterministic s1 μ s1' s1'' htr1' htr1 - rw [hdets1] + have htr1' := MTr.single_invert lts₁ _ _ _ hmtr1 + have hdets₁ := hdet₁.deterministic s₁ μ s₁' s₁'' htr1' htr1 + rw [hdets₁] exact hmtr1' end Cslib.LTS diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 08a9b002ee..83850eb12e 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -204,14 +204,14 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q constructor · unfold lts cases htr with grind - · grind [ChoiceComm] + · grind [HomBisimilarity.refl, ChoiceComm] case right => intro s1' htr exists s1' constructor · unfold lts cases htr with grind - · grind [ChoiceComm] + · grind [HomBisimilarity.refl, ChoiceComm] case bisim h => grind [ChoiceComm] @@ -326,7 +326,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceR htr · constructor - apply Bisimilarity.refl + apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s2', htr2, hr2⟩ := hb.follow_fst hr htr @@ -353,7 +353,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceR htr · constructor - apply Bisimilarity.refl + apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s1', htr1, hr1⟩ := hb.follow_snd hr htr @@ -435,7 +435,7 @@ theorem bisimilarity_is_congruence /-- Bisimilarity is a congruence in CCS. -/ instance bisimilarityCongruence : - Congruence (Process Name Constant) (Bisimilarity (lts (defs := defs))) where + Congruence (Process Name Constant) (HomBisimilarity (lts (defs := defs))) where covariant := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩ end CCS diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean index 3b887a237c..9d7478a5a2 100644 --- a/Cslib/Logics/HML/Basic.lean +++ b/Cslib/Logics/HML/Basic.lean @@ -116,7 +116,7 @@ abbrev theory (lts : LTS State Label) (s : State) : Set (Proposition Label) := abbrev TheoryEq (lts : LTS State Label) (s1 s2 : State) := theory lts s1 = theory lts s2 -open Proposition LTS Bisimulation Simulation +open Proposition LTS /-- Characterisation theorem for the denotational semantics. -/ @[scoped grind =] @@ -201,7 +201,7 @@ end ImageToPropositions @[scoped grind ⇒] theorem theoryEq_isBisimulation (lts : LTS State Label) [image_finite : ∀ s μ, Finite (lts.image s μ)] : - lts.IsBisimulation (TheoryEq lts) := by + lts.IsHomBisimulation (TheoryEq lts) := by intro s1 s2 h μ let (s : State) := @Fintype.ofFinite (lts.image s μ) (image_finite s μ) constructor @@ -237,7 +237,7 @@ theorem theoryEq_isBisimulation (lts : LTS State Label) well. -/ @[scoped grind ⇒] lemma bisimulation_satisfies {lts : LTS State Label} - {hrb : lts.IsBisimulation r} + {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) (a : Proposition Label) (hs : Satisfies lts s1 a) : Satisfies lts s2 a := by induction a generalizing s1 s2 with @@ -245,7 +245,7 @@ lemma bisimulation_satisfies {lts : LTS State Label} | _ => grind lemma bisimulation_TheoryEq {lts : LTS State Label} - {hrb : lts.IsBisimulation r} + {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) : TheoryEq lts s1 s2 := by have : s2 ~[lts] s1 := by grind [Bisimilarity.symm] @@ -254,7 +254,7 @@ lemma bisimulation_TheoryEq {lts : LTS State Label} /-- Theory equivalence and bisimilarity coincide for image-finite LTSs. -/ theorem theoryEq_eq_bisimilarity (lts : LTS State Label) [image_finite : ∀ s μ, Finite (lts.image s μ)] : - TheoryEq lts = Bisimilarity lts := by + TheoryEq lts = HomBisimilarity lts := by ext s1 s2 apply Iff.intro <;> intro h · exists TheoryEq lts diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean index c33f2318cc..4468a436aa 100644 --- a/CslibTests/Bisimulation.lean +++ b/CslibTests/Bisimulation.lean @@ -8,7 +8,7 @@ import Cslib.Foundations.Semantics.LTS.Bisimulation namespace CslibTests -open Cslib +open Cslib LTS /- An LTS with two bisimilar states. -/ private inductive tr1 : ℕ → Char → ℕ → Prop where diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean index 8f9d247b92..3e9346f2b8 100644 --- a/CslibTests/HML.lean +++ b/CslibTests/HML.lean @@ -13,7 +13,7 @@ open Cslib open CCS Logic.HML LTS example [∀ p μ, Finite ((CCS.lts (defs := defs)).image p μ)] : - TheoryEq (CCS.lts (defs := defs)) = Bisimilarity (CCS.lts (defs := defs)) := + TheoryEq (CCS.lts (defs := defs)) = HomBisimilarity (CCS.lts (defs := defs)) := theoryEq_eq_bisimilarity .. end CslibTests diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean index 88adf7ba7e..34f3c3db93 100644 --- a/CslibTests/LTS.lean +++ b/CslibTests/LTS.lean @@ -12,7 +12,7 @@ import Cslib.Foundations.Semantics.LTS.Notation namespace CslibTests -open Cslib +open Cslib LTS -- A simple LTS on natural numbers From 0d37cc7fcc985cfc53b155e7eef2453f846c6da2 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Tue, 31 Mar 2026 14:56:45 +0200 Subject: [PATCH 02/18] chore: bump toolchain to v4.29.0 (#463) Co-authored-by: Chris Henson --- Cslib/Foundations/Data/Relation.lean | 15 +++++++------- .../CombinatoryLogic/Confluence.lean | 10 +++++----- lake-manifest.json | 20 +++++++++---------- lean-toolchain | 2 +- 4 files changed, 24 insertions(+), 23 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 22a3d67874..b969bf9c22 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -181,26 +181,27 @@ theorem ChurchRosser.normal_eq (cr : ChurchRosser r) (nx : Normal r x) (ny : Nor /-- A pair of subrelations lifts to transitivity on the relation. -/ @[implicit_reducible] -def trans_of_subrelation (s s' r : α → α → Prop) (hr : Transitive r) +def trans_of_subrelation (s s' r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) (h' : Subrelation s' r) : Trans s s' r where - trans hab hbc := hr (h hab) (h' hbc) + trans hab hbc := hr.trans _ _ _ (h hab) (h' hbc) /-- A subrelation lifts to transitivity on the left of the relation. -/ @[implicit_reducible] -def trans_of_subrelation_left (s r : α → α → Prop) (hr : Transitive r) +def trans_of_subrelation_left (s r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) : Trans s r r where - trans hab hbc := hr (h hab) hbc + trans hab hbc := hr.trans _ _ _ (h hab) hbc /-- A subrelation lifts to transitivity on the right of the relation. -/ @[implicit_reducible] -def trans_of_subrelation_right (s r : α → α → Prop) (hr : Transitive r) +def trans_of_subrelation_right (s r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) : Trans r s r where - trans hab hbc := hr hab (h hbc) + trans hab hbc := hr.trans _ _ _ hab (h hbc) /-- Confluence implies that multi-step joinability is an equivalence. -/ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) : Equivalence (Join (ReflTransGen r)) := by - grind [equivalence_join, reflexive_reflTransGen, transitive_reflTransGen] + apply equivalence_join reflexive_reflTransGen inferInstance + grind /-- A relation is terminating when the inverse of its transitive closure is well-founded. Note that this is also called Noetherian or strongly normalizing in the literature. -/ diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index ff3a07b294..d2553421b6 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -92,13 +92,13 @@ theorem reflTransGen_parallelReduction_mRed : ReflTransGen ParallelReduction = ReflTransGen Red := by ext a b constructor - · apply Relation.reflTransGen_of_transitive_reflexive - · exact fun _ => by rfl - · exact Relation.transitive_reflTransGen + · apply Relation.reflTransGen_of_isTrans_reflexive + · exact Relation.reflexive_reflTransGen + · infer_instance · exact @mRed_of_parallelReduction - · apply Relation.reflTransGen_of_transitive_reflexive + · apply Relation.reflTransGen_of_isTrans_reflexive · exact Relation.reflexive_reflTransGen - · exact Relation.transitive_reflTransGen + · infer_instance · exact fun a a' h => Relation.ReflTransGen.single (parallelReduction_of_red h) /-! diff --git a/lake-manifest.json b/lake-manifest.json index 753330ea60..6b469356b0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "698d2b68b870f1712040ab0c233d34372d4b56df", + "rev": "1a37cd3c8e618022c5e78dee604c75c3c946a681", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "22a0afa903bcf65285152eea298a3d319badc78d", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3", + "rev": "00fe208b8e1364736cca3a9b9601c4fe865856af", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.94", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc8", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lean-toolchain b/lean-toolchain index ccec351f41..14791d727f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc8 +leanprover/lean4:v4.29.0 From 3875bc924771d63b97c02076c37529a7d4773d44 Mon Sep 17 00:00:00 2001 From: Xueying Qin <32066429+XYUnknown@users.noreply.github.com> Date: Thu, 2 Apr 2026 19:20:14 +0200 Subject: [PATCH 03/18] feat(FinFun): Implement the decidable equality for FinFun (#466) Add the implementation of `DecidableEq` for `FinFun` --- Cslib/Foundations/Data/FinFun.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Cslib/Foundations/Data/FinFun.lean b/Cslib/Foundations/Data/FinFun.lean index 3f5b54f957..2f1202cd8e 100644 --- a/Cslib/Foundations/Data/FinFun.lean +++ b/Cslib/Foundations/Data/FinFun.lean @@ -133,6 +133,14 @@ theorem fromFun_comm [Zero β] [DecidableEq α] (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by grind only [= coe_eq_fn, = fromFun_fn, ←= ext] +/-- Decidable equality -/ +instance instDecidableEq [Zero β] [DecidableEq α] [DecidableEq β] : DecidableEq (α →₀ β) := + fun f g => + if h : ∀ a ∈ f.support ∪ g.support, f a = g a then + isTrue <| ext fun a => by grind + else + isFalse <| by grind + end FinFun end Cslib From d1dbe1ec53e08957ff4cb893d82f3e0f7eaa4b00 Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Thu, 2 Apr 2026 22:02:45 -0700 Subject: [PATCH 04/18] chore: Update mathlib revision, fixing a conflict (#467) [This commit](https://github.com/leanprover-community/mathlib4/commit/ed4fde18eec46c041fd609768b16dee361fa6018#diff-54ef6c59abdddf67950b1ee785a0c22c7e03d04f9ad8cdb7cf1d336a72f4d850) in mathlib4 moves `foldl_eq_foldr` to another module, so we need to import it or the build fails with ```lean error: Cslib/Computability/URM/Basic.lean:178:27: Unknown constant `List.foldl_eq_foldr` ``` This PR updates the lake manifest past this commit with `lake update mathlib` and fixes the issue --- Cslib/Computability/URM/Basic.lean | 1 + lake-manifest.json | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Cslib/Computability/URM/Basic.lean b/Cslib/Computability/URM/Basic.lean index b1b9cb1345..bdedd9b0a5 100644 --- a/Cslib/Computability/URM/Basic.lean +++ b/Cslib/Computability/URM/Basic.lean @@ -7,6 +7,7 @@ module public import Cslib.Computability.URM.Defs public import Mathlib.Data.List.MinMax +public import Mathlib.Data.List.Fold /-! # URM Basic Lemmas diff --git a/lake-manifest.json b/lake-manifest.json index 6b469356b0..b19d1a3c91 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a37cd3c8e618022c5e78dee604c75c3c946a681", + "rev": "6ef8cc2731780be866bf243afcb7732f4da5f406", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "d11647e94d22ea0d9c503af4a63d814f89ea0323", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "be1a02994ae681d2676c068ebac67a08bf708f96", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 7643ee4fba05fe7c53dc87f179e0da58e49d102d Mon Sep 17 00:00:00 2001 From: Garmelon Date: Mon, 6 Apr 2026 14:27:14 +0200 Subject: [PATCH 05/18] chore: bump toolchain to v4.30.0-rc1 (#469) Co-authored-by: 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: leanprover-community-mathlib4-bot 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: mathlib-nightly-testing[bot] Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> --- Cslib/Computability/Automata/DA/Congr.lean | 6 +++- Cslib/Computability/Automata/DA/ToNA.lean | 17 ++++++---- .../Automata/EpsilonNA/ToNA.lean | 4 ++- .../Computability/Automata/NA/BuchiEquiv.lean | 5 ++- Cslib/Computability/Automata/NA/Concat.lean | 25 ++++++++++----- Cslib/Computability/Automata/NA/Loop.lean | 15 ++++++--- Cslib/Computability/Automata/NA/Sum.lean | 4 ++- Cslib/Computability/Automata/NA/ToDA.lean | 4 ++- .../Congruences/BuchiCongruence.lean | 22 +++++++++++-- Cslib/Computability/Languages/Language.lean | 31 ++++++++++++------- .../Languages/OmegaLanguage.lean | 25 ++++++++++++--- .../Languages/OmegaRegularLanguage.lean | 4 +-- .../Languages/RegularLanguage.lean | 26 ++++++++++++---- .../Machines/SingleTapeTuring/Basic.lean | 4 ++- Cslib/Computability/URM/Basic.lean | 4 +-- Cslib/Foundations/Data/Nat/Segment.lean | 23 ++++++++++---- Cslib/Foundations/Lint/Basic.lean | 2 +- Cslib/Languages/CCS/BehaviouralTheory.lean | 16 +++++++--- .../LocallyNameless/Untyped/Basic.lean | 2 +- .../Logics/LinearLogic/CLL/EtaExpansion.lean | 26 ++++++++++++++-- .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 12 +++++-- CslibTests/GrindLint.lean | 15 ++++++++- lake-manifest.json | 31 ++++++++++--------- lean-toolchain | 2 +- 24 files changed, 237 insertions(+), 88 deletions(-) diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean index 6301073dca..5d3d47eeb6 100644 --- a/Cslib/Computability/Automata/DA/Congr.lean +++ b/Cslib/Computability/Automata/DA/Congr.lean @@ -58,7 +58,11 @@ the equivalence class corresponding to `s`. -/ @[simp] theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by ext - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + constructor <;> + · intro h + simpa [mem_language, Accepts, congr_mtr_eq] using h end FinAcc diff --git a/Cslib/Computability/Automata/DA/ToNA.lean b/Cslib/Computability/Automata/DA/ToNA.lean index dabbdc1473..8e8bec77ae 100644 --- a/Cslib/Computability/Automata/DA/ToNA.lean +++ b/Cslib/Computability/Automata/DA/ToNA.lean @@ -54,11 +54,13 @@ open scoped FLTS NA.FinAcc in theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} : language a.toNAFinAcc = language a := by ext xs + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ constructor - · grind + · simp_all [mem_language a xs, Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr] · intro _ use a.start - grind + simp_all [Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr] end FinAcc @@ -70,16 +72,19 @@ def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol := { a.toNA with accept := a.accept } open ωAcceptor in -open scoped NA.Buchi in /-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/ @[simp, scoped grind _=_] theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} : language a.toNABuchi = language a := by ext xs; constructor - · grind - · intro _ + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + · simp_all [Accepts, language, toNABuchi] + · intro h use (a.run xs) - grind + split_ands + · grind + · exact Filter.frequently_map.mp h end Buchi diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean index 4882cf6570..35c48e10cf 100644 --- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean @@ -52,7 +52,9 @@ theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} : ext xs have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by simp [LTS.noε_saturate_mTr] - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + grind [Accepts] end Automata.εNA.FinAcc diff --git a/Cslib/Computability/Automata/NA/BuchiEquiv.lean b/Cslib/Computability/Automata/NA/BuchiEquiv.lean index 3c065975d9..607d48a575 100644 --- a/Cslib/Computability/Automata/NA/BuchiEquiv.lean +++ b/Cslib/Computability/Automata/NA/BuchiEquiv.lean @@ -60,7 +60,10 @@ theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} : ext xs constructor · rintro ⟨ss', h_run', h_acc'⟩ - grind [reindex_run_iff] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + simp only [mem_language, Accepts] + exact frequently_principal.mp (· (reindex_run_iff.mp h_run') h_acc') · rintro ⟨ss, h_run, h_acc⟩ use ss.map f constructor <;> grind [reindex_run_iff'] diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index 6e7dac29a2..168621c18a 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -159,22 +159,31 @@ theorem finConcat_language_eq [Inhabited Symbol] : obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_omegaExecution h_mtr have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run] have hr : (ss xl.length).isRight := by grind - obtain ⟨n, _⟩ := concat_run_proj hc hr + obtain ⟨n, _, _, ss2, h_run2, _⟩ := concat_run_proj hc hr refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩ · grind [totalize_language_eq, take_append_of_le_length] · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind - grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have : ss xl.length = inr (ss2 (xl.length - n)) := by grind + have hl : (ss2 (xl.length - n)).isLeft := by grind + obtain ⟨s2, t2, h_mtr2, _, _, _⟩ := totalize_run_mtr h_run2 hl + refine ⟨s2, ?_, t2, ?_, ?_⟩ <;> grind [drop_append_of_le_length, take_append_of_le_length] · exact xl.take_append_drop n · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩ rw [← totalize_language_eq] at h_xl1 obtain ⟨_, h_s2, _, _, h_mtr2⟩ := h_xl2 - obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2 + obtain ⟨_, ss2, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2 obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2 - grind [ - finConcat, List.length_append, take_append_of_le_length, - extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss, - LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length)) - ] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length)) + simp [← append_append_ωSequence, extract_eq_drop_take, + take_append_of_le_length, ← List.length_append] at h_mtr + have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind + have : ss (xl1.length + xl2.length) = inr (ss2 xl2.length) := by grind + refine ⟨ss 0, ?_, ss (xl1.length + xl2.length), ?_, ?_⟩ <;> + grind [finConcat, List.length_append] end FinAcc diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean index 5f4f64b946..7bc0f2a16d 100644 --- a/Cslib/Computability/Automata/NA/Loop.lean +++ b/Cslib/Computability/Automata/NA/Loop.lean @@ -145,8 +145,10 @@ theorem loop_language_eq [Inhabited Symbol] : rintro xs ⟨ss, h_run, h_acc⟩ obtain ⟨k, h1, h2⟩ : ∃ k > 0, (ss k).isLeft := by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0] - obtain ⟨n, _⟩ := loop_run_one_iter h_run h1 h2 - refine ⟨xs.take n, by grind, xs.drop n, ?_, by simp⟩ + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + obtain ⟨n, _, h, _⟩ := loop_run_one_iter h_run h1 h2 + refine ⟨xs.take n, h, xs.drop n, ?_, by simp⟩ refine ⟨ss.drop n, by grind, ?_⟩ apply (drop_frequently_iff_frequently n).mpr grind @@ -191,10 +193,13 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) : obtain ⟨h1, h2⟩ : 0 < xl.length ∧ (ss xl.length).isLeft := by simp only [mem_singleton_iff] at h_acc grind - obtain ⟨n, h_n, _, _, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2 + obtain ⟨n, h_n, h_take, h_drop, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2 left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩ - · grind [totalize_language_eq, take_append_of_le_length] - · refine ⟨ss n, by grind, ss xl.length, by grind, ?_⟩ + · #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + change List.take n xl ∈ language na - 1 -- canonicalize membership instance + grind [totalize_language_eq, take_append_of_le_length] + · refine ⟨ss n, by aesop, ss xl.length, by grind, ?_⟩ have := LTS.OmegaExecution.extract_mTr h_ωtr' (show 0 ≤ xl.length - n by grind) have : n + (xl.length - n) = xl.length := by grind have : ((xl ++ω xs).drop n).extract 0 (xl.length - n) = xl.drop n := by diff --git a/Cslib/Computability/Automata/NA/Sum.lean b/Cslib/Computability/Automata/NA/Sum.lean index 541e152433..2fafad9554 100644 --- a/Cslib/Computability/Automata/NA/Sum.lean +++ b/Cslib/Computability/Automata/NA/Sum.lean @@ -71,7 +71,9 @@ theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I) constructor · rintro ⟨ss, h_run, h_acc⟩ simp only [mem_iUnion] at h_acc - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + grind [Accepts] · rintro ⟨i, ss_i, _⟩ use ss_i.map (Sigma.mk i) simp only [mem_iUnion] diff --git a/Cslib/Computability/Automata/NA/ToDA.lean b/Cslib/Computability/Automata/NA/ToDA.lean index 041f6ab346..3fa43ee86d 100644 --- a/Cslib/Computability/Automata/NA/ToDA.lean +++ b/Cslib/Computability/Automata/NA/ToDA.lean @@ -42,7 +42,9 @@ open scoped DA.FinAcc LTS in theorem toDAFinAcc_language_eq {na : NA.FinAcc State Symbol} : language na.toDAFinAcc = language na := by ext xs - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + grind [Accepts] end FinAcc diff --git a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean index 8a980b7766..c1da62ffb5 100644 --- a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean @@ -84,6 +84,10 @@ lemma buchiCongruence_transfer ( xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl ) := by have h_eq : na.BuchiCongruence.eq xl yl := by apply Quotient.exact + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have : ⟦xl⟧ = a := mem_singleton_iff.mp <| mem_preimage.mp hc + have : ⟦yl⟧ = a := mem_singleton_iff.mp <| mem_preimage.mp hc' grind have := h_eq s t have h_yl : yl ∈ na.pairLang s t := by grind @@ -121,14 +125,26 @@ theorem buchiFamily_cover [Inhabited Symbol] [Finite State] : use ⟦ xs.take (f 0) ⟧, b apply mem_buchiFamily.mpr use xs.take (f 0), xs.drop (f 0) |>.toSegs (f · - f 0) + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ split_ands - · grind + · rfl · intro k specialize h_color {f k, f (k + 1)} have := @h_mono 0 k have := @h_mono k (k + 1) - grind [extract_drop, Finset.insert_nonempty, Finset.singleton_nonempty, min'_insert, - min'_singleton, max'_insert, max'_singleton, toSegs_def, Language.mem_sub_one] + simp only [Language.mem_sub_one, toSegs_def] + split_ands + · have : b = color {f k, f (k + 1)} := by grind + simp_all only [extract_drop, color] + split_ifs with h + · have : f k ≤ f (k + 1) := by lia + have : f 0 + (f k - f 0) = f k := by lia + have : f 0 + (f (k + 1) - f 0) = f (k + 1) := by lia + simp_all + rfl + · simp at h + · grind · grind [Nat.base_zero_strictMono h_mono] -- This intermediate result is split out of the proof of `buchiCongruence_saturation` below diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index e02b50aafd..d9ac2a530f 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -30,14 +30,13 @@ theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i := mem_iInter₂ +#adaptation_note +/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ @[simp] theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) : - (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by - constructor <;> intro h - · have := mem_iUnion₂.mp h - grind - · apply mem_iUnion₂.mpr - grind + (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i where + mp h := bex_def.mp (mem_iUnion₂.mp h) + mpr h := mem_iUnion₂.mpr (bex_def.mpr h) theorem le_one_iff_eq : l ≤ 1 ↔ l = 0 ∨ l = 1 := subset_singleton_iff_eq @@ -50,17 +49,23 @@ theorem mem_sub_one (x : List α) : x ∈ (l - 1) ↔ x ∈ l ∧ x ≠ [] := theorem reverse_sub (l m : Language α) : (l - m).reverse = l.reverse - m.reverse := by ext x; simp [mem_sub] +#adaptation_note +/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ @[scoped grind =] theorem sub_one_mul : (l - 1) * l = l * l - 1 := by ext x; constructor · rintro ⟨u, h_u, v, h_v, rfl⟩ constructor - · refine ⟨u, ?_, v, ?_⟩ <;> grind - · grind [append_eq_nil_iff, mem_one] + · exact ⟨u, Set.mem_of_mem_inter_left h_u, v, h_v, rfl⟩ + · by_contra h + have := mem_sub_one u |>.mp h_u + have := mem_one (u ++ v) |>.mp h + grind [append_eq_nil_iff] · rintro ⟨⟨u, h_u, v, h_v, rfl⟩, h_x⟩ rcases eq_or_ne u [] with (rfl | h_u') - · refine ⟨v, ?_, [], ?_⟩ <;> grind [mem_sub, mem_one] - · refine ⟨u, ?_, v, ?_⟩ <;> grind + · use v, (mem_sub l 1 v |>.mpr) ⟨h_v, Not.intro h_x⟩, [] + grind [mem_sub, mem_one] + · use u, (mem_sub_one u).mpr ⟨h_u, h_u'⟩, v @[scoped grind =] theorem mul_sub_one : l * (l - 1) = l * l - 1 := by @@ -70,6 +75,8 @@ theorem mul_sub_one : l * (l - 1) = l * l - 1 := by _ = (l.reverse * l.reverse - 1).reverse := by rw [sub_one_mul] _ = _ := by rw [reverse_sub, reverse_one, reverse_mul, reverse_reverse] +#adaptation_note +/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ @[scoped grind =] theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by ext x; constructor @@ -77,8 +84,8 @@ theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by obtain ⟨xl, rfl, h_xl⟩ := kstar_def_nonempty l ▸ h1 have h3 : ¬ xl = [] := by grind [one_def] obtain ⟨x, xl', h_xl'⟩ := exists_cons_of_ne_nil h3 - have := h_xl x - refine ⟨x, ?_, xl'.flatten, ?_, ?_⟩ <;> grind [join_mem_kstar] + subst h_xl' + refine ⟨x, mem_preimage.mp (h_xl x ?_), xl'.flatten, join_mem_kstar ?_, ?_⟩ <;> grind · rintro ⟨y, ⟨h_y, h_1⟩, z, h_z, rfl⟩ refine ⟨?_, ?_⟩ · apply (show l * l∗ ≤ l∗ by exact mul_kstar_le_kstar) diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index a761e7182c..8d0892386c 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -279,11 +279,14 @@ theorem one_omegaPow [Inhabited α] : (1 : Language α)^ω = ⊥ := by theorem omegaPow_of_le_one [Inhabited α] (h : l ≤ 1) : l^ω = ⊥ := by cases (Language.le_one_iff_eq.mp h) <;> simp_all +#adaptation_note +/-- A grind regression found moving to nightly-2026-03-31 (from lean#13166? seems different) -/ theorem omegaPow_eq_empty [Inhabited α] (h : l^ω = ⊥) : l ≤ 1 := by intro x h_x by_contra h_contra suffices h' : (const x).flatten ∈ l^ω by simp [h] at h' - exact ⟨const x, rfl, by grind [Language.mem_sub]⟩ + use const x, rfl + exact fun _ => ⟨h_x, h_contra⟩ /-- An alternative characterization of `l * p`. -/ theorem hmul_seq_prop : l * p = { s | ∃ k, s.take k ∈ l ∧ s.drop k ∈ p } := by @@ -325,8 +328,18 @@ theorem omegaPow_coind' [Inhabited α] (h_nn : [] ∉ l) (h_le : p ≤ l * p) : grind [extract_eq_drop_take] choose nxt_n nxt_p using h_nxt let f := iter_helper (fun n ↦ s.drop n ∈ p) nxt_n - have h_f (n) : f n < f (n + 1) ∧ s.extract (f n) (f (n + 1)) ∈ l ∧ s.drop (f (n + 1)) ∈ p := by - induction n <;> grind [iter_helper] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have _ (n) : f n < f (n + 1) := by + induction n + · simp only [f, iter_helper] + split_ifs with h + · simp_all + · simp [drop_zero] at h + contradiction + · grind [iter_helper] + have _ (n) : s.extract (f n) (f (n + 1)) ∈ l ∧ s.drop (f (n + 1)) ∈ p := by + induction n <;> grind [iter_helper] rw [omegaPow_seq_prop] use f grind [strictMono_nat_of_lt_succ, iter_helper] @@ -337,11 +350,13 @@ theorem omegaPow_coind [Inhabited α] (h_le : p ≤ (l - 1) * p) : p ≤ l^ω := refine omegaPow_coind' ?_ h_le simp +#adaptation_note +/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ theorem omegaPow_le_hmul_omegaPow' [Inhabited α] (l : Language α) : l^ω ≤ (l - 1) * l^ω := by rintro s ⟨xs, rfl, h_xs⟩ - refine ⟨xs.head, ?_, xs.tail.flatten, ⟨xs.tail, rfl, ?_⟩, ?_⟩ <;> - grind [Language.mem_sub_one, Language.mem_sub_one, List.ne_nil_iff_length_pos] + refine ⟨xs.head, h_xs 0, xs.tail.flatten, ⟨xs.tail, rfl, ?_⟩, ?_⟩ <;> + grind [l.mem_sub_one] theorem omegaPow_le_hmul_omegaPow [Inhabited α] (l : Language α) : l^ω ≤ l * l^ω := by have h1 := omegaPow_le_hmul_omegaPow' l diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 526cd5e2a9..58e7c4f5a8 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -119,7 +119,7 @@ theorem IsRegular.sup {p1 p2 : ωLanguage Symbol} ext xs simp only [NA.Buchi.iSum_language_eq, mem_sup, mem_language] rw [mem_iUnion, Fin.exists_fin_two] - grind + rfl -- TODO: fix proof to work with backward.isDefEq.respectTransparency set_option backward.isDefEq.respectTransparency false in @@ -141,7 +141,7 @@ theorem IsRegular.inf {p1 p2 : ωLanguage Symbol} ext xs simp only [inter_language_eq, mem_inf, mem_language] rw [mem_iInter, Bool.forall_bool] - grind + rfl /-- The union of any finite number of ω-regular languages is ω-regular. -/ @[simp] diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index af7e9f51b1..7ebaf3ae8d 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -61,7 +61,11 @@ theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegul rw [IsRegular.iff_dfa] at h ⊢ obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h use State, inferInstance, ⟨da, accᶜ⟩ - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + ext + simp only [language, Accepts] + rfl /-- The empty language is regular. -/ @[simp] @@ -69,7 +73,11 @@ theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by rw [IsRegular.iff_dfa] let flts := FLTS.mk (fun () (_ : Symbol) ↦ ()) use Unit, inferInstance, ⟨DA.mk flts (), ∅⟩ - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + ext + simp only [language, Accepts] + rfl /-- The language containing only the empty word is regular. -/ @[simp] @@ -78,10 +86,12 @@ theorem IsRegular.one : (1 : Language Symbol).IsRegular := by let flts := FLTS.mk (fun (_ : Fin 2) (_ : Symbol) ↦ 1) use Fin 2, inferInstance, ⟨DA.mk flts 0, {0}⟩ ext; constructor + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ · intro h; by_contra h' have := dropLast_append_getLast h' - grind - · grind [Language.mem_one] + grind [Accepts] + · grind [Accepts, Language.mem_one] /-- The language of all finite words is regular. -/ @[simp] @@ -97,7 +107,9 @@ theorem IsRegular.inf {l1 l2 : Language Symbol} obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1 obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2 use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩ - ext; grind [Language.mem_inf] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + ext; grind [Accepts, Language.mem_inf] /-- The union of two regular languages is regular. -/ @[simp] @@ -107,7 +119,9 @@ theorem IsRegular.add {l1 l2 : Language Symbol} obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1 obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2 use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩ - ext; grind [Language.mem_add] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + ext; grind [Accepts, Language.mem_add] /-- The intersection of any finite number of regular languages is regular. -/ @[simp] diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 4f31c1530f..4d37134ac1 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -306,7 +306,9 @@ private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) : simp only [step, toCompCfg_left, compComputer] generalize hM : tm1.tr q BiTape.head = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result - cases nextState <;> grind [toCompCfg_left] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + cases nextState <;> (simp_all; rfl) /-- The right converting function commutes with steps of the machines. -/ private theorem map_toCompCfg_right_step : diff --git a/Cslib/Computability/URM/Basic.lean b/Cslib/Computability/URM/Basic.lean index bdedd9b0a5..01786c14d4 100644 --- a/Cslib/Computability/URM/Basic.lean +++ b/Cslib/Computability/URM/Basic.lean @@ -7,7 +7,7 @@ module public import Cslib.Computability.URM.Defs public import Mathlib.Data.List.MinMax -public import Mathlib.Data.List.Fold +--public import Mathlib.Data.List.Fold /-! # URM Basic Lemmas @@ -176,7 +176,7 @@ namespace Program theorem mem_maxRegister {p : Program} {instr : Instr} (h : instr ∈ p) : instr.maxRegister ≤ p.maxRegister := by unfold maxRegister - rw [List.foldl_map.symm, List.foldl_eq_foldr] + rw [List.foldl_map.symm, ←List.foldr_eq_foldl] exact List.le_max_of_le' 0 (List.mem_map.mpr ⟨instr, h, rfl⟩) (le_refl _) end Program diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index be061363b6..9a7240883d 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -59,8 +59,14 @@ theorem nth_succ_gap {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) : element of the range of `f`. -/ theorem nth_of_strictMono (hm : StrictMono f) (n : ℕ) : f n = nth (· ∈ range f) n := by - have (hf : (range f).Finite) : False := hf.not_infinite (strictMono_infinite hm) - rw [←nth_comp_of_strictMono hm] <;> first | grind | simp + rw [← nth_comp_of_strictMono hm] + · simp + · simp + · #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + intros + have : (range f).Infinite := strictMono_infinite hm + contradiction open scoped Classical in /-- If `f 0 = 0`, then `0` is below any `n` not in the range of `f`. -/ @@ -152,11 +158,16 @@ theorem segment_range_val (hm : StrictMono f) {m k : ℕ} · obtain ⟨j, h_j, rfl⟩ : ∃ j < f (m + 1) - f m - 1, k = j + f m + 1 := ⟨k - f m - 1, by omega⟩ induction j case zero => - have : count (· ∈ range f) (f m + 1 + 1) = count (· ∈ range f) (f m + 1) := by - have := strictMono_range_gap hm (show f m < f m + 1 by grind) - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have := strictMono_range_gap hm (show f m < f m + 1 by grind) + have : count (· ∈ range f) (f m + 1 + 1) = count (· ∈ range f) (f m + 1) := by grind have := nth_of_strictMono hm m - grind [count_nth_of_infinite, strictMono_infinite] + have := count_succ (· ∈ range f) + simp_all only [segment, mem_range] + split + · grind [count_nth_of_infinite (strictMono_infinite hm) m] + · grind case succ j _ => have := strictMono_range_gap hm (show f m < j + 1 + f m by grind) have := strictMono_range_gap hm (show f m < j + 1 + f m + 1 by grind) diff --git a/Cslib/Foundations/Lint/Basic.lean b/Cslib/Foundations/Lint/Basic.lean index d7cbeb59f2..5eb31ac5e6 100644 --- a/Cslib/Foundations/Lint/Basic.lean +++ b/Cslib/Foundations/Lint/Basic.lean @@ -22,7 +22,7 @@ public meta def topNamespace : Batteries.Tactic.Lint.Linter where if ← isAutoDecl declName then return none let env ← getEnv if ← isImplicitReducible declName then return none - let nss := env.getNamespaceSet + let nss := env.getNamespaces let top := nss.fold (init := (∅ : NameSet)) fun tot n => match n.components with | r::_::_ => tot.insert r diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 83850eb12e..ad06cf6350 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -283,17 +283,25 @@ theorem bisimilarity_congr_res : case left => intro s1' htr cases htr with | res _ _ htr => - obtain ⟨q', _⟩ := Bisimilarity.is_bisimulation.follow_fst h htr + obtain ⟨q', _, bisim⟩ := Bisimilarity.is_bisimulation.follow_fst h htr exists res a q' unfold lts at * - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + split_ands + · grind + · exact ResBisim.res bisim case right => intro s2' htr cases htr with | res _ _ htr => - obtain ⟨p', _⟩ := Bisimilarity.is_bisimulation.follow_snd h htr + obtain ⟨p', _, bisim⟩ := Bisimilarity.is_bisimulation.follow_snd h htr exists res a p' unfold lts at * - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + split_ands + · grind + · exact ResBisim.res bisim private inductive ChoiceBisim : Process Name Constant → Process Name Constant → Prop where | choice : (p ~[lts (defs := defs)] q) → ChoiceBisim (choice p r) (choice q r) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean index 8e4b44ebe4..164f82d174 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean @@ -113,7 +113,7 @@ def fv : Term Var → Finset Var /-- Locally closed terms. -/ inductive LC : Term Var → Prop -| fvar (x) : LC (fvar x) +| fvar (x : Var) : LC (fvar x) | abs (L : Finset Var) (e : Term Var) : (∀ x ∉ L, LC (e ^ fvar x)) → LC (abs e) | app {l r} : l.LC → r.LC → LC (app l r) diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean index de4cfdb959..2810cb8a35 100644 --- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean +++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean @@ -108,11 +108,33 @@ open Proposition Proof in @[local grind →] private lemma Proof.expand_onlyAtomicAxioms_dual {a : Proposition Atom} : a.expand.onlyAtomicAxioms → a⫠.expand.onlyAtomicAxioms := by - induction a <;> grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + induction a with + | one => simp +contextual [dual, expand, onlyAtomicAxioms] + | bot => + intro h + rw [←h] + congr 1 + · grind + · simp [dual, expand, rwConclusion, Logic.InferenceSystem.rwConclusion] + | _ => grind open Proposition Proof in /-- η-expansion is correct: the proof returned by η-expansion contains only atomic axioms. -/ theorem Proof.expand_onlyAtomicAxioms (a : Proposition Atom) : a.expand.onlyAtomicAxioms := by - induction a <;> grind [onlyAtomicAxioms_rwConclusion] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + induction a with + | one => + rw [←dual_involution .one] + apply expand_onlyAtomicAxioms_dual + simp [expand, onlyAtomicAxioms, dual] + | zero => + rw [←dual_involution .zero] + apply expand_onlyAtomicAxioms_dual + simp [expand, onlyAtomicAxioms, dual] + | top | bot => simp [expand, onlyAtomicAxioms] + | _ => grind end Cslib.CLL diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index 536cb6a5a4..a2d1d7ad8c 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -257,7 +257,13 @@ lemma biorth_least_fact (G : Set P) : have h_min : ∀ {F : Set P}, isFact F → G ⊆ F → G⫠⫠ ⊆ F := by intro F hF hGF - have : F = c F := by grind [isFact] + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + have : F = c F := by + simp only [isFact] at hF + rw [hF] + symm at hF ⊢ + apply ClosureOperator.IsClosed.closure_eq (congrArg orthogonal (congrArg orthogonal hF)) have hF_closed : c.IsClosed F := (c.isClosed_iff).2 this.symm simpa [c] using ClosureOperator.closure_min hGF hF_closed apply h_min @@ -440,7 +446,9 @@ lemma tensor_of_par {G H : Fact P} : (G ⊗ H) = (Gᗮ ⅋ Hᗮ)ᗮ := SetLike.coe_injective <| by simp only [tensor, parr, dualFact, mk_dual, mk_subset, coe_mk] rw [G.eq, H.eq] - grind + #adaptation_note + /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/ + rfl lemma par_of_tensor {G H : Fact P} : (G ⅋ H) = (Gᗮ ⊗ Hᗮ)ᗮ := by simp [tensor_of_par] diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index 37ceb32d21..0a9d2d43dd 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -6,7 +6,7 @@ open Lean Elab.Command elab "open_scoped_all" pre:ident : command => do let env ← getEnv - let nss := env.getNamespaceSet.toList.filter (fun name => name.getRoot = pre.getId) + let nss := env.getNamespaces.filter (fun name => name.getRoot = pre.getId) for ns in nss do let cmd ← `(open scoped $(mkIdent ns)) elabCommand cmd @@ -79,6 +79,19 @@ open_scoped_all Cslib #grind_lint skip Cslib.Logic.HML.bisimulation_satisfies #grind_lint skip Cslib.Logic.HML.Satisfies.diamond #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_l +#adaptation_note +/-- (changes from lean#13166) -/ +#grind_lint skip Cslib.ωLanguage.map_id +#grind_lint skip Cslib.LTS.Bisimilarity.gfp +#grind_lint skip Cslib.LTS.Bisimilarity.is_bisimulation +#grind_lint skip Cslib.LTS.Bisimilarity.largest_bisimulation +#grind_lint skip Cslib.LTS.IsBisimulation.bot +#grind_lint skip Cslib.LTS.IsBisimulation.comp +#grind_lint skip Cslib.LTS.IsBisimulation.inv +#grind_lint skip Cslib.LTS.IsBisimulation.sup +#grind_lint skip Cslib.LTS.IsBisimulation.traceEq +#grind_lint skip Cslib.LTS.IsBisimulationUpTo.is_bisimulation +#grind_lint skip Cslib.Logic.HML.theoryEq_isBisimulation #guard_msgs in #grind_lint check (min := 20) in Cslib diff --git a/lake-manifest.json b/lake-manifest.json index b19d1a3c91..6699e262e3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6ef8cc2731780be866bf243afcb7732f4da5f406", + "rev": "ae0c6140a8312511dbb5bc265a0146dd418eca8d", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d11647e94d22ea0d9c503af4a63d814f89ea0323", + "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,51 +45,52 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "00fe208b8e1364736cca3a9b9601c4fe865856af", + "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.97", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "be1a02994ae681d2676c068ebac67a08bf708f96", + "rev": "bf597c77bf9b8e66720d724928207f5911533113", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", + "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean-toolchain b/lean-toolchain index 14791d727f..2210cba4ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.30.0-rc1 From 6178564385020c1b9ce5d97bc6d2ce5cfc401d61 Mon Sep 17 00:00:00 2001 From: thomaskwaring <51426330+thomaskwaring@users.noreply.github.com> Date: Mon, 6 Apr 2026 19:12:30 +0200 Subject: [PATCH 06/18] feat(Logics/Propositional): definitions (#89) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR defines propositions for propositional logic, including notation for the logical connectives. A `Theory` is a set of `Proposition`. Also defines minimal, intuitionistic and classical theories, and extensions of maps `Atom → Atom'` to maps `Proposition Atom → Proposition Atom'` and `Theory Atom → Theory Atom'`. --------- Co-authored-by: twwar --- Cslib.lean | 1 + Cslib/Logics/Propositional/Defs.lean | 158 +++++++++++++++++++++++++++ 2 files changed, 159 insertions(+) create mode 100644 Cslib/Logics/Propositional/Defs.lean diff --git a/Cslib.lean b/Cslib.lean index a621d6e147..a3ede3c275 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -118,3 +118,4 @@ public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.CutElimination public import Cslib.Logics.LinearLogic.CLL.EtaExpansion public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic +public import Cslib.Logics.Propositional.Defs diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean new file mode 100644 index 0000000000..f80797ff47 --- /dev/null +++ b/Cslib/Logics/Propositional/Defs.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ + +module + +public import Cslib.Init +public import Mathlib.Data.FunLike.Basic +public import Mathlib.Data.Set.Image +public import Mathlib.Order.TypeTags + +@[expose] public section + +/-! # Propositions and theories + +## Main definitions + +- `Proposition` : the type of propositions over a given type of atom. This type has a `Bot` +instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited. +- `Theory` : set of `Proposition`. +- `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion. +- `IsClassical` : an intuitionistic theory is classical if it further contains double negation +elimination. +- `Proposition.map`, `Theory.map` : a map between `Atom` types extends to a map between +propositions and theories. +- `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given +theory. + +## Notation + +We introduce notation for the logical connectives: `⊥ ⊤ ⋏ ⋎ ⟶ ~` for, respectively, falsum, verum, +conjunction, disjunction, implication and negation. +-/ + +universe u + +variable {Atom : Type u} [DecidableEq Atom] + +namespace Cslib.Logic.PL + +/-- Propositions. -/ +inductive Proposition (Atom : Type u) : Type u where + /-- Propositional atoms -/ + | atom (x : Atom) + /-- Conjunction -/ + | and (a b : Proposition Atom) + /-- Disjunction -/ + | or (a b : Proposition Atom) + /-- Implication -/ + | impl (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 · ⊥) + +/-- 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) + +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 + +/-- A function on atoms induces a function on propositions. -/ +def Proposition.map {Atom Atom' : Type u} (f : Atom → Atom') : Proposition Atom → Proposition Atom' + | atom x => atom (f x) + | and A B => (A.map f) ∧ (B.map f) + | or A B => (A.map f) ∨ (B.map f) + | impl A B => (A.map f) → (B.map f) + +instance {Atom Atom' : Type u} : FunLike (Atom → Atom') (Proposition Atom) (Proposition Atom') where + coe := Proposition.map + coe_injective' f f' h := by + ext x + have : (Proposition.atom x).map f = (Proposition.atom x).map f' := + congrFun h (Proposition.atom x) + grind [Proposition.map] + +/-- Theories are arbitrary sets of propositions. -/ +abbrev Theory (Atom) := Set (Proposition Atom) + +namespace Theory + +/-- Extend `Proposition.map` to theories. -/ +def map {Atom Atom' : Type u} (f : Atom → Atom') : Theory Atom → Theory Atom' := + Set.image (Proposition.map f) + +instance {Atom Atom' : Type u} : FunLike (Atom → Atom') (Theory Atom) (Theory Atom') where + coe := Theory.map + coe_injective' f f' h := by + ext x + have : Theory.map f {Proposition.atom x} = Theory.map f' {Proposition.atom x} := + congrFun h {Proposition.atom x} + simpa [Theory.map, Proposition.map] using this + +/-- The empty theory corresponds to minimal propositional logic. -/ +abbrev MPL : Theory (Atom) := ∅ + +/-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/ +abbrev IPL [Bot Atom] : Theory Atom := + Set.range (⊥ → ·) + +/-- Classical logic further adds double negation elimination. -/ +abbrev CPL [Bot Atom] : Theory Atom := + Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A) + +/-- A theory is intuitionistic if it validates ex falso quodlibet. -/ +@[scoped grind] +class IsIntuitionistic [Bot Atom] (T : Theory Atom) where + efq (A : Proposition Atom) : (⊥ → A) ∈ T + +omit [DecidableEq Atom] in +@[scoped grind =] +theorem isIntuitionisticIff [Bot Atom] (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind + +/-- A theory is classical if it validates double-negation elimination. -/ +@[scoped grind] +class IsClassical [Bot Atom] (T : Theory Atom) where + dne (A : Proposition Atom) : (¬¬A → A) ∈ T + +omit [DecidableEq Atom] in +@[scoped grind =] +theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind + +instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where + efq A := Set.mem_range.mpr ⟨A, rfl⟩ + +instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where + dne A := Set.mem_range.mpr ⟨A, rfl⟩ + +omit [DecidableEq Atom] in +@[scoped grind →] +theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T] + (h : T ⊆ T') : IsIntuitionistic T' := by grind + +omit [DecidableEq Atom] in +@[scoped grind →] +theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : + IsClassical T' := by grind + +/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ +@[reducible] +def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) := + T.map (WithBot.some) ∪ IPL + +instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) : + IsIntuitionistic T.intuitionisticCompletion := by grind + +end Cslib.Logic.PL.Theory From 48e29fde33e1d1650a1615ba4d1440a1c36a23c3 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 7 Apr 2026 07:56:41 +0100 Subject: [PATCH 07/18] feat: define the category of LTSs (#391) This PR resolves #387. --------- Co-authored-by: Chris Henson Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib.lean | 1 + .../Semantics/LTS/LTSCat/Basic.lean | 100 ++++++++++++++++++ references.bib | 13 +++ 3 files changed, 114 insertions(+) create mode 100644 Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean diff --git a/Cslib.lean b/Cslib.lean index a3ede3c275..3e5977af26 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -65,6 +65,7 @@ public import Cslib.Foundations.Semantics.LTS.Bisimulation public import Cslib.Foundations.Semantics.LTS.Divergence public import Cslib.Foundations.Semantics.LTS.Execution public import Cslib.Foundations.Semantics.LTS.HasTau +public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic public import Cslib.Foundations.Semantics.LTS.Notation public import Cslib.Foundations.Semantics.LTS.OmegaExecution public import Cslib.Foundations.Semantics.LTS.Relation diff --git a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean new file mode 100644 index 0000000000..4b8b2ff875 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Ayberk Tosun (Zeroth Research). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ayberk Tosun +-/ + +module + +public import Mathlib.CategoryTheory.Category.Basic +public import Cslib.Foundations.Semantics.LTS.Basic +public import Mathlib.Control.Basic + +@[expose] public section + +namespace Cslib + +variable {State Label : Type*} + +/-! # Category of Labelled Transition Systems + +This file contains the definition of the category of labelled transition systems +as defined in Winskel and Nielsen's handbook chapter [WinskelNielsen1995]. + +## References + +* [N. Winskel and M. Nielsen, *Models for concurrency*][WinskelNielsen1995] +-/ + +/-- +We first define what is denoted Tran* in [WinskelNielsen1995]: the extension of +a transition relation with idle transitions. +-/ +def LTS.withIdle (lts : LTS State Label) : LTS State (Option Label) := + ⟨fun s l s' => l.elim (s = s') (lts.Tr s · s')⟩ + +/-! ## LTSs and LTS morphisms form a category -/ + +/-- +The definition of labelled transition system (with the type of states and the +type of labels as part of the structure). +-/ +@[nolint checkUnivs] +structure LTSCat : Type (max u v + 1) where + /-- Type of states of an LTS -/ + State : Type u + /-- Type of labels of an LTS -/ + Label : Type v + /-- Transition relation of an LTS -/ + lts : LTS State Label + +/-- +A morphism between two labelled transition systems consists of (1) a function on +states, (2) a partial function on labels, and a proof that (1) preserves each +transition along (2). +-/ +structure LTS.Morphism (lts₁ lts₂ : LTSCat) : Type where + /-- Mapping of states of `lts₁` to states of `lts₂` -/ + stateMap : lts₁.State → lts₂.State + /-- Mapping of labels of `lts₁` to labels of `lts₂` -/ + labelMap : lts₁.Label → Option lts₂.Label + /-- Stipulation that `stateMap` preserve transitions -/ + labelMap_tr (s s' : lts₁.State) (l : lts₁.Label) : + lts₁.lts.Tr s l s' → (withIdle lts₂.lts).Tr (stateMap s) (labelMap l) (stateMap s') + +/-- The identity LTS morphism. -/ +def LTS.Morphism.id (lts : LTSCat) : LTS.Morphism lts lts where + stateMap := _root_.id + labelMap := pure + labelMap_tr _ _ _ := _root_.id + +/-- Composition of LTS morphisms. + +We use Kleisli composition to define this. +-/ +def LTS.Morphism.comp {lts₁ lts₂ lts₃} (f : LTS.Morphism lts₁ lts₂) (g : LTS.Morphism lts₂ lts₃) : + LTS.Morphism lts₁ lts₃ where + stateMap := g.stateMap ∘ f.stateMap + labelMap := f.labelMap >=> g.labelMap + labelMap_tr s s' l h := by + obtain ⟨f, μ, p⟩ := f + obtain ⟨g, ν, q⟩ := g + simp only [LTS.withIdle] at p q + change ((μ l).bind ν).elim (g (f s) = g (f s')) _ + cases hμ : μ l with grind + +/-- Finally, we prove that these form a category. -/ +instance : CategoryTheory.Category LTSCat where + Hom := LTS.Morphism + id := LTS.Morphism.id + comp := LTS.Morphism.comp + comp_id _ := by + simp only [LTS.Morphism.comp, LTS.Morphism.id] + congr 1 + rw [fish_pure] + assoc _ _ _ := by + simp only [LTS.Morphism.comp] + congr 1 + rw [fish_assoc] + +end Cslib diff --git a/references.bib b/references.bib index edb111f479..2cccb928f5 100644 --- a/references.bib +++ b/references.bib @@ -264,3 +264,16 @@ @article{ ShepherdsonSturgis1963 publisher = {Association for Computing Machinery}, address = {New York, NY, USA} } + +@incollection{WinskelNielsen1995, + author = {Winskel, Glynn and Nielsen, Mogens}, + isbn = {9780198537809}, + title = {Models for concurrency}, + booktitle = {Handbook of Logic in Computer Science}, + publisher = {Oxford University Press}, + year = {1995}, + month = {05}, + doi = {10.1093/oso/9780198537809.003.0001}, + url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, + eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, +} From 615b6d3f688931a77ae8abd2d7ef03e0ecdc882b Mon Sep 17 00:00:00 2001 From: Chris Henson <46805207+chenson2018@users.noreply.github.com> Date: Mon, 13 Apr 2026 04:05:29 -0400 Subject: [PATCH 08/18] ci: use full `weeklyLintSet` and mathlib-ci (#488) This PR updates the weekly linting job to use the full `linter.weeklyLintSet` and the same reporting script as Mathlib for consistency. The manifest update is intentional to bring in new linting added in https://github.com/leanprover-community/mathlib4/pull/37916. --- .github/workflows/weekly-lints.yml | 29 ++++++++-- lake-manifest.json | 6 +- scripts/README.md | 10 ---- scripts/weekly_lint_report.sh | 90 ------------------------------ 4 files changed, 27 insertions(+), 108 deletions(-) delete mode 100755 scripts/weekly_lint_report.sh diff --git a/.github/workflows/weekly-lints.yml b/.github/workflows/weekly-lints.yml index 57a22ff048..42462e34ef 100644 --- a/.github/workflows/weekly-lints.yml +++ b/.github/workflows/weekly-lints.yml @@ -5,20 +5,35 @@ on: - cron: '0 5 * * 1' # Run at 05:00 UTC every Monday workflow_dispatch: # Allow manual triggering +env: + CSLIB: cslib + jobs: weekly-lints: name: Weekly Linting runs-on: ubuntu-latest if: github.repository == 'leanprover/cslib' steps: + - name: Checkout Mathlib actions + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 1 + repository: leanprover-community/mathlib4 + sparse-checkout: .github/actions + path: workflow-actions + + - name: Get mathlib-ci + uses: ./workflow-actions/.github/actions/get-mathlib-ci + - uses: actions/checkout@v4 with: - ref: main + path: ${{ env.CSLIB }} - name: Enable weekly linters + working-directory: ${{ github.workspace }}/${{ env.CSLIB }} run: | # Add the mergeWithGrind linter back for this run - sed -i '/^\[leanOptions\]/a weak.linter.tacticAnalysis.mergeWithGrind = true' lakefile.toml + sed -i '/^\[leanOptions\]/a weak.linter.weeklyLintSet = true' lakefile.toml # Show what changed git diff lakefile.toml @@ -29,17 +44,21 @@ jobs: auto-config: false use-github-cache: true use-mathlib-cache: true + lake-package-directory: ${{ env.CSLIB }} - name: Build with weekly linters id: build + working-directory: ${{ github.workspace }}/${{ env.CSLIB }} continue-on-error: true run: | lean_outfile=$(mktemp) (lake build || true) 2>&1 | tee "${lean_outfile}" - # Generate report for Zulip - bash scripts/weekly_lint_report.sh "${lean_outfile}" \ - "${{ github.sha }}" "${{ github.repository }}" "${{ github.run_id }}" > "${GITHUB_OUTPUT}" + # Process output for posting to Zulip + SHA=${{ github.sha }} \ + REPO=${{ github.repository }} \ + RUN_ID=${{ github.run_id }} \ + "${CI_SCRIPTS_DIR}/reporting/zulip_build_report.sh" "${lean_outfile}" > "${GITHUB_OUTPUT}" - name: Post output to Zulip uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 diff --git a/lake-manifest.json b/lake-manifest.json index 6699e262e3..d9898a180a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ae0c6140a8312511dbb5bc265a0146dd418eca8d", + "rev": "3d8100bbc657181d1f48868decaba9159580aa40", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3", + "rev": "a3b459a8312125758e51c354b93d54ba620efda6", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/scripts/README.md b/scripts/README.md index df8e55c302..19d71dfa67 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -45,13 +45,3 @@ to learn about it as well! **Init Imports** - `CheckInitImports.lean` (run by `lake exe checkInitImports`) checks that all files transitively import `Cslib.Init`. - -**Linting** -- `weekly_lint_report.sh` - Generates a summary of the weekly lint run for posting to Zulip. Called by the `weekly-lints.yml` workflow. - The output format matches Mathlib's weekly linting reports, with tables showing grouped message counts. - - **Usage:** - ```bash - bash scripts/weekly_lint_report.sh - ``` diff --git a/scripts/weekly_lint_report.sh b/scripts/weekly_lint_report.sh deleted file mode 100755 index ca8bf31ce7..0000000000 --- a/scripts/weekly_lint_report.sh +++ /dev/null @@ -1,90 +0,0 @@ -#!/bin/bash -# Weekly lint report generator for CSLib. -# -# Parses Lean build output and generates a Zulip-formatted report with tables -# showing grouped message counts. Output format matches Mathlib's weekly linting reports. -# -# Usage: weekly_lint_report.sh - -set -euo pipefail - -lean_outfile=$1 -sha=$2 -repo=$3 -run_id=$4 - -short_sha=${sha:0:7} - -# Filter out build progress and trace lines -filtered_out=$(grep -v '^✔' "${lean_outfile}" | grep -v '^trace: ' | grep -v 'checking out revision' || true) -echo "$(echo "${filtered_out}" | grep -c '' || echo 0) lines of output" >&2 - -# Extract and count messages by type -error_lines=$(echo "${filtered_out}" | grep '^error: ' || true) -warning_lines=$(echo "${filtered_out}" | grep '^warning: ' || true) -info_lines=$(echo "${filtered_out}" | grep '^info: ' || true) - -# Strip prefix and file:line:col to get just descriptions -error_descriptions=$(echo "${error_lines}" | sed 's/^error: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^error: //' || true) -warning_descriptions=$(echo "${warning_lines}" | sed 's/^warning: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^warning: //' || true) -info_descriptions=$(echo "${info_lines}" | sed 's/^info: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^info: //' || true) - -# Count non-empty lines -count_lines() { - local input="$1" - if [ -z "${input}" ]; then - echo 0 - else - echo "${input}" | grep -c '' || echo 0 - fi -} - -# Format descriptions as markdown table rows, grouped and sorted by count -format_table_rows() { - sort | uniq -c | sort -bgr | sed 's/^ *\([0-9][0-9]*\) \(.*\)$/| \1 | \2 |/' -} - -# Combine all descriptions -all_descriptions=$(printf '%s\n%s\n%s' "${error_descriptions}" "${warning_descriptions}" "${info_descriptions}" | grep -v '^$' || true) - -error_count=$(count_lines "${error_lines}") -warning_count=$(count_lines "${warning_lines}") -info_count=$(count_lines "${info_lines}") - -echo "${error_count} errors" >&2 -echo "${warning_count} warnings" >&2 -echo "${info_count} info messages" >&2 - -# Output in GitHub Actions multiline format -delimiter=$(uuidgen 2>/dev/null || cat /proc/sys/kernel/random/uuid 2>/dev/null || echo "EOF_${RANDOM}") -echo "zulip-message<<${delimiter}" - -echo "CSLib weekly lint run [completed](https://github.com/${repo}/actions/runs/${run_id}) ([${short_sha}](https://github.com/${repo}/commit/${sha}))." - -if [ "${error_count}" -eq 0 ] && [ "${warning_count}" -eq 0 ] && [ "${info_count}" -eq 0 ]; then - echo "Build completed without lint messages." -else - # Summary counts - if [ "${error_count}" -gt 0 ]; then - echo " Errors: ${error_count}" - fi - if [ "${warning_count}" -gt 0 ]; then - echo " Warnings: ${warning_count}" - fi - if [ "${info_count}" -gt 0 ]; then - echo " Info messages: ${info_count}" - fi - echo - - # Detail table - if [ -n "${all_descriptions}" ]; then - echo "\`\`\`spoiler Lint message counts" - echo "| | Message |" - echo "| ---: | --- |" - echo "${all_descriptions}" | format_table_rows - echo "\`\`\`" - echo - fi -fi - -echo "${delimiter}" From f22a2413a471f4ede14853aaa2afeabdd145fca0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 13 Apr 2026 11:27:28 -0700 Subject: [PATCH 09/18] fix: missing `pure`s in the `Id` monad (#439) This fixes some statements that were type incorrect; their LHS was `Id X` and their RHS `X`. The latter can be cast to the former with `pure`. --- .../Control/Monad/Free/Effects.lean | 38 +++++++++---------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/Cslib/Foundations/Control/Monad/Free/Effects.lean b/Cslib/Foundations/Control/Monad/Free/Effects.lean index e1675c01aa..b68cfcb9d8 100644 --- a/Cslib/Foundations/Control/Monad/Free/Effects.lean +++ b/Cslib/Foundations/Control/Monad/Free/Effects.lean @@ -100,9 +100,8 @@ The canonical interpreter `toStateM` derived from `liftM` agrees with the hand-w recursive interpreter `run` for `FreeState`. -/ @[simp] -theorem run_toStateM {α : Type u} (comp : FreeState σ α) : - (toStateM comp).run = run comp := by - ext s₀ : 1 +theorem run_toStateM {α : Type u} (comp : FreeState σ α) (s₀ : σ) : + (toStateM comp).run s₀ = pure (run comp s₀) := by induction comp generalizing s₀ with | pure a => rfl | liftBind op cont ih => @@ -123,11 +122,10 @@ lemma run_set (s' : σ) (k : PUnit → FreeState σ α) (s₀ : σ) : /-- Run a state computation, returning only the result. -/ def run' (c : FreeState σ α) (s₀ : σ) : α := (run c s₀).1 -@[simp] -theorem run'_toStateM {α : Type u} (comp : FreeState σ α) : - (toStateM comp).run' = run' comp := by - ext s₀ : 1 - rw [run', ← run_toStateM] +-- not `simp` since `StateT.run'` is unfolded by `simp` +theorem run'_toStateM {α : Type u} (comp : FreeState σ α) (s₀ : σ) : + (toStateM comp).run' s₀ = pure (run' comp s₀) := by + rw [run', StateT.run'_eq, run_toStateM] rfl @[simp] @@ -209,13 +207,16 @@ The canonical interpreter `toWriterT` derived from `liftM` agrees with the hand- recursive interpreter `run` for `FreeWriter`. -/ @[simp] -theorem run_toWriterT {α : Type u} [Monoid ω] : - ∀ comp : FreeWriter ω α, (toWriterT comp).run = run comp - | .pure _ => by simp only [toWriterT, liftM_pure, run_pure, pure, WriterT.run] - | liftBind (.tell w) cont => by - simp only [toWriterT, liftM_liftBind, run_liftBind_tell] at * - rw [← run_toWriterT] - congr +theorem run_toWriterT {α : Type u} [Monoid ω] (comp : FreeWriter ω α) : + (toWriterT comp).run = pure (run comp) := by + ext : 1 + induction comp with + | pure _ => simp only [toWriterT, liftM_pure, run_pure, pure, WriterT.run] + | liftBind op cont ih => + cases op + simp only [toWriterT, liftM_liftBind, run_liftBind_tell, Id.run_pure] at * + rw [ ← ih] + simp [WriterT.run_bind, writerInterp] /-- `listen` captures the log produced by a subcomputation incrementally. It traverses the computation, @@ -301,9 +302,8 @@ The canonical interpreter `toContT` derived from `liftM` agrees with the hand-wr recursive interpreter `run` for `FreeCont`. -/ @[simp] -theorem run_toContT {α : Type u} (comp : FreeCont r α) : - (toContT comp).run = run comp := by - ext k +theorem run_toContT {α : Type u} (comp : FreeCont r α) (k : α → r) : + (toContT comp).run k = pure (run comp k) := by induction comp with | pure a => rfl | liftBind op cont ih => @@ -387,7 +387,7 @@ The canonical interpreter `toReaderM` derived from `liftM` agrees with the hand- recursive interpreter `run` for `FreeReader` -/ @[simp] theorem run_toReaderM {α : Type u} (comp : FreeReader σ α) (s : σ) : - (toReaderM comp).run s = run comp s := by + (toReaderM comp).run s = pure (run comp s) := by induction comp generalizing s with | pure a => rfl | liftBind op cont ih => From d3a900658f191f4dba19ccd49a3afea61095560e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Apr 2026 05:25:04 -0700 Subject: [PATCH 10/18] feat(Free/Effects): add missing run_bind lemmas (#490) --- .../Control/Monad/Free/Effects.lean | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/Cslib/Foundations/Control/Monad/Free/Effects.lean b/Cslib/Foundations/Control/Monad/Free/Effects.lean index b68cfcb9d8..77982767af 100644 --- a/Cslib/Foundations/Control/Monad/Free/Effects.lean +++ b/Cslib/Foundations/Control/Monad/Free/Effects.lean @@ -119,6 +119,15 @@ lemma run_get (k : σ → FreeState σ α) (s₀ : σ) : lemma run_set (s' : σ) (k : PUnit → FreeState σ α) (s₀ : σ) : run (liftBind (.set s') k) s₀ = run (k .unit) s' := rfl +@[simp] +lemma run_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) : + run (x.bind f) s₀ = let p := x.run s₀; (f p.1).run p.2 := by + induction x generalizing f s₀ with + | pure => simp + | liftBind op cont ih => + rw [FreeM.liftBind_bind] + cases op <;> simp [run, ih] + /-- Run a state computation, returning only the result. -/ def run' (c : FreeState σ α) (s₀ : σ) : α := (run c s₀).1 @@ -140,6 +149,11 @@ lemma run'_get (k : σ → FreeState σ α) (s₀ : σ) : lemma run'_set (s' : σ) (k : PUnit → FreeState σ α) (s₀ : σ) : run' (liftBind (.set s') k) s₀ = run' (k .unit) s' := rfl +@[simp] +lemma run'_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) : + run' (x.bind f) s₀ = let p := x.run s₀; (f p.1).run' p.2 := + congr_arg Prod.fst <| run_bind _ _ _ + end FreeState /-! ### Writer Monad via `FreeM` -/ @@ -198,6 +212,16 @@ def run [Monoid ω] : FreeWriter ω α → α × ω lemma run_pure [Monoid ω] (a : α) : run (.pure a : FreeWriter ω α) = (a, 1) := rfl +@[simp] +lemma run_bind [Monoid ω] (x : FreeWriter ω α) (f : α → FreeWriter ω β) : + run (x.bind f) = let p := run x; ((f p.1).run.1, p.2 * (f p.1).run.2) := by + induction x generalizing f with + | pure => simp + | liftBind op cont ih => + rw [FreeM.liftBind_bind] + cases op + simp [run, ih, mul_assoc] + @[simp] lemma run_liftBind_tell [Monoid ω] (w : ω) (k : PUnit → FreeWriter ω α) : run (liftBind (.tell w) k) = (let (a, w') := run (k .unit); (a, w * w')) := rfl @@ -317,6 +341,16 @@ theorem run_toContT {α : Type u} (comp : FreeCont r α) (k : α → r) : lemma run_pure (a : α) (k : α → r) : run (.pure a : FreeCont r α) k = k a := rfl +@[simp] +lemma run_bind (x : FreeCont r α) (f : α → FreeCont r β) (k : β → r) : + run (x.bind f) k = run x (fun i => run (f i) k) := by + induction x generalizing k with + | pure a => rfl + | liftBind op cont ih => + rw [FreeM.liftBind_bind] + cases op + simp [run, ih] + @[simp] lemma run_liftBind_callCC (g : (α → r) → r) (cont : α → FreeCont r β) (k : β → r) : @@ -401,6 +435,14 @@ lemma run_pure (a : α) (s₀ : σ) : lemma run_read (k : σ → FreeReader σ α) (s₀ : σ) : run (liftBind .read k) s₀ = run (k s₀) s₀ := rfl +@[simp] +lemma run_bind (x : FreeReader σ α) (f : α → FreeReader σ β) (s₀ : σ) : + run (x.bind f) s₀ = run (f <| run x s₀) s₀ := by + induction x generalizing s₀ with + | pure a => rfl + | liftBind op cont ih => + cases op; apply ih + instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where withReader {α} f m := let rec go : FreeReader σ α → FreeReader σ α From 906574d376632467fd84a2a404efbe58a95fc13c Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 15 Apr 2026 08:53:49 -0400 Subject: [PATCH 11/18] feat(Cryptography): formalise perfect secrecy and the one-time pad (#464) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `Cslib.Cryptography.PerfectSecrecy` with information-theoretic private-key encryption schemes and perfect secrecy following Katz-Lindell, Chapter 2: - `EncScheme`: private-key encryption (Definition 2.1) - `PerfectlySecret`: perfect secrecy (Definition 2.3) - `perfectlySecret_iff_ciphertextIndist`: ciphertext indistinguishability characterization (Lemma 2.5) - `otp`: the one-time pad construction (Construction 2.9) - `otp_perfectlySecret`: the OTP is perfectly secret (Theorem 2.10) - `perfectlySecret_keySpace_ge`: Shannon's theorem, |K| ≥ |M| (Theorem 2.12) For some context, Katz reviewed this in its original home: https://github.com/SamuelSchlesinger/introduction-to-modern-cryptography/pull/1. --- Cslib.lean | 7 + .../Protocols/PerfectSecrecy/Basic.lean | 51 +++++++ .../Crypto/Protocols/PerfectSecrecy/Defs.lean | 84 +++++++++++ .../Protocols/PerfectSecrecy/Encryption.lean | 61 ++++++++ .../PerfectSecrecy/Internal/OneTimePad.lean | 38 +++++ .../Internal/PerfectSecrecy.lean | 131 ++++++++++++++++++ .../Protocols/PerfectSecrecy/OneTimePad.lean | 51 +++++++ .../PerfectSecrecy/PMFUtilities.lean | 90 ++++++++++++ references.bib | 10 ++ 9 files changed, 523 insertions(+) create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean create mode 100644 Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean diff --git a/Cslib.lean b/Cslib.lean index 3e5977af26..ef09e6f16d 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -36,6 +36,13 @@ public import Cslib.Computability.URM.Defs public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine +public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic +public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs +public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption +public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad +public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy +public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad +public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean new file mode 100644 index 0000000000..1b44b97081 --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs +public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy + +@[expose] public section + +/-! +# Perfect Secrecy + +Characterisation theorems for perfect secrecy following +[KatzLindell2020], Chapter 2. + +## Main results + +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_iff_ciphertextIndist`: + ciphertext indistinguishability characterization ([KatzLindell2020], Lemma 2.5) +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.perfectlySecret_keySpace_ge`: + Shannon's theorem, `|K| ≥ |M|` ([KatzLindell2020], Theorem 2.12) + +## References + +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme + +universe u +variable {M K C : Type u} + +/-- A scheme is perfectly secret iff the ciphertext distribution is +independent of the plaintext ([KatzLindell2020], Lemma 2.5). -/ +theorem perfectlySecret_iff_ciphertextIndist (scheme : EncScheme M K C) : + scheme.PerfectlySecret ↔ scheme.CiphertextIndist := + ⟨PerfectSecrecy.ciphertextIndist_of_perfectlySecret scheme, + PerfectSecrecy.perfectlySecret_of_ciphertextIndist scheme⟩ + +/-- Perfect secrecy requires `|K| ≥ |M|` +([KatzLindell2020], Theorem 2.12). -/ +theorem perfectlySecret_keySpace_ge [Finite K] + (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) : + Nat.card K ≥ Nat.card M := + PerfectSecrecy.shannonKeySpace scheme h + +end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean new file mode 100644 index 0000000000..818c4473ae --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption +public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities +public import Mathlib.Probability.ProbabilityMassFunction.Constructions + +@[expose] public section + +/-! +# Perfect Secrecy: Definitions + +Core definitions for perfect secrecy following [KatzLindell2020], Chapter 2. + +## Main definitions + +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.ciphertextDist`: + ciphertext distribution for a given message +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.jointDist`: + joint (message, ciphertext) distribution given a message prior +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.marginalCiphertextDist`: + marginal ciphertext distribution given a message prior +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.posteriorMsgDist`: + posterior message distribution `Pr[M | C = c]` as a `PMF` +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.PerfectlySecret`: + perfect secrecy ([KatzLindell2020], Definition 2.3) +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme.CiphertextIndist`: + ciphertext indistinguishability ([KatzLindell2020], Lemma 2.5) +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme + +universe u +variable {M K C : Type u} + +/-- The distribution of `Enc_K(m)` when `K ← Gen`. -/ +noncomputable def ciphertextDist (scheme : EncScheme M K C) (m : M) : PMF C := do + scheme.enc (← scheme.gen) m + +/-- Joint distribution of `(M, C)` given a message prior. -/ +noncomputable def jointDist (scheme : EncScheme M K C) (msgDist : PMF M) : PMF (M × C) := do + let m ← msgDist + return (m, ← scheme.ciphertextDist m) + +/-- Marginal ciphertext distribution given a message prior. -/ +noncomputable def marginalCiphertextDist (scheme : EncScheme M K C) + (msgDist : PMF M) : PMF C := do + scheme.ciphertextDist (← msgDist) + +/-- The posterior message distribution `Pr[M | C = c]` as a probability +distribution, given a message prior and a ciphertext in the support of +the marginal distribution. -/ +noncomputable def posteriorMsgDist (scheme : EncScheme M K C) + (msgDist : PMF M) (c : C) + (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) : PMF M := + PMFUtilities.posteriorDist msgDist scheme.ciphertextDist c hc + +@[simp] +theorem posteriorMsgDist_apply (scheme : EncScheme M K C) + (msgDist : PMF M) (c : C) + (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support) (m : M) : + scheme.posteriorMsgDist msgDist c hc m = + scheme.jointDist msgDist (m, c) / scheme.marginalCiphertextDist msgDist c := + rfl + +/-- An encryption scheme is perfectly secret if the posterior message +distribution equals the prior for every ciphertext with positive probability +([KatzLindell2020], Definition 2.3). -/ +def PerfectlySecret (scheme : EncScheme M K C) : Prop := + ∀ (msgDist : PMF M) (c : C) + (hc : c ∈ (scheme.marginalCiphertextDist msgDist).support), + scheme.posteriorMsgDist msgDist c hc = msgDist + +/-- Ciphertext indistinguishability: the ciphertext distribution is the same +for all messages ([KatzLindell2020], Lemma 2.5). -/ +def CiphertextIndist (scheme : EncScheme M K C) : Prop := + ∀ m₀ m₁ : M, scheme.ciphertextDist m₀ = scheme.ciphertextDist m₁ + +end Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean new file mode 100644 index 0000000000..543dbab766 --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Probability.ProbabilityMassFunction.Monad + +@[expose] public section + +/-! +# Private-Key Encryption Schemes (Information-Theoretic) + +An information-theoretic private-key encryption scheme following +[KatzLindell2020], Definition 2.1. Key generation and encryption are +probability distributions over arbitrary types, with no computational +constraints. + +## Main definitions + +- `Cslib.Crypto.Protocols.PerfectSecrecy.EncScheme`: + a private-key encryption scheme (Gen, Enc, Dec) with correctness + +## References + +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy + +/-- +A private-key encryption scheme over message space `M`, key space `K`, +and ciphertext space `C` ([KatzLindell2020], Definition 2.1). +-/ +structure EncScheme (Message Key Ciphertext : Type*) where + /-- Probabilistic key generation. -/ + gen : PMF Key + /-- (Possibly randomized) encryption. -/ + enc (key : Key) (message : Message) : PMF Ciphertext + /-- Deterministic decryption. -/ + dec (key : Key) (ciphertext : Ciphertext) : Message + /-- Decryption inverts encryption for all keys in the support of `gen`. -/ + correct : ∀ key, key ∈ gen.support → ∀ message ciphertext, + ciphertext ∈ (enc key message).support → dec key ciphertext = message + +/-- Build an encryption scheme from deterministic pure encryption/decryption +where decryption is a left inverse of encryption for every key. -/ +noncomputable def EncScheme.ofPure.{u} {Message Key Ciphertext : Type u} (gen : PMF Key) + (enc : Key → Message → Ciphertext) (dec : Key → Ciphertext → Message) + (h : ∀ key, Function.LeftInverse (dec key) (enc key)) : + EncScheme Message Key Ciphertext where + gen := gen + enc key message := PMF.pure (enc key message) + dec := dec + correct key _ message _ hc := by + rw [PMF.mem_support_pure_iff] at hc; subst hc; exact h key message + +end Cslib.Crypto.Protocols.PerfectSecrecy diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean new file mode 100644 index 0000000000..c4a1f669c3 --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Probability.Distributions.Uniform + +@[expose] public section + +/-! +# One-Time Pad: Internal proofs + +The OTP ciphertext distribution is uniform regardless of message. +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy.OTP + +-- TODO: upstream to Mathlib as a FinEnum instance for BitVec. +instance bitVecFintype (n : ℕ) : Fintype (BitVec n) := + Fintype.ofEquiv (Fin (2 ^ n)) + ⟨BitVec.ofFin, BitVec.toFin, fun x => by simp, fun x => by simp⟩ + +-- TODO: upstream to Mathlib — general BitVec XOR cancellation lemma. +/-- XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ c ^^^ m = k`. -/ +lemma eq_xor_iff_xor_eq {l : ℕ} (c m k : BitVec l) : + (c = k ^^^ m) ↔ (c ^^^ m = k) := by grind + +/-- The ciphertext distribution of the OTP is uniform, regardless of the message. -/ +theorem otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) : + (PMF.uniformOfFintype (BitVec l)).bind + (fun k => PMF.pure (k ^^^ m)) = + PMF.uniformOfFintype (BitVec l) := by simp [PMF.ext_iff, eq_xor_iff_xor_eq] + +end Cslib.Crypto.Protocols.PerfectSecrecy.OTP diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean new file mode 100644 index 0000000000..e3cc2fa8e7 --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean @@ -0,0 +1,131 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs +public import Mathlib.Probability.Distributions.Uniform + +@[expose] public section + +/-! +# Perfect Secrecy: Internal proofs + +Auxiliary lemmas for perfect secrecy: +- Equivalence of the conditional-probability and independence formulations +- Both directions of the ciphertext indistinguishability characterization + ([KatzLindell2020], Lemma 2.5) +- Shannon's key-space bound ([KatzLindell2020], Theorem 2.12) +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy + +open PMF ENNReal + +universe u +variable {M K C : Type u} + +/-- The joint distribution at `(m, c)` equals `msgDist m * ciphertextDist m c`. -/ +theorem jointDist_eq (scheme : EncScheme M K C) (msgDist : PMF M) + (m : M) (c : C) : + scheme.jointDist msgDist (m, c) = msgDist m * scheme.ciphertextDist m c := + PMFUtilities.bind_pair_apply msgDist scheme.ciphertextDist m c + +/-- Summing the joint distribution over messages gives the marginal ciphertext distribution. -/ +theorem jointDist_tsum_fst (scheme : EncScheme M K C) (msgDist : PMF M) (c : C) : + ∑' m, scheme.jointDist msgDist (m, c) = scheme.marginalCiphertextDist msgDist c := + PMFUtilities.bind_pair_tsum_fst msgDist scheme.ciphertextDist c + +/-- Perfect secrecy is equivalent to message-ciphertext independence. +The two formulations are related by multiplying/dividing by `marginal(c)`. -/ +theorem perfectlySecret_iff_indep (scheme : EncScheme M K C) : + scheme.PerfectlySecret ↔ + ∀ (msgDist : PMF M) (m : M) (c : C), + scheme.jointDist msgDist (m, c) = + msgDist m * scheme.marginalCiphertextDist msgDist c := by + constructor + · intro h msgDist m c + by_cases hc : (scheme.marginalCiphertextDist msgDist) c = 0 + · have := ENNReal.tsum_eq_zero.mp + ((jointDist_tsum_fst scheme msgDist c).trans hc) m + rw [this, hc, mul_zero] + · have hne_top := ne_top_of_le_ne_top one_ne_top + (PMF.coe_le_one (scheme.marginalCiphertextDist msgDist) c) + have := DFunLike.congr_fun (h msgDist c ((PMF.mem_support_iff _ _).mpr hc)) m + simp only [EncScheme.posteriorMsgDist_apply] at this + rw [← this, ENNReal.div_mul_cancel hc hne_top] + · intro h msgDist c hc; ext m + simp only [EncScheme.posteriorMsgDist_apply] + rw [h msgDist m c, ENNReal.mul_div_cancel_right + ((PMF.mem_support_iff _ _).mp hc) + (ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one _ c))] + +/-- Ciphertext indistinguishability implies message-ciphertext independence. -/ +theorem indep_of_ciphertextIndist (scheme : EncScheme M K C) + (h : scheme.CiphertextIndist) + (msgDist : PMF M) (m : M) (c : C) : + scheme.jointDist msgDist (m, c) = + msgDist m * scheme.marginalCiphertextDist msgDist c := by + rw [jointDist_eq]; congr 1 + change scheme.ciphertextDist m c = + PMF.bind msgDist (fun m' => scheme.ciphertextDist m') c + rw [PMF.bind_apply] + conv_rhs => arg 1; ext m'; rw [h m' m] + rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + +/-- Ciphertext indistinguishability implies perfect secrecy. -/ +theorem perfectlySecret_of_ciphertextIndist (scheme : EncScheme M K C) + (h : scheme.CiphertextIndist) : + scheme.PerfectlySecret := + (perfectlySecret_iff_indep scheme).mpr (fun msgDist m c => + indep_of_ciphertextIndist scheme h msgDist m c) + +/-- Perfect secrecy implies ciphertext indistinguishability. -/ +theorem ciphertextIndist_of_perfectlySecret (scheme : EncScheme M K C) + (h : scheme.PerfectlySecret) : + scheme.CiphertextIndist := by + classical + rw [perfectlySecret_iff_indep] at h + intro m₀ m₁; ext c + have hs : ({m₀, m₁} : Finset M).Nonempty := ⟨m₀, Finset.mem_insert_self ..⟩ + set μ := PMF.uniformOfFinset _ hs + suffices key : ∀ m ∈ ({m₀, m₁} : Finset M), + scheme.ciphertextDist m c = scheme.marginalCiphertextDist μ c by + exact (key m₀ (by simp)).trans (key m₁ (by simp)).symm + intro m hm + have hne := (PMF.mem_support_uniformOfFinset_iff hs m).mpr hm + have hne_top := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one μ m) + exact (ENNReal.mul_right_inj hne hne_top).mp (by rw [← jointDist_eq]; exact h μ m c) + +/-- If each message maps to a key that encrypts it to a common ciphertext, +then the key assignment is injective (by correctness of decryption). -/ +lemma encrypt_key_injective (scheme : EncScheme M K C) + (f : M → K) (c₀ : C) + (hf_mem : ∀ m, f m ∈ scheme.gen.support) + (hf_enc : ∀ m, c₀ ∈ (scheme.enc (f m) m).support) : + Function.Injective f := + fun m₁ m₂ heq => + (scheme.correct _ (hf_mem m₁) m₁ c₀ (hf_enc m₁)).symm.trans + (heq ▸ scheme.correct _ (hf_mem m₂) m₂ c₀ (hf_enc m₂)) + +/-- Perfect secrecy requires `|K| ≥ |M|` (Shannon's theorem). -/ +theorem shannonKeySpace [Finite K] + (scheme : EncScheme M K C) (h : scheme.PerfectlySecret) : + Nat.card K ≥ Nat.card M := by + classical + have hci := ciphertextIndist_of_perfectlySecret scheme h + by_cases hM : IsEmpty M; · simp + obtain ⟨m₀⟩ := not_isEmpty_iff.mp hM + obtain ⟨c₀, hc₀⟩ := (scheme.ciphertextDist m₀).support_nonempty + have key_exists : ∀ m, ∃ k ∈ scheme.gen.support, c₀ ∈ (scheme.enc k m).support := by + intro m + exact (PMF.mem_support_bind_iff _ _ _).mp + (show c₀ ∈ (scheme.ciphertextDist m).support by rw [hci m m₀]; exact hc₀) + choose f hf_mem hf_enc using key_exists + exact Nat.card_le_card_of_injective f + (encrypt_key_injective scheme f c₀ hf_mem hf_enc) + +end Cslib.Crypto.Protocols.PerfectSecrecy diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean new file mode 100644 index 0000000000..aeb09bb20b --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic +public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad +public import Mathlib.Probability.Distributions.Uniform + +@[expose] public section + +/-! +# One-Time Pad + +The one-time pad (Vernam cipher) over `BitVec l` +([KatzLindell2020], Construction 2.9). + +## Main definitions + +- `Cslib.Crypto.Protocols.PerfectSecrecy.otp`: the one-time pad encryption scheme + +## Main results + +- `Cslib.Crypto.Protocols.PerfectSecrecy.otp_perfectlySecret`: + the one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10) + +## References + +* [J. Katz, Y. Lindell, *Introduction to Modern Cryptography*][KatzLindell2020] +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy + +/-- The one-time pad over `l`-bit strings. Encryption and decryption +are XOR ([KatzLindell2020], Construction 2.9). -/ +noncomputable def otp (l : ℕ) : + EncScheme (BitVec l) (BitVec l) (BitVec l) := + .ofPure (PMF.uniformOfFintype _) (· ^^^ ·) (· ^^^ ·) fun k m => by + simp [← BitVec.xor_assoc] + +/-- The one-time pad is perfectly secret ([KatzLindell2020], Theorem 2.10). -/ +theorem otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret := + (EncScheme.perfectlySecret_iff_ciphertextIndist _).mpr fun m₀ m₁ => by + simp only [EncScheme.ciphertextDist, otp] + exact (OTP.otp_ciphertextDist_eq_uniform l m₀).trans + (OTP.otp_ciphertextDist_eq_uniform l m₁).symm + +end Cslib.Crypto.Protocols.PerfectSecrecy diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean new file mode 100644 index 0000000000..3980e3e890 --- /dev/null +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/PMFUtilities.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Probability.ProbabilityMassFunction.Monad + +@[expose] public section + +/-! +# PMF Utilities + +## NB: This module is temporary + +Everything here is a general PMF bind/pure lemma with no dependence on +any domain-specific structure. It should be upstreamed to Mathlib +(likely `Mathlib.Probability.ProbabilityMassFunction.Monad` or a new +`Mathlib.Probability.ProbabilityMassFunction.Prod`). Once accepted +upstream, this file should be deleted and its consumers should import +the Mathlib module instead. + +## Main results + +- `PMFUtilities.bind_pair_apply`: the "pairing" bind at `(a, b)` equals `p a * f a b` +- `PMFUtilities.bind_pair_tsum_fst`: marginalizing over the first component +- `PMFUtilities.posterior_hasSum`: posterior probabilities sum to 1 +- `PMFUtilities.posteriorDist`: the posterior as a `PMF` +-/ + +namespace Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities + +open PMF ENNReal + +universe u +variable {α β : Type u} + +/-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)` +gives the product `p a * f a b`. -/ +theorem bind_pair_apply (p : PMF α) (f : α → PMF β) (a : α) (b : β) : + (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) = p a * f a b := by + rw [PMF.bind_apply, tsum_eq_single a] + · rw [PMF.bind_apply]; congr 1; rw [tsum_eq_single b] + · simp [PMF.pure_apply] + · intro b' hb'; simp [PMF.pure_apply, hb'.symm] + · intro a' ha'; rw [PMF.bind_apply]; simp [PMF.pure_apply, ha'.symm] + +/-- Summing the pairing bind over the first component gives the marginal. -/ +theorem bind_pair_tsum_fst (p : PMF α) (f : α → PMF β) (b : β) : + ∑' a, (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) = + (p.bind f) b := by + simp_rw [bind_pair_apply, PMF.bind_apply] + +/-- Posterior probabilities `joint(a, b) / marginal(b)` sum to 1 +when `b` is in the support of the marginal. -/ +theorem posterior_hasSum (p : PMF α) (f : α → PMF β) (b : β) + (hb : b ∈ (p.bind f).support) : + HasSum (fun a => + (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) / + (p.bind f) b) 1 := by + have hne := (PMF.mem_support_iff _ _).mp hb + have hne_top := ne_top_of_le_ne_top one_ne_top (PMF.coe_le_one (p.bind f) b) + have : ∑' a, (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) / + (p.bind f) b = 1 := by + simp only [div_eq_mul_inv] + rw [ENNReal.tsum_mul_right, bind_pair_tsum_fst] + exact ENNReal.mul_inv_cancel hne hne_top + exact this ▸ ENNReal.summable.hasSum + +/-- The posterior distribution `Pr[A = a | B = b]` as a `PMF`, +given `a ← p`, `b ← f a`, and that `b` has positive marginal probability. -/ +noncomputable def posteriorDist (p : PMF α) (f : α → PMF β) (b : β) + (hb : b ∈ (p.bind f).support) : PMF α := + ⟨fun a => + (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) / + (p.bind f) b, + posterior_hasSum p f b hb⟩ + +@[simp] +theorem posteriorDist_apply (p : PMF α) (f : α → PMF β) (b : β) + (hb : b ∈ (p.bind f).support) (a : α) : + posteriorDist p f b hb a = + (p.bind fun a' => (f a').bind fun b' => PMF.pure (a', b')) (a, b) / + (p.bind f) b := + rfl + +end Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities diff --git a/references.bib b/references.bib index 2cccb928f5..1f8c0dc518 100644 --- a/references.bib +++ b/references.bib @@ -123,6 +123,16 @@ @article{ Hennessy1985 bibsource = {dblp computer science bibliography, https://dblp.org} } +@book{ KatzLindell2020, + author = {Jonathan Katz and + Yehuda Lindell}, + title = {Introduction to Modern Cryptography}, + edition = {3rd}, + publisher = {CRC Press}, + year = {2020}, + isbn = {9780815354369} +} + @inproceedings{ Kiselyov2015, author = {Kiselyov, Oleg and Ishii, Hiromi}, title = {Freer Monads, More Extensible Effects}, From 95fdc7dc863ff83e9d6c3a68fcb2505540462a4d Mon Sep 17 00:00:00 2001 From: Garmelon Date: Sat, 18 Apr 2026 14:54:35 +0200 Subject: [PATCH 12/18] chore: bump toolchain to v4.30.0-rc2 (#496) Co-authored-by: Chris Henson --- .github/workflows/lean_action_ci.yml | 6 ++--- Cslib/Foundations/Data/Relation.lean | 2 +- .../CombinatoryLogic/Confluence.lean | 8 ++---- lake-manifest.json | 26 +++++++++---------- lean-toolchain | 2 +- 5 files changed, 20 insertions(+), 24 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 1053d8a537..7e1d5d7ba0 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -34,6 +34,6 @@ jobs: run: | set -e lake exe checkInitImports - - uses: leanprover-community/lint-style-action@main - with: - mode: check + #- uses: leanprover-community/lint-style-action@main + # with: + # mode: check diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index b969bf9c22..3e117dc738 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -200,7 +200,7 @@ def trans_of_subrelation_right (s r : α → α → Prop) (hr : IsTrans α r) /-- Confluence implies that multi-step joinability is an equivalence. -/ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) : Equivalence (Join (ReflTransGen r)) := by - apply equivalence_join reflexive_reflTransGen inferInstance + apply equivalence_join grind /-- A relation is terminating when the inverse of its transitive closure is well-founded. diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index d2553421b6..0ca7fcf162 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -93,13 +93,9 @@ theorem reflTransGen_parallelReduction_mRed : ext a b constructor · apply Relation.reflTransGen_of_isTrans_reflexive - · exact Relation.reflexive_reflTransGen - · infer_instance - · exact @mRed_of_parallelReduction + exact @mRed_of_parallelReduction · apply Relation.reflTransGen_of_isTrans_reflexive - · exact Relation.reflexive_reflTransGen - · infer_instance - · exact fun a a' h => Relation.ReflTransGen.single (parallelReduction_of_red h) + exact fun a a' h => Relation.ReflTransGen.single (parallelReduction_of_red h) /-! Irreducibility for the (partially applied) primitive combinators. diff --git a/lake-manifest.json b/lake-manifest.json index d9898a180a..c2af358d22 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3d8100bbc657181d1f48868decaba9159580aa40", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a3b459a8312125758e51c354b93d54ba620efda6", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4411c5f89c797401c609b3a946c8874569e69731", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,50 +45,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.97", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf597c77bf9b8e66720d724928207f5911533113", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lean-toolchain b/lean-toolchain index 2210cba4ff..6c7e31fffe 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc1 +leanprover/lean4:v4.30.0-rc2 From f57bb82a750c5d3dac3d4f7ed0c5e164a3f4f6c0 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 18 Apr 2026 18:08:59 +0200 Subject: [PATCH 13/18] Function view for tapes. --- Cslib/Foundations/Data/BiTape.lean | 95 +++++++++++++++++++++++++++ Cslib/Foundations/Data/StackTape.lean | 36 ++++++++++ 2 files changed, 131 insertions(+) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index de7a9c8fa2..91730dccbb 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -78,6 +78,31 @@ def mk₁ (l : List Symbol) : BiTape Symbol := | [] => ∅ | h :: t => { head := some h, left := ∅, right := StackTape.map_some t } +/-- Returns the tape symbol at positon `p` relative to the head, where +positive numbers are right of the head and negative are left of the head. -/ +def get (t : BiTape Symbol) : ℤ → Option Symbol + | Int.ofNat 0 => t.head + | Int.ofNat (Nat.succ p') => t.right.toList[p']?.getD none + | Int.negSucc p' => t.left.toList[p']?.getD none + +/-- Two tapes are equal if and only if their `get` functions are equal. This allows to view +tapes as functions `ℤ → Option Symbol`. -/ +lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : + t₁ = t₂ := by + obtain ⟨head₁, left₁, right₁⟩ := t₁ + obtain ⟨head₂, left₂, right₂⟩ := t₂ + have h_head : head₁ = head₂ := by simpa [get] using h_get_eq 0 + have h_right : right₁ = right₂ := by + apply StackTape.ext_get + intro p + simpa [get] using h_get_eq p.succ + have h_left : left₁ = left₂ := by + apply StackTape.ext_get + intro p + simpa [get] using h_get_eq (Int.negSucc p) + simp only [h_head, h_left, h_right] + + section Move /-- @@ -114,6 +139,66 @@ lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := b lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by simp [move_left, move_right] +/-- Translate an optional direction into a head movement offset, where the positive +direction is to the right. -/ +def optionDirToInt (d : Option Dir) : ℤ := + match d with + | none => 0 + | some .left => -1 + | some .right => 1 + +@[simp] +lemma get_move_left (t : BiTape Symbol) (p : ℤ) : + (t.move_left).get p = t.get (p - 1) := by + unfold move_left get + match p with + | Int.ofNat 0 => + rw [show Int.ofNat 0 - 1 = Int.negSucc 0 from rfl] + simp [StackTape.head_eq_getD] + | Int.ofNat 1 => simp + | Int.ofNat (n + 2) => + rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) from by grind] + simp + | Int.negSucc n => simp + +@[simp] +lemma get_move_right (t : BiTape Symbol) (p : ℤ) : + (t.move_right).get p = t.get (p + 1) := by + unfold move_right get + match p with + | Int.ofNat n => + rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) from by grind] + cases n <;> simp [StackTape.head_eq_getD] + | Int.negSucc 0 => simp + | Int.negSucc (n + 1) => + rw [show Int.negSucc (n + 1) + 1 = Int.negSucc n from rfl] + simp + +@[simp] +lemma get_optionMove (t : BiTape Symbol) (d : Option Dir) (p : ℤ) : + (t.optionMove d).get p = t.get (p + optionDirToInt d) := by + unfold optionMove optionDirToInt + cases d with + | none => simp + | some d => + cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] + +@[simp] +lemma get_move_right_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : + (move_right^[n] t).get p = t.get (p + n):= by + induction n generalizing t p with + | zero => simp + | succ n ih => simp [Function.iterate_succ_apply, ih, Int.add_assoc] + +@[simp] +lemma get_move_left_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : + (move_left^[n] t).get p = t.get (p - n):= by + induction n generalizing t p with + | zero => simp + | succ n ih => + have : p - n - 1 = p - (n + 1) := by grind + simp [Function.iterate_succ_apply, ih, this] + end Move /-- @@ -121,6 +206,16 @@ Write a value under the head of the `BiTape`. -/ def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } +@[simp] +lemma get_write (t : BiTape Symbol) (a : Option Symbol) : + (t.write a).get = Function.update t.get 0 a := by + unfold write get Function.update + funext p + match p with + | Int.ofNat 0 => simp + | Int.ofNat (n + 1) => simp; grind + | Int.negSucc n => simp + /-- The space used by a `BiTape` is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`. diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 049d52a195..e64758dba8 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -106,6 +106,25 @@ def head (l : StackTape Symbol) : Option Symbol := | [] => none | h :: _ => h +lemma head_eq_getD (s : StackTape Symbol) : + s.head = s.toList[0]?.getD none := by + unfold head; cases s.toList <;> simp + +@[simp] +lemma tail_getD (s : StackTape Symbol) (n : ℕ) : + s.tail.toList[n]?.getD none = s.toList[n + 1]?.getD none := by + cases s with | mk l h => cases l <;> simp [tail, nil] + +@[simp] +lemma cons_getD_zero (x : Option Symbol) (s : StackTape Symbol) : + (cons x s).toList[0]?.getD none = x := by + cases x <;> (cases s with | mk l h => cases l <;> simp [cons]) + +@[simp] +lemma cons_getD_succ (x : Option Symbol) (s : StackTape Symbol) (n : ℕ) : + (cons x s).toList[n + 1]?.getD none = s.toList[n]?.getD none := by + cases x <;> (cases s with | mk l h => cases l <;> simp [cons]) + lemma eq_iff (l1 l2 : StackTape Symbol) : l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by constructor @@ -115,6 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) : cases l2 with | mk as2 h2 => cases as1 <;> cases as2 <;> grind +lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : + t₁ = t₂ := by + obtain ⟨t₁, h₁⟩ := t₁ + obtain ⟨t₂, h₂⟩ := t₂ + simpa using h_toList_eq + +lemma ext_get (t₁ t₂ : StackTape Symbol) + (h_get_eq : ∀ p, t₁.toList.getD p none = t₂.toList.getD p none) : + t₁ = t₂ := by + apply ext + obtain ⟨l₁, h₁⟩ := t₁ + obtain ⟨l₂, h₂⟩ := t₂ + simp only [List.getD_eq_getElem?_getD] at h_get_eq + have hlen : l₁.length = l₂.length := by grind + apply List.ext_getElem hlen + grind + @[simp] lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o := by cases o with From e1d2527e9b2ebab97703e05568b9ed887b8d3f0b Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 18 Apr 2026 21:02:11 +0200 Subject: [PATCH 14/18] Use head positions to define space requirement. --- .../Machines/SingleTapeTuring/Basic.lean | 77 ++++++++++++++++--- 1 file changed, 66 insertions(+), 11 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 4d37134ac1..4284a4ca2d 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -132,18 +132,23 @@ structure Cfg : Type where BiTape : BiTape Symbol deriving Inhabited +/-- The value of the transition function (i.e. the statement and the successor state, if any) +applied to a configuration of the Turing machine. +If the configuration is in the halting state, returns `none`. -/ +abbrev transitionValue : tm.Cfg → Option (Stmt Symbol × Option tm.State) + -- If in the halting state, there is nothing to do any more. + | ⟨none, _⟩ => none + -- If in state q, perform look up in the transition function + | ⟨some q, t⟩ => some (tm.tr q t.head) + /-- The step function corresponding to a `SingleTapeTM`. -/ @[simp] -def step : tm.Cfg → Option tm.Cfg - | ⟨none, _⟩ => - -- If in the halting state, there is no next configuration - none - | ⟨some q', t⟩ => - -- If in state q', perform look up in the transition function - match tm.tr q' t.head with - -- and enter a new configuration with state q'' (or none for halting) - -- and tape updated according to the Stmt - | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ +def step (cfg : tm.Cfg) : Option tm.Cfg := do + -- If the transition function has a value on the current configuration + let ⟨⟨wr, dir⟩, q'⟩ ← tm.transitionValue cfg + -- enter a new configuration with state q'' (or none for halting) + -- and tape updated according to the Stmt + return ⟨q', (cfg.BiTape.write wr).optionMove dir⟩ /-- The initial configuration corresponding to a list in the input alphabet. @@ -188,6 +193,56 @@ open Cfg variable [Inhabited Symbol] [Fintype Symbol] +/-- The sequence of configurations of the Turing machine `tm` starting from configuration `c`. +After the sequence has reached a configuration in the halting state, it turns +`none` and stays `none`. -/ +def configs (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : (Option tm.Cfg) := + (Option.bind · tm.step)^[t] (some c) + +def optionDirToInt : Option Dir → ℤ + | none => 0 + | some .left => -1 + | some .right => 1 + +/-- The next movement of the tape head when in configuration `c`, as an integer. -/ +def headMovement (tm : SingleTapeTM Symbol) (c : tm.Cfg) : ℤ := + match tm.transitionValue c with + | none => 0 + | some ⟨⟨_, dir⟩, _⟩ => optionDirToInt dir + +/-- The sequence of positions of the tape head starting from configuration `c`, +relative to the initial position of zero, at the beginning of step `t`. -/ +def headPosition (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : ℤ := + ∑ t' : Fin t, ((tm.configs c t').map fun c => tm.headMovement c).getD 0 + +/-- The tape of machine `tm` at the start of step `t` as a function `ℤ → Option Symbol` +that does not "move" with the head. I.e. regardless of `t`, the symbol at zero is always +the symbol in the same tape cell. -/ +def fixedTape (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : Option (ℤ → Option Symbol) := + (tm.configs c t).map fun cfg p => cfg.BiTape.get (p + tm.headPosition c t) + +/-- The space used by machine `tm` when starting in configuration `c` and executing for `t` steps, +defined as the number of cells visited by the tape head. -/ +def spaceUsed (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : ℤ := + 1 + (List.ofFn (n := t.succ) (tm.headPosition c ·)).max (by simp) - + (List.ofFn (n := t.succ) (tm.headPosition c ·)).min (by simp) + +lemma only_modification_at_headPosition (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) (i : ℤ) + (h_next : (tm.fixedTape c (t + 1)).isSome = true) + -- the next one should not be needed + (h_next_next : (tm.fixedTape c t).isSome = true) + (h_noHead : i ≠ tm.headPosition c t) : + (tm.fixedTape c (t + 1)).get h_next i = (tm.fixedTape c t).get h_next_next i := by + unfold fixedTape + simp + have h_c : tm.configs c (t + 1) = (tm.configs c t).bind tm.step := by + simp [configs, Function.iterate_succ_apply'] + rw [h_c] + + -- rw [h_c] + + sorry + /-- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` is defined by the `step` function, @@ -318,7 +373,7 @@ private theorem map_toCompCfg_right_step : | mk state BiTape => cases state with | none => - simp only [step, toCompCfg_right, Option.map_none, compComputer] + simp [step, toCompCfg_right, compComputer] | some q => generalize hM : tm2.tr q BiTape.head = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result From 642162c56369302365a23c8e2507fe9d164355e8 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 11:38:51 +0200 Subject: [PATCH 15/18] Apply suggestions from code review Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Foundations/Data/BiTape.lean | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 91730dccbb..c2621771de 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -78,12 +78,13 @@ def mk₁ (l : List Symbol) : BiTape Symbol := | [] => ∅ | h :: t => { head := some h, left := ∅, right := StackTape.map_some t } +open scoped Int in /-- Returns the tape symbol at positon `p` relative to the head, where positive numbers are right of the head and negative are left of the head. -/ def get (t : BiTape Symbol) : ℤ → Option Symbol - | Int.ofNat 0 => t.head - | Int.ofNat (Nat.succ p') => t.right.toList[p']?.getD none - | Int.negSucc p' => t.left.toList[p']?.getD none + | 0 => t.head + | (p' + 1 : Nat) => t.right.toList[p']?.getD none + | -[p'+1] => t.left.toList[p']?.getD none /-- Two tapes are equal if and only if their `get` functions are equal. This allows to view tapes as functions `ℤ → Option Symbol`. -/ @@ -95,7 +96,7 @@ lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.g have h_right : right₁ = right₂ := by apply StackTape.ext_get intro p - simpa [get] using h_get_eq p.succ + simpa [get] using h_get_eq (p + 1) have h_left : left₁ = left₂ := by apply StackTape.ext_get intro p @@ -157,7 +158,7 @@ lemma get_move_left (t : BiTape Symbol) (p : ℤ) : simp [StackTape.head_eq_getD] | Int.ofNat 1 => simp | Int.ofNat (n + 2) => - rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) from by grind] + rw [show Int.ofNat (n + 2) - 1 = Int.ofNat (n + 1) by lia] simp | Int.negSucc n => simp @@ -167,7 +168,7 @@ lemma get_move_right (t : BiTape Symbol) (p : ℤ) : unfold move_right get match p with | Int.ofNat n => - rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) from by grind] + rw [show Int.ofNat n + 1 = Int.ofNat (n + 1) by lia] cases n <;> simp [StackTape.head_eq_getD] | Int.negSucc 0 => simp | Int.negSucc (n + 1) => @@ -196,7 +197,7 @@ lemma get_move_left_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : induction n generalizing t p with | zero => simp | succ n ih => - have : p - n - 1 = p - (n + 1) := by grind + have : p - n - 1 = p - (n + 1) := by lia simp [Function.iterate_succ_apply, ih, this] end Move @@ -213,7 +214,7 @@ lemma get_write (t : BiTape Symbol) (a : Option Symbol) : funext p match p with | Int.ofNat 0 => simp - | Int.ofNat (n + 1) => simp; grind + | Int.ofNat (n + 1) => grind | Int.negSucc n => simp /-- From be6855a82b58c4690c37837976eb4c44dc22469b Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 13:07:33 +0200 Subject: [PATCH 16/18] Simplify some proofs and add annotations. --- Cslib/Foundations/Data/BiTape.lean | 25 +++++++++---------- Cslib/Foundations/Data/StackTape.lean | 35 +++++++++++---------------- 2 files changed, 26 insertions(+), 34 deletions(-) diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index c2621771de..74c6a8190b 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -81,6 +81,7 @@ def mk₁ (l : List Symbol) : BiTape Symbol := open scoped Int in /-- Returns the tape symbol at positon `p` relative to the head, where positive numbers are right of the head and negative are left of the head. -/ +@[scoped grind] def get (t : BiTape Symbol) : ℤ → Option Symbol | 0 => t.head | (p' + 1 : Nat) => t.right.toList[p']?.getD none @@ -88,8 +89,8 @@ def get (t : BiTape Symbol) : ℤ → Option Symbol /-- Two tapes are equal if and only if their `get` functions are equal. This allows to view tapes as functions `ℤ → Option Symbol`. -/ -lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : - t₁ = t₂ := by +@[ext] +lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.get p) : t₁ = t₂ := by obtain ⟨head₁, left₁, right₁⟩ := t₁ obtain ⟨head₂, left₂, right₂⟩ := t₂ have h_head : head₁ = head₂ := by simpa [get] using h_get_eq 0 @@ -101,7 +102,7 @@ lemma ext_get (t₁ t₂ : BiTape Symbol) (h_get_eq : ∀ p, t₁.get p = t₂.g apply StackTape.ext_get intro p simpa [get] using h_get_eq (Int.negSucc p) - simp only [h_head, h_left, h_right] + grind section Move @@ -142,13 +143,14 @@ lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := b /-- Translate an optional direction into a head movement offset, where the positive direction is to the right. -/ +@[scoped grind] def optionDirToInt (d : Option Dir) : ℤ := match d with | none => 0 | some .left => -1 | some .right => 1 -@[simp] +@[simp, scoped grind =] lemma get_move_left (t : BiTape Symbol) (p : ℤ) : (t.move_left).get p = t.get (p - 1) := by unfold move_left get @@ -162,7 +164,7 @@ lemma get_move_left (t : BiTape Symbol) (p : ℤ) : simp | Int.negSucc n => simp -@[simp] +@[simp, scoped grind =] lemma get_move_right (t : BiTape Symbol) (p : ℤ) : (t.move_right).get p = t.get (p + 1) := by unfold move_right get @@ -175,23 +177,20 @@ lemma get_move_right (t : BiTape Symbol) (p : ℤ) : rw [show Int.negSucc (n + 1) + 1 = Int.negSucc n from rfl] simp -@[simp] +@[simp, scoped grind =] lemma get_optionMove (t : BiTape Symbol) (d : Option Dir) (p : ℤ) : (t.optionMove d).get p = t.get (p + optionDirToInt d) := by unfold optionMove optionDirToInt - cases d with - | none => simp - | some d => - cases d <;> simp [move, show p + (-1 : ℤ) = p - 1 from by omega] + grind [move] -@[simp] +@[simp, scoped grind =] lemma get_move_right_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : (move_right^[n] t).get p = t.get (p + n):= by induction n generalizing t p with | zero => simp | succ n ih => simp [Function.iterate_succ_apply, ih, Int.add_assoc] -@[simp] +@[simp, scoped grind =] lemma get_move_left_iterate (t : BiTape Symbol) (n : ℕ) (p : ℤ) : (move_left^[n] t).get p = t.get (p - n):= by induction n generalizing t p with @@ -207,7 +206,7 @@ Write a value under the head of the `BiTape`. -/ def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } -@[simp] +@[simp, scoped grind =] lemma get_write (t : BiTape Symbol) (a : Option Symbol) : (t.write a).get = Function.update t.get 0 a := by unfold write get Function.update diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index e64758dba8..add0b18edf 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -106,21 +106,21 @@ def head (l : StackTape Symbol) : Option Symbol := | [] => none | h :: _ => h -lemma head_eq_getD (s : StackTape Symbol) : - s.head = s.toList[0]?.getD none := by +@[scoped grind =] +lemma head_eq_getD (s : StackTape Symbol) : s.head = s.toList[0]?.getD none := by unfold head; cases s.toList <;> simp -@[simp] -lemma tail_getD (s : StackTape Symbol) (n : ℕ) : - s.tail.toList[n]?.getD none = s.toList[n + 1]?.getD none := by +@[simp, scoped grind =] +lemma tail_getElem? (s : StackTape Symbol) (n : ℕ) : + s.tail.toList[n]? = s.toList[n + 1]? := by cases s with | mk l h => cases l <;> simp [tail, nil] -@[simp] +@[simp, scoped grind =] lemma cons_getD_zero (x : Option Symbol) (s : StackTape Symbol) : (cons x s).toList[0]?.getD none = x := by cases x <;> (cases s with | mk l h => cases l <;> simp [cons]) -@[simp] +@[simp, scoped grind =] lemma cons_getD_succ (x : Option Symbol) (s : StackTape Symbol) (n : ℕ) : (cons x s).toList[n + 1]?.getD none = s.toList[n]?.getD none := by cases x <;> (cases s with | mk l h => cases l <;> simp [cons]) @@ -134,30 +134,23 @@ lemma eq_iff (l1 l2 : StackTape Symbol) : cases l2 with | mk as2 h2 => cases as1 <;> cases as2 <;> grind -lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : - t₁ = t₂ := by +@[ext] +lemma ext (t₁ t₂ : StackTape Symbol) (h_toList_eq : t₁.toList = t₂.toList) : t₁ = t₂ := by obtain ⟨t₁, h₁⟩ := t₁ obtain ⟨t₂, h₂⟩ := t₂ simpa using h_toList_eq +@[ext] lemma ext_get (t₁ t₂ : StackTape Symbol) - (h_get_eq : ∀ p, t₁.toList.getD p none = t₂.toList.getD p none) : - t₁ = t₂ := by - apply ext + (h_get_eq : ∀ p : ℕ, t₁.toList[p]?.getD none = t₂.toList[p]?.getD none) : + t₁ = t₂ := by obtain ⟨l₁, h₁⟩ := t₁ obtain ⟨l₂, h₂⟩ := t₂ - simp only [List.getD_eq_getElem?_getD] at h_get_eq - have hlen : l₁.length = l₂.length := by grind - apply List.ext_getElem hlen - grind + grind [List.ext_getElem] @[simp] lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o := by - cases o with - | none => - cases l with | mk toList hl => - cases toList <;> grind - | some a => grind + grind @[simp] lemma tail_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).tail = l := by From e6d0067398b6a3a3095b635630e6e5dcbfe6bf76 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 16:42:13 +0200 Subject: [PATCH 17/18] helper lemmas --- .../Machines/SingleTapeTuring/Basic.lean | 59 ++++++++++++++----- 1 file changed, 45 insertions(+), 14 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 4284a4ca2d..55c8d22965 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -199,6 +199,25 @@ After the sequence has reached a configuration in the halting state, it turns def configs (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : (Option tm.Cfg) := (Option.bind · tm.step)^[t] (some c) +@[simp, grind =] +lemma configs_isSome_of_succ_isSome (tm : SingleTapeTM Symbol) (init : tm.Cfg) + (t : ℕ) (h_some : (tm.configs init (t + 1)).isSome) : + (tm.configs init t).isSome := by + unfold configs + sorry + +/-- Once the sequence of configurations reaches `none`, it stays `none`. -/ +lemma configs_isNone_mono (tm : SingleTapeTM Symbol) (init : tm.Cfg) + (t₁ t₂ : ℕ) (h_le : t₁ ≤ t₂) (h_some : (tm.configs init t₂).isSome) : + Monotone (fun t => (tm.configs init t).isNone) := by + unfold configs + intro t₁ t₂ h_le + induction t₂ with + | zero => grind [Function.iterate_zero] + | succ t₁' ih => + simp only [Function.iterate_succ_apply'] + sorry + def optionDirToInt : Option Dir → ℤ | none => 0 | some .left => -1 @@ -213,13 +232,24 @@ def headMovement (tm : SingleTapeTM Symbol) (c : tm.Cfg) : ℤ := /-- The sequence of positions of the tape head starting from configuration `c`, relative to the initial position of zero, at the beginning of step `t`. -/ def headPosition (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : ℤ := - ∑ t' : Fin t, ((tm.configs c t').map fun c => tm.headMovement c).getD 0 + ∑ t' : Fin t, ((tm.configs c t').map tm.headMovement).getD 0 + +@[simp, scoped grind =] +lemma headPosition_succ (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : + tm.headPosition c (t + 1) = + tm.headPosition c t + (((tm.configs c t).map tm.headMovement).getD 0) := by + sorry /-- The tape of machine `tm` at the start of step `t` as a function `ℤ → Option Symbol` that does not "move" with the head. I.e. regardless of `t`, the symbol at zero is always the symbol in the same tape cell. -/ def fixedTape (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : Option (ℤ → Option Symbol) := - (tm.configs c t).map fun cfg p => cfg.BiTape.get (p + tm.headPosition c t) + (tm.configs c t).map fun cfg p => cfg.BiTape.get (p - tm.headPosition c t) + +@[simp, scoped grind =] +lemma fixedTape_isSome_of_succ_isSome (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) + (h_isSome : (tm.fixedTape c (t + 1)).isSome) : + (tm.fixedTape c t).isSome := by sorry /-- The space used by machine `tm` when starting in configuration `c` and executing for `t` steps, defined as the number of cells visited by the tape head. -/ @@ -227,21 +257,22 @@ def spaceUsed (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : ℤ := 1 + (List.ofFn (n := t.succ) (tm.headPosition c ·)).max (by simp) - (List.ofFn (n := t.succ) (tm.headPosition c ·)).min (by simp) -lemma only_modification_at_headPosition (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) (i : ℤ) - (h_next : (tm.fixedTape c (t + 1)).isSome = true) - -- the next one should not be needed - (h_next_next : (tm.fixedTape c t).isSome = true) - (h_noHead : i ≠ tm.headPosition c t) : - (tm.fixedTape c (t + 1)).get h_next i = (tm.fixedTape c t).get h_next_next i := by +lemma only_modification_at_headPosition (tm : SingleTapeTM Symbol) (init : tm.Cfg) (t : ℕ) (i : ℤ) + (h_next : (tm.fixedTape init (t + 1)).isSome) + (h_noHead : i ≠ tm.headPosition init t) : + (tm.fixedTape init (t + 1)).get h_next i = (tm.fixedTape init t).get (by grind) i := by unfold fixedTape simp - have h_c : tm.configs c (t + 1) = (tm.configs c t).bind tm.step := by + have h_configs_some : (tm.configs init t).isSome := by sorry + have h_c : tm.configs init (t + 1) = (tm.configs init t).bind tm.step := by simp [configs, Function.iterate_succ_apply'] - rw [h_c] - - -- rw [h_c] - - sorry + simp [h_c, Option.get_bind] + simp [Function.update] + split_ifs + · simp [transitionValue] + sorry + · simp [transitionValue] + sorry /-- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol` From 7a815041546fd8ee8674095d4503359c85f21bb8 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Apr 2026 21:44:07 +0200 Subject: [PATCH 18/18] simplify proofs --- .../Machines/SingleTapeTuring/Basic.lean | 97 ++++++++++++------- 1 file changed, 64 insertions(+), 33 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 55c8d22965..27b6a6d2e2 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -9,6 +9,7 @@ module public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.RelatesInSteps public import Mathlib.Algebra.Polynomial.Eval.Defs +public import Mathlib.Algebra.BigOperators.Fin @[expose] public section @@ -193,41 +194,67 @@ open Cfg variable [Inhabited Symbol] [Fintype Symbol] +/-- If the transition value is known, the step function produces the expected configuration. -/ +lemma step_of_transitionValue {tm : SingleTapeTM Symbol} {cfg : tm.Cfg} + {wr : Option Symbol} {dir : Option Dir} {q' : Option tm.State} + (h : tm.transitionValue cfg = some ⟨⟨wr, dir⟩, q'⟩) : + tm.step cfg = some ⟨q', (cfg.BiTape.write wr).optionMove dir⟩ := by + simp only [step, h]; rfl + +/-- If the transition value is `none`, the step function returns `none`. -/ +@[scoped grind =] +lemma step_none_of_transitionValue_none {tm : SingleTapeTM Symbol} {cfg : tm.Cfg} + (h : tm.transitionValue cfg = none) : tm.step cfg = none := by + simp only [step, h]; rfl + +/-- If `step` returns `some`, then the transition value is `some`. -/ +lemma transitionValue_isSome_of_step {tm : SingleTapeTM Symbol} {cfg cfg' : tm.Cfg} + (h : tm.step cfg = some cfg') : + (tm.transitionValue cfg).isSome := by + grind + /-- The sequence of configurations of the Turing machine `tm` starting from configuration `c`. After the sequence has reached a configuration in the halting state, it turns `none` and stays `none`. -/ def configs (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : (Option tm.Cfg) := (Option.bind · tm.step)^[t] (some c) -@[simp, grind =] +/-- Unrolling the last iteration of `configs`: one more step applied to the previous config. -/ +lemma configs_succ (tm : SingleTapeTM Symbol) (init : tm.Cfg) (t : ℕ) : + tm.configs init (t + 1) = (tm.configs init t).bind tm.step := by + simp [configs, Function.iterate_succ_apply'] + +/-- Unrolling the first iteration of `configs`: take the first step, then continue for `t` steps. -/ +lemma configs_succ' (tm : SingleTapeTM Symbol) (init : tm.Cfg) (t : ℕ) : + tm.configs init (t + 1) = (tm.step init).bind (tm.configs · t) := by + unfold configs + change (Option.bind · tm.step)^[t] (tm.step init) = + (tm.step init).bind (fun c => (Option.bind · tm.step)^[t] (some c)) + cases tm.step init with + | none => exact Function.iterate_fixed rfl t + | some _ => rfl + +@[simp, scoped grind →] lemma configs_isSome_of_succ_isSome (tm : SingleTapeTM Symbol) (init : tm.Cfg) (t : ℕ) (h_some : (tm.configs init (t + 1)).isSome) : (tm.configs init t).isSome := by - unfold configs - sorry - -/-- Once the sequence of configurations reaches `none`, it stays `none`. -/ -lemma configs_isNone_mono (tm : SingleTapeTM Symbol) (init : tm.Cfg) - (t₁ t₂ : ℕ) (h_le : t₁ ≤ t₂) (h_some : (tm.configs init t₂).isSome) : - Monotone (fun t => (tm.configs init t).isNone) := by - unfold configs - intro t₁ t₂ h_le - induction t₂ with - | zero => grind [Function.iterate_zero] - | succ t₁' ih => - simp only [Function.iterate_succ_apply'] - sorry - -def optionDirToInt : Option Dir → ℤ - | none => 0 - | some .left => -1 - | some .right => 1 + rw [configs_succ] at h_some + cases h : tm.configs init t with + | some _ => rfl + | none => simp [h] at h_some /-- The next movement of the tape head when in configuration `c`, as an integer. -/ def headMovement (tm : SingleTapeTM Symbol) (c : tm.Cfg) : ℤ := match tm.transitionValue c with | none => 0 - | some ⟨⟨_, dir⟩, _⟩ => optionDirToInt dir + | some ⟨⟨_, dir⟩, _⟩ => BiTape.optionDirToInt dir + +/-- The head movement equals `BiTape.optionDirToInt dir` when the transition value is known. -/ +lemma headMovement_of_transitionValue {tm : SingleTapeTM Symbol} {cfg : tm.Cfg} + {wr : Option Symbol} {dir : Option Dir} {q' : Option tm.State} + (h : tm.transitionValue cfg = some ⟨⟨wr, dir⟩, q'⟩) : + tm.headMovement cfg = BiTape.optionDirToInt dir := by + simp only [headMovement, h] /-- The sequence of positions of the tape head starting from configuration `c`, relative to the initial position of zero, at the beginning of step `t`. -/ @@ -238,7 +265,7 @@ def headPosition (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : ℤ := lemma headPosition_succ (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : tm.headPosition c (t + 1) = tm.headPosition c t + (((tm.configs c t).map tm.headMovement).getD 0) := by - sorry + exact Fin.sum_univ_castSucc _ /-- The tape of machine `tm` at the start of step `t` as a function `ℤ → Option Symbol` that does not "move" with the head. I.e. regardless of `t`, the symbol at zero is always @@ -249,7 +276,8 @@ def fixedTape (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) : Option (ℤ @[simp, scoped grind =] lemma fixedTape_isSome_of_succ_isSome (tm : SingleTapeTM Symbol) (c : tm.Cfg) (t : ℕ) (h_isSome : (tm.fixedTape c (t + 1)).isSome) : - (tm.fixedTape c t).isSome := by sorry + (tm.fixedTape c t).isSome := by + grind [fixedTape] /-- The space used by machine `tm` when starting in configuration `c` and executing for `t` steps, defined as the number of cells visited by the tape head. -/ @@ -261,18 +289,21 @@ lemma only_modification_at_headPosition (tm : SingleTapeTM Symbol) (init : tm.Cf (h_next : (tm.fixedTape init (t + 1)).isSome) (h_noHead : i ≠ tm.headPosition init t) : (tm.fixedTape init (t + 1)).get h_next i = (tm.fixedTape init t).get (by grind) i := by + have h_cs : (tm.configs init (t + 1)).isSome := by grind [fixedTape] unfold fixedTape + set cfg := (tm.configs init t).get (by grind) + have h_cfg : tm.configs init t = some cfg := by grind + have h_step : (tm.step cfg).isSome := by grind [configs_succ] + let stmt := ((tm.transitionValue cfg).get (by grind)).1 + simp only [Option.get_map, configs_succ, Option.get_bind] + have : ((tm.step cfg).get (by grind)).BiTape = + (cfg.BiTape.write stmt.symbol).optionMove stmt.movement := by + grind [step] + rw [this] + have h_hm : ((tm.configs init t).map tm.headMovement).getD 0 = + BiTape.optionDirToInt stmt.movement := by grind [headMovement] simp - have h_configs_some : (tm.configs init t).isSome := by sorry - have h_c : tm.configs init (t + 1) = (tm.configs init t).bind tm.step := by - simp [configs, Function.iterate_succ_apply'] - simp [h_c, Option.get_bind] - simp [Function.update] - split_ifs - · simp [transitionValue] - sorry - · simp [transitionValue] - sorry + grind [Fin.sum_univ_castSucc] /-- The `TransitionRelation` corresponding to a `SingleTapeTM Symbol`