From 189476fed26667c10616449410606914d99fa821 Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 17:03:01 +0200 Subject: [PATCH 01/18] basic results --- Cslib/Foundations/Relation/Basic.lean | 68 ++++++++++++++++++++++++++- Cslib/Foundations/Relation/Defs.lean | 16 +++++-- 2 files changed, 78 insertions(+), 6 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index aafcddac2..9a8d310ad 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -24,6 +24,8 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou namespace Relation +open Function + /-- A pair of subrelations lifts to transitivity on the relation. -/ @[implicit_reducible] def transLeftRight (s s' r : α → α → Prop) [IsTrans α r] (h : s ≤ r) (h' : s' ≤ r) : @@ -40,28 +42,90 @@ def transLeft (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s def transRight (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r where trans hab hbc := _root_.trans hab (h _ _ hbc) +theorem comp_le_comp {s s' r r' : α → α → Prop} (hs : s ≤ s') (hr : r ≤ r') : + Comp s r ≤ Comp s' r' := fun a c ⟨b, hab, hbc⟩ ↦ ⟨b, hs a b hab, hr b c hbc⟩ + +theorem comp_self_le (r : α → α → Prop) [IsTrans α r] : Comp r r ≤ r := + fun _ _ ⟨_, hab, hbc⟩ ↦ _root_.trans hab hbc + +theorem swap_le_iff_le_swap {r₁ r₂ : α → α → Prop} : swap r₁ ≤ r₂ ↔ r₁ ≤ swap r₂ := by + constructor <;> intro h a b hab <;> exact h b a hab + attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen +theorem ReflGen.le_reflGen : r ≤ ReflGen r := fun _ _ => ReflGen.single + theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := EqvGen.reflGen_le_eqvGen r _ _ h +theorem TransGen.le_transGen : r ≤ TransGen r := fun _ _ => TransGen.single + theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := EqvGen.transGen_le_eqvGen r _ _ h theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := EqvGen.reflTransGen_le_eqvGen r _ _ h +theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl + theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := EqvGen.symmGen_le_eqvGen r _ _ h +theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel + +theorem _root_.Equivalence.eqvGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : EqvGen r₁ ≤ r₂ := + have := h.isEquiv + EqvGen.eqvGen_le hle + attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen SymmGen.to_eqvGen +theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩ + +@[simp] theorem hJoin_eq_join : HJoin r r = Join r := rfl + +@[grind =] theorem hJoin_eq_comp_swap : HJoin r₁ r₂ = Comp r₁ (swap r₂) := rfl + +instance [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (HJoin r₁ r₂) where + refl a := ⟨a, refl a, refl a⟩ + +theorem HJoin.single_left [Std.Refl r₂] (h : r₁ a b) : HJoin r₁ r₂ a b := ⟨b, h, refl b⟩ + +theorem HJoin.single_right [Std.Refl r₁] (h : r₂ a b) : HJoin r₁ r₂ b a := ⟨b, refl b, h⟩ + +theorem HJoin.hJoin_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : HJoin r₁ r₂ ≤ r := + (comp_le_comp h₁ h₂).trans (comp_self_le r) + +theorem HJoin.swap_iff {a b : α} : HJoin r₁ r₂ b a ↔ HJoin r₂ r₁ a b := by grind [HJoin] + @[deprecated _root_.refl (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a -theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by - use b +@[deprecated Join.single (since := "2026-09-07")] +theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := Join.single h + +theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : + MJoin r₁ ≤ r₂ := + have := h.isEquiv + join_le_of_equivalence_of_le h <| reflTransGen_le_of_le hle + +theorem MJoin.mJoin_le_eqvGen : MJoin r ≤ EqvGen r := + (EqvGen.is_equivalence r).mJoin_le EqvGen.le_eqvGen + +theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl + +theorem MHJoin.mHJoin_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : + MHJoin r₁ r₂ ≤ r := by + refine HJoin.hJoin_le ?_ (ReflTransGen.swap.trans ?_) + <;> apply reflTransGen_le_of_le <;> assumption + +theorem MHJoin.mHJoin_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + MHJoin r₁ r₂ ≤ r := mHJoin_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq]) + +theorem _root_.Equivalence.mHJoin_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + MHJoin r₁ r₂ ≤ r := + have := h.isEquiv + MHJoin.mHJoin_le_of_isEquiv h₁ h₂ /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) : diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 10e57bd42..967091392 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -35,10 +35,14 @@ def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b} /-- Codomain of a relation, aka range. -/ def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b} +def HJoin (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a c ∧ r₂ b c + /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/ abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) +abbrev MHJoin (r₁ r₂ : α → α → Prop) := HJoin (ReflTransGen r₁) (ReflTransGen r₂) + /-- The relation `r` 'up to' the relation `s`. -/ def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s) @@ -52,7 +56,7 @@ abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → /-- Generalization of `Diamond` to two relations. -/ def DiamondCommute (r₁ r₂ : α → α → Prop) := - ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → ∃ z, r₂ y₁ z ∧ r₁ y₂ z + ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → HJoin r₁ r₂ y₁ y₂ /-- A relation is confluent when its reflexive transitive closure has the diamond property. -/ abbrev Confluent (r : α → α → Prop) := Diamond (ReflTransGen r) @@ -63,14 +67,18 @@ abbrev Commute (r₁ r₂ : α → α → Prop) := DiamondCommute (ReflTransGen /-- A relation is semi-confluent when single and multiple steps with common origin are multi-joinable. -/ abbrev SemiConfluent (r : α → α → Prop) := - ∀ {x y₁ y₂}, ReflTransGen r x y₂ → r x y₁ → Join (ReflTransGen r) y₁ y₂ + ∀ {x y₁ y₂}, ReflTransGen r x y₂ → r x y₁ → MJoin r y₁ y₂ /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/ -abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join (ReflTransGen r) x y +abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → MJoin r x y /-- A relation is locally confluent when all reductions with a common origin are multi-joinable -/ abbrev LocallyConfluent (r : α → α → Prop) := - ∀ {a b c : α}, r a b → r a c → Join (ReflTransGen r) b c + ∀ {a b c : α}, r a b → r a c → MJoin r b c + +/-- Generalization of `LocallyConfluent` to two relations. -/ +def LocallyCommute (r₁ r₂ : α → α → Prop) := + ∀ {a b c : α}, r₁ a b → r₂ a c → MHJoin r₁ r₂ b c /-- A relation is strongly confluent when single steps are reflexive- and multi-joinable. -/ abbrev StronglyConfluent (r : α → α → Prop) := From fe95f374a560f09c5af46da61ae990410c3bc501 Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 19:07:51 +0200 Subject: [PATCH 02/18] generalise to commutation --- Cslib/Foundations/Relation/Basic.lean | 27 ++- Cslib/Foundations/Relation/Confluence.lean | 221 +++++++++++---------- Cslib/Foundations/Relation/Defs.lean | 9 +- 3 files changed, 147 insertions(+), 110 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 9a8d310ad..b1b2d88cf 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -71,6 +71,8 @@ theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := EqvGen.symmGen_le_eqvGen r _ _ h +theorem symmGen_eq_sup_swap : SymmGen r = r ⊔ Function.swap r := rfl + theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel theorem _root_.Equivalence.eqvGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : EqvGen r₁ ≤ r₂ := @@ -112,7 +114,7 @@ theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) theorem MJoin.mJoin_le_eqvGen : MJoin r ≤ EqvGen r := (EqvGen.is_equivalence r).mJoin_le EqvGen.le_eqvGen -theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl +@[simp] theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl theorem MHJoin.mHJoin_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : MHJoin r₁ r₂ ≤ r := by @@ -127,6 +129,13 @@ theorem _root_.Equivalence.mHJoin_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h have := h.isEquiv MHJoin.mHJoin_le_of_isEquiv h₁ h₂ +theorem MHJoin.swap_iff : MHJoin r₁ r₂ b a ↔ MHJoin r₂ r₁ a b := HJoin.swap_iff + +theorem MHJoin.left_le : r₁ ≤ MHJoin r₁ r₂ := fun _ _ h => HJoin.single_left (.single h) + +theorem MHJoin.swap_right_le : swap r₂ ≤ MHJoin r₁ r₂ := + fun _ _ h => HJoin.single_right (.single h) + /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) : ReflTransGen r₁ = ReflTransGen r₂ := by @@ -140,4 +149,20 @@ lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a @[simp, grind =] theorem reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := EqvGen.reflTransGen_symmGen r +@[scoped grind <=] +theorem join_inl (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b := + Or.inl r₁_ab + +@[scoped grind <=] +theorem join_inr (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b := + Or.inr r₂_ab + +@[scoped grind <=] +theorem join_inl_reflTransGen (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b := + ReflTransGen.mono le_sup_left _ _ r₁_ab + +@[scoped grind <=] +theorem join_inr_reflTransGen (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b := + ReflTransGen.mono le_sup_right _ _ r₂_ab + end Relation diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index bdfb8b857..e251ff50a 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -7,9 +7,9 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module public import Cslib.Foundations.Relation.Termination -public import Mathlib.Data.List.Pairwise +public import Mathlib.Tactic.TFAE -/-! # Relations: Confluence and Termination +/-! # Relations: Confluence This module proves some properties regarding confluence that are used for both lambda calculi and combinatory logic. Some notable theorems: @@ -29,60 +29,101 @@ variable {α : Type*} {r r₁ r₂ : α → α → Prop} namespace Relation +open Function ReflTransGen + +@[simp] theorem Commute.to_confluent : Commute r r = Confluent r := rfl + +@[deprecated (since := "2026-09-03")] alias Commute.toConfluent := Commute.to_confluent + +@[simp] theorem StronglyCommute.to_stronglyConfluent : + StronglyCommute r r = StronglyConfluent r := rfl + +@[deprecated (since := "2026-09-03")] alias StronglyCommute.toStronglyConfluent := + StronglyCommute.to_stronglyConfluent + +@[simp] theorem DiamondCommute.to_diamond : DiamondCommute r r = Diamond r := rfl + +@[deprecated (since := "2026-09-03")] alias DiamondCommute.toDiamond := DiamondCommute.to_diamond + +@[simp] theorem SemiCommute.to_semiConfluent : SemiCommute r r = SemiConfluent r := rfl + +@[simp] theorem LocallyCommute.to_locallyConfluent : LocallyCommute r r = LocallyConfluent r := rfl + +instance : Std.Symm (@Commute α) where + symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, HJoin] + +lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : + MHJoin r₂ r₁ b c := by + induction h₁ using ReflTransGen.head_induction_on generalizing c with + | refl => exact HJoin.single_left (.single h₂) + | head ha _ ih => + obtain ⟨d, had, hcd⟩ := h ha h₂ + obtain ⟨d', hbd', hdd'⟩ := ih had + exact ⟨d', hbd', hdd'.head hcd⟩ + /-- Extending a multistep reduction by a single step preserves multi-joinability. -/ lemma Diamond.extend (h : Diamond r) : - ReflTransGen r a b → r a c → Join (ReflTransGen r) b c := by - intros ab ac - induction ab using ReflTransGen.head_induction_on generalizing c - case refl => exists c, .single ac - case head a'_c' _ ih => - obtain ⟨d, cd, c'_d⟩ := h ac a'_c' - obtain ⟨d', b_d', d_d'⟩ := ih c'_d - exact ⟨d', b_d', .head cd d_d'⟩ + ReflTransGen r a b → r a c → Join (ReflTransGen r) b c := DiamondCommute.extend h + +lemma DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := by + intro a b₁ b₂ hab₁ hab₂ + induction hab₂ using ReflTransGen.head_induction_on generalizing b₁ with + | refl => exact HJoin.single_right hab₁ + | @head a a' ha hab₂ ih => + obtain ⟨c, hb₁c, hac⟩ := h.extend hab₁ ha + obtain ⟨d, hcd, hb₂d⟩ := ih hac + exact ⟨d, hb₁c.trans hcd, hb₂d⟩ /-- The diamond property implies confluence. -/ -theorem Diamond.to_confluent (h : Diamond r) : Confluent r := by - intros a b c ab bc - induction ab using ReflTransGen.head_induction_on generalizing c - case refl => exists c - case head _ _ a'_c' _ ih => - obtain ⟨d, cd, c'_d⟩ := h.extend bc a'_c' - obtain ⟨d', b_d', d_d'⟩ := ih c'_d - exact ⟨d', b_d', .trans cd d_d'⟩ +theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_commute h @[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent -theorem Confluent.to_churchRosser (h : Confluent r) : ChurchRosser r := by - intro x y h_eqv - induction h_eqv with - | rel _ b => exists b; grind [ReflTransGen.single] - | refl a => exists a - | symm a b _ ih => exact symm ih - | trans _ _ _ _ _ ih1 ih2 => - obtain ⟨u, _, hbu⟩ := ih1 - obtain ⟨v, hbv, _⟩ := ih2 - obtain ⟨w, _, _⟩ := h hbu hbv - exists w - grind [ReflTransGen.trans] - -@[deprecated (since := "2026-09-03")] alias Confluent.toChurchRosser := Confluent.to_churchRosser - -theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := by - intro x y1 y2 h_xy1 h_xy2 - induction h_xy1 with - | refl => use y2 - | tail h_xz h_zy1 ih => - obtain ⟨u, h_zu, _⟩ := ih - obtain ⟨v, _, _⟩ := h h_zu h_zy1 - exists v - grind [ReflTransGen.trans] +theorem Commute.isTrans_mHJoin (h : Commute r₁ r₂) : IsTrans α (MHJoin r₁ r₂) where + trans a b c := by + intro ⟨d, had, hbd⟩ ⟨d', hbd', hcd'⟩ + obtain ⟨e, he, he'⟩ := h hbd' hbd + exact ⟨e, had.trans he', hcd'.trans he⟩ -@[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent +theorem Confluent.isTrans_mJoin (h : Confluent r) : IsTrans α (MJoin r) := Commute.isTrans_mHJoin h -attribute [scoped grind →] Confluent.to_churchRosser SemiConfluent.to_confluent +theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by + intro a b₁ b₂ hab₁ hab₂ + induction hab₁ with + | refl => use b₂ + | tail hab hbb' ih => + obtain ⟨d, hd, hd'⟩ := ih + obtain ⟨e, he, he'⟩ := h hbb' hd + use e, he, hd'.trans he' -private theorem confluent_equivalents : [ChurchRosser r, SemiConfluent r, Confluent r].TFAE := by - grind [List.tfae_cons_cons, List.tfae_singleton] +theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := SemiCommute.to_commute h + +@[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent + +theorem commute_equivalents : + [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (MHJoin r₁ r₂), + ReflTransGen (r₁ ⊔ swap r₂) ≤ MHJoin r₁ r₂, + ReflTransGen (r₁ ⊔ swap r₂) = MHJoin r₁ r₂].TFAE := by + tfae_have 1 → 2 := SemiCommute.to_commute + tfae_have 2 → 3 := Commute.isTrans_mHJoin + tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <| sup_le MHJoin.left_le MHJoin.swap_right_le + tfae_have 4 → 5 := fun h => h.antisymm <| + MHJoin.mHJoin_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen) + tfae_have 5 → 1 := by + intro h a b₁ b₂ h₁ h₂ + rw [MHJoin.swap_iff, ← h] + exact (ReflTransGen.mono le_sup_right _ _ <| reflTransGen_swap.mpr h₂).tail (Or.inl h₁) + tfae_finish + +theorem churchRosser_iff_eqvGen_le_mJoin : ChurchRosser r ↔ EqvGen r ≤ MJoin r := Iff.rfl + +theorem confluent_equivalents : + [ChurchRosser r, SemiConfluent r, Confluent r, IsTrans α (MJoin r), + EqvGen r ≤ MJoin r, EqvGen r = MJoin r].TFAE := by + refine (List.tfae_cons ?_).mpr ⟨churchRosser_iff_eqvGen_le_mJoin, ?_⟩ + · grind + · simpa [← symmGen_eq_sup_swap, reflTransGen_symmGen] using + commute_equivalents (r₁ := r) (r₂ := r) theorem semiConfluent_iff_churchRosser : SemiConfluent r ↔ ChurchRosser r := List.TFAE.out confluent_equivalents 2 1 @@ -93,8 +134,12 @@ theorem semiConfluent_iff_churchRosser : SemiConfluent r ↔ ChurchRosser r := theorem confluent_iff_churchRosser : Confluent r ↔ ChurchRosser r := List.TFAE.out confluent_equivalents 3 1 +alias ⟨_, Confluent.to_churchRosser⟩ := confluent_iff_churchRosser + @[deprecated (since := "2026-09-03")] alias Confluent_iff_ChurchRosser := confluent_iff_churchRosser +attribute [scoped grind →] Confluent.to_churchRosser SemiConfluent.to_confluent + theorem confluent_iff_semiConfluent : Confluent r ↔ SemiConfluent r := List.TFAE.out confluent_equivalents 3 2 @@ -125,9 +170,8 @@ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) : apply equivalence_join grind -theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) : +theorem Normalizing.confluent_iff_forall_unique_normal (hn : Normalizing r) : Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n := by - have hn : Normalizing r := ht.to_normalizing constructor · intro hc a apply existsUnique_of_exists_of_unique (hn a) @@ -142,11 +186,11 @@ theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) : obtain ⟨nc, hcnc, hnc⟩ := hn c have hanb : (ReflTransGen r) a nb := ReflTransGen.trans hab hbnb have hanc : (ReflTransGen r) a nc := ReflTransGen.trans hac hcnc - have hnanb : nb = na := H nb ⟨hanb, hnb⟩ - have hnanc : nc = na := H nc ⟨hanc, hnc⟩ - rw [hnanb] at hbnb - rw [hnanc] at hcnc - exact ⟨hbnb, hcnc⟩ + grind + +theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) : + Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n := + ht.to_normalizing.confluent_iff_forall_unique_normal @[deprecated (since := "2026-09-03")] alias Terminating.isConfluent_iff_all_unique_Normal := Terminating.confluent_iff_forall_unique_normal @@ -177,45 +221,28 @@ theorem Confluent.to_locallyConfluent (h : Confluent r) : LocallyConfluent r := @[deprecated (since := "2026-09-03")] alias Confluent.toLocallyConfluent := Confluent.to_locallyConfluent -/-- Newman's lemma: a terminating, locally confluent relation is confluent. -/ -theorem LocallyConfluent.terminating_toConfluent (hlc : LocallyConfluent r) (ht : Terminating r) : - Confluent r := by +theorem LocallyCommute.commute_of_terminating_sup (hlc : LocallyCommute r₁ r₂) + (ht : Terminating (r₁ ⊔ r₂)) : Commute r₁ r₂ := by intro x induction x using ht.induction with | h x ih => - intro y z xy xz - cases xy.cases_head with - | inl => exists z; grind - | inr h => - obtain ⟨y₁, x_y₁, y₁_y⟩ := h - cases xz.cases_head with - | inl => exists y; grind - | inr h => - obtain ⟨z₁, x_z₁, z₁_z⟩ := h - have ⟨u, z₁_u, y₁_u⟩ := hlc x_z₁ x_y₁ - have ⟨v, uv, yv⟩ : Join (ReflTransGen r) u y := by grind - have ⟨w, vw, zw⟩ : Join (ReflTransGen r) v z := by grind [ReflTransGen.trans] - exact ⟨w, .trans yv vw, zw⟩ + intro y z hy hz + rcases hy.cases_head with (rfl | ⟨y', hy, hy'⟩) + · use z + · rcases hz.cases_head with (rfl | ⟨z', hz, hz'⟩) + · use y + · obtain ⟨u, hyu, hzu⟩ := hlc hy hz + obtain ⟨v, hyv, huv⟩ := ih y' (join_inl hy) hy' hyu + obtain ⟨w, hvw, hzw⟩ := ih z' (join_inr hz) (hzu.trans huv) hz' + exact ⟨w, hyv.trans hvw, hzw⟩ + +/-- Newman's lemma: a terminating, locally confluent relation is confluent. -/ +theorem LocallyConfluent.terminating_toConfluent (hlc : LocallyConfluent r) (ht : Terminating r) : + Confluent r := LocallyCommute.commute_of_terminating_sup hlc ((sup_idem r).symm ▸ ht) @[deprecated (since := "2026-09-03")] alias LocallyConfluent.Terminating_toConfluent := LocallyConfluent.terminating_toConfluent -instance : Std.Symm (@Commute α) where - symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁] - -theorem Commute.to_confluent : Commute r r = Confluent r := rfl - -@[deprecated (since := "2026-09-03")] alias Commute.toConfluent := Commute.to_confluent - -theorem StronglyCommute.to_stronglyConfluent : StronglyCommute r r = StronglyConfluent r := rfl - -@[deprecated (since := "2026-09-03")] alias StronglyCommute.toStronglyConfluent := - StronglyCommute.to_stronglyConfluent - -theorem DiamondCommute.to_diamond : DiamondCommute r r = Diamond r := by rfl - -@[deprecated (since := "2026-09-03")] alias DiamondCommute.toDiamond := DiamondCommute.to_diamond - theorem StronglyCommute.extend (h : StronglyCommute r₁ r₂) (xy : ReflTransGen r₁ x y) (xz : r₂ x z) : ∃ w, ReflGen r₂ y w ∧ ReflTransGen r₁ z w := by induction xy with @@ -243,37 +270,19 @@ theorem StronglyConfluent.to_confluent (h : StronglyConfluent r) : Confluent r : @[deprecated (since := "2026-09-03")] alias StronglyConfluent.toConfluent := StronglyConfluent.to_confluent -variable {r₁ r₂ : α → α → Prop} - -@[scoped grind <=] -theorem join_inl (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b := - Or.inl r₁_ab - -@[scoped grind <=] -theorem join_inr (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b := - Or.inr r₂_ab - -@[scoped grind <=] -theorem join_inl_reflTransGen (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b := - ReflTransGen.mono le_sup_left _ _ r₁_ab - -@[scoped grind <=] -theorem join_inr_reflTransGen (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b := - ReflTransGen.mono le_sup_right _ _ r₂_ab - lemma Commute.join_left (c₁ : Commute r₁ r₃) (c₂ : Commute r₂ r₃) : Commute (r₁ ⊔ r₂) r₃ := by intro x y z xy xz induction xy with - | refl => grind + | refl => grind [HJoin] | @tail b c _ bc ih => have ⟨w, bw, _⟩ := ih cases bc with | inl bc => obtain ⟨_, _, _⟩ := c₁ (.single bc) bw - grind [ReflTransGen.trans] + grind [HJoin, ReflTransGen.trans] | inr bc => obtain ⟨_, _, _⟩ := c₂ (.single bc) bw - grind [ReflTransGen.trans] + grind [HJoin, ReflTransGen.trans] theorem Commute.join_confluent (c₁ : Confluent r₁) (c₂ : Confluent r₂) (comm : Commute r₁ r₂) : Confluent (r₁ ⊔ r₂) := by diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 967091392..9409c4fb1 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -56,7 +56,7 @@ abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → /-- Generalization of `Diamond` to two relations. -/ def DiamondCommute (r₁ r₂ : α → α → Prop) := - ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → HJoin r₁ r₂ y₁ y₂ + ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → HJoin r₂ r₁ y₁ y₂ /-- A relation is confluent when its reflexive transitive closure has the diamond property. -/ abbrev Confluent (r : α → α → Prop) := Diamond (ReflTransGen r) @@ -67,7 +67,10 @@ abbrev Commute (r₁ r₂ : α → α → Prop) := DiamondCommute (ReflTransGen /-- A relation is semi-confluent when single and multiple steps with common origin are multi-joinable. -/ abbrev SemiConfluent (r : α → α → Prop) := - ∀ {x y₁ y₂}, ReflTransGen r x y₂ → r x y₁ → MJoin r y₁ y₂ + ∀ {x y₁ y₂}, r x y₁ → ReflTransGen r x y₂ → MJoin r y₁ y₂ + +abbrev SemiCommute (r₁ r₂ : α → α → Prop) := + ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → MHJoin r₂ r₁ y₁ y₂ /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/ abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → MJoin r x y @@ -78,7 +81,7 @@ abbrev LocallyConfluent (r : α → α → Prop) := /-- Generalization of `LocallyConfluent` to two relations. -/ def LocallyCommute (r₁ r₂ : α → α → Prop) := - ∀ {a b c : α}, r₁ a b → r₂ a c → MHJoin r₁ r₂ b c + ∀ {a b c : α}, r₁ a b → r₂ a c → MHJoin r₂ r₁ b c /-- A relation is strongly confluent when single steps are reflexive- and multi-joinable. -/ abbrev StronglyConfluent (r : α → α → Prop) := From bb51be03d77ead71a17af91e7fbfd2ed7fc3f4d7 Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 19:19:29 +0200 Subject: [PATCH 03/18] docs --- Cslib/Foundations/Relation/Basic.lean | 2 +- Cslib/Foundations/Relation/Confluence.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index b1b2d88cf..96e2eec62 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -71,7 +71,7 @@ theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := EqvGen.symmGen_le_eqvGen r _ _ h -theorem symmGen_eq_sup_swap : SymmGen r = r ⊔ Function.swap r := rfl +@[simp] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index e251ff50a..622cdc021 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -17,6 +17,9 @@ combinatory logic. Some notable theorems: * `Diamond.to_confluent`: the diamond property implies confluence * `LocallyConfluent.terminating_toConfluent`: Newman's lemma +We prove most results first for two relations, where `Confluent r` becomes `Commute r₁ r₂`, then +specialize to the classical case where `r₁ = r₂`. + ## References * [*Term Rewriting and All That*][Baader1998] From fb5b9e5e2493b8b6a63187774897692a01bf992d Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 19:39:36 +0200 Subject: [PATCH 04/18] fix build --- Cslib/Foundations/Relation/Confluence.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 622cdc021..f6f285c88 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -125,8 +125,7 @@ theorem confluent_equivalents : EqvGen r ≤ MJoin r, EqvGen r = MJoin r].TFAE := by refine (List.tfae_cons ?_).mpr ⟨churchRosser_iff_eqvGen_le_mJoin, ?_⟩ · grind - · simpa [← symmGen_eq_sup_swap, reflTransGen_symmGen] using - commute_equivalents (r₁ := r) (r₂ := r) + · simpa [reflTransGen_symmGen] using commute_equivalents (r₁ := r) (r₂ := r) theorem semiConfluent_iff_churchRosser : SemiConfluent r ↔ ChurchRosser r := List.TFAE.out confluent_equivalents 2 1 From 277a87b584c267339acc3dc943ca2d9d3c78058a Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 20:19:02 +0200 Subject: [PATCH 05/18] un-use deprecated theorems --- Cslib/Languages/CombinatoryLogic/Confluence.lean | 4 ++-- Cslib/Languages/CombinatoryLogic/Evaluation.lean | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index 97c48458d..053ab299c 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -217,8 +217,8 @@ theorem mJoin_red_equivalence : Equivalence (MJoin Red) := by theorem MRed.diamond : Confluent Red := by intro a b c hab hac apply mJoin_red_equivalence.trans (y := a) - · exact mJoin_red_equivalence.symm (MJoin.single hab) - · exact MJoin.single hac + · exact mJoin_red_equivalence.symm (Join.single hab) + · exact Join.single hac end SKI diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean index 8971eebe8..b4c08550c 100644 --- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean +++ b/Cslib/Languages/CombinatoryLogic/Evaluation.lean @@ -214,11 +214,11 @@ theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool have h : MJoin Red (if u then S else K) (if v then S else K) := by apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K) · apply mJoin_red_equivalence.symm - apply Relation.MJoin.single + apply Relation.Join.single exact hx S K · apply mJoin_red_equivalence.trans (y := y ⬝ S ⬝ K) · exact mJoin_red_head K <| mJoin_red_head S hxy - · apply Relation.MJoin.single + · apply Relation.Join.single exact hy S K grind [sk_nequiv, mJoin_red_equivalence.symm h] @@ -254,11 +254,11 @@ theorem isChurch_injective (x y : SKI) (n m : Nat) (hx : IsChurch n x) (hy : IsC exact eq_of_mJoin_red_redexFree this (churchK_redexFree n) (churchK_redexFree m) apply mJoin_red_equivalence.trans (y := x ⬝ K ⬝ K) · simp_rw [churchK_church] - exact mJoin_red_equivalence.symm <| Relation.MJoin.single (hx K K) + exact mJoin_red_equivalence.symm <| Relation.Join.single (hx K K) · apply mJoin_red_equivalence.trans (y := y ⬝ K ⬝ K) · apply mJoin_red_head; apply mJoin_red_head; assumption · simp_rw [churchK_church] - exact Relation.MJoin.single (hy K K) + exact Relation.Join.single (hy K K) /-- **Rice's theorem**: no SKI term is a non-trivial predicate. From f0fb93c6db0b70ad62aad31d48cabd988a506aad Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 7 Sep 2026 20:34:26 +0200 Subject: [PATCH 06/18] lint --- Cslib/Foundations/Relation/Basic.lean | 2 +- Cslib/Foundations/Relation/Confluence.lean | 2 +- Cslib/Foundations/Relation/Defs.lean | 3 +++ 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 96e2eec62..bcdfb71b1 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -114,7 +114,7 @@ theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) theorem MJoin.mJoin_le_eqvGen : MJoin r ≤ EqvGen r := (EqvGen.is_equivalence r).mJoin_le EqvGen.le_eqvGen -@[simp] theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl +theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl theorem MHJoin.mHJoin_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : MHJoin r₁ r₂ ≤ r := by diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index f6f285c88..12ae0475b 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -34,7 +34,7 @@ namespace Relation open Function ReflTransGen -@[simp] theorem Commute.to_confluent : Commute r r = Confluent r := rfl +theorem Commute.to_confluent : Commute r r = Confluent r := rfl @[deprecated (since := "2026-09-03")] alias Commute.toConfluent := Commute.to_confluent diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 9409c4fb1..201c5cc9b 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -35,12 +35,14 @@ def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b} /-- Codomain of a relation, aka range. -/ def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b} +/-- Generalisation of `Join` to two relations. -/ def HJoin (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a c ∧ r₂ b c /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/ abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) +/-- Generalisation of `MJoin` to two relations. -/ abbrev MHJoin (r₁ r₂ : α → α → Prop) := HJoin (ReflTransGen r₁) (ReflTransGen r₂) /-- The relation `r` 'up to' the relation `s`. -/ @@ -69,6 +71,7 @@ abbrev Commute (r₁ r₂ : α → α → Prop) := DiamondCommute (ReflTransGen abbrev SemiConfluent (r : α → α → Prop) := ∀ {x y₁ y₂}, r x y₁ → ReflTransGen r x y₂ → MJoin r y₁ y₂ +/-- Generalisation of `SemiConfluent` to two relations. -/ abbrev SemiCommute (r₁ r₂ : α → α → Prop) := ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → MHJoin r₂ r₁ y₁ y₂ From ffad88e7ca153c59b0971ea7f81d6d6a32e21657 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 11 Sep 2026 10:14:46 +0200 Subject: [PATCH 07/18] upstreaming note --- Cslib/Foundations/Relation/Basic.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index bcdfb71b1..b64642c98 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -9,7 +9,13 @@ module public import Cslib.Foundations.Relation.Defs public import Mathlib.Order.WellFounded -/-! # Basic properties of relations -/ +/-! # Basic properties of relations + +## TODO: +Many of the results here could be upstreamed to Mathlib. In particular: +- `ReflGen.le_reflGen` and relatives, +- `ReflGen.to_eqvGen` and relatives. +-/ @[expose] public section From e1c1009bbaf1a4f143fa73a296f432bfb52a11d6 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 11 Sep 2026 10:19:22 +0200 Subject: [PATCH 08/18] join2 naming --- Cslib/Foundations/Relation/Basic.lean | 40 +++++++++++----------- Cslib/Foundations/Relation/Confluence.lean | 32 ++++++++--------- Cslib/Foundations/Relation/Defs.lean | 10 +++--- 3 files changed, 41 insertions(+), 41 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index b64642c98..12702524d 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -90,21 +90,21 @@ attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.t theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩ -@[simp] theorem hJoin_eq_join : HJoin r r = Join r := rfl +@[simp] theorem join₂_eq_join : Join₂ r r = Join r := rfl -@[grind =] theorem hJoin_eq_comp_swap : HJoin r₁ r₂ = Comp r₁ (swap r₂) := rfl +@[grind =] theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl -instance [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (HJoin r₁ r₂) where +instance [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (Join₂ r₁ r₂) where refl a := ⟨a, refl a, refl a⟩ -theorem HJoin.single_left [Std.Refl r₂] (h : r₁ a b) : HJoin r₁ r₂ a b := ⟨b, h, refl b⟩ +theorem Join₂.single_left [Std.Refl r₂] (h : r₁ a b) : Join₂ r₁ r₂ a b := ⟨b, h, refl b⟩ -theorem HJoin.single_right [Std.Refl r₁] (h : r₂ a b) : HJoin r₁ r₂ b a := ⟨b, refl b, h⟩ +theorem Join₂.single_right [Std.Refl r₁] (h : r₂ a b) : Join₂ r₁ r₂ b a := ⟨b, refl b, h⟩ -theorem HJoin.hJoin_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : HJoin r₁ r₂ ≤ r := +theorem Join₂.join₂_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : Join₂ r₁ r₂ ≤ r := (comp_le_comp h₁ h₂).trans (comp_self_le r) -theorem HJoin.swap_iff {a b : α} : HJoin r₁ r₂ b a ↔ HJoin r₂ r₁ a b := by grind [HJoin] +theorem Join₂.swap_iff {a b : α} : Join₂ r₁ r₂ b a ↔ Join₂ r₂ r₁ a b := by grind [Join₂] @[deprecated _root_.refl (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a @@ -120,27 +120,27 @@ theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) theorem MJoin.mJoin_le_eqvGen : MJoin r ≤ EqvGen r := (EqvGen.is_equivalence r).mJoin_le EqvGen.le_eqvGen -theorem mHJoin_eq_mJoin : MHJoin r r = MJoin r := rfl +theorem mJoin₂_eq_mJoin : MJoin₂ r r = MJoin r := rfl -theorem MHJoin.mHJoin_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : - MHJoin r₁ r₂ ≤ r := by - refine HJoin.hJoin_le ?_ (ReflTransGen.swap.trans ?_) +theorem MJoin₂.mJoin₂_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : + MJoin₂ r₁ r₂ ≤ r := by + refine Join₂.join₂_le ?_ (ReflTransGen.swap.trans ?_) <;> apply reflTransGen_le_of_le <;> assumption -theorem MHJoin.mHJoin_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : - MHJoin r₁ r₂ ≤ r := mHJoin_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq]) +theorem MJoin₂.mJoin₂_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + MJoin₂ r₁ r₂ ≤ r := mJoin₂_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq]) -theorem _root_.Equivalence.mHJoin_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : - MHJoin r₁ r₂ ≤ r := +theorem _root_.Equivalence.mJoin₂_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + MJoin₂ r₁ r₂ ≤ r := have := h.isEquiv - MHJoin.mHJoin_le_of_isEquiv h₁ h₂ + MJoin₂.mJoin₂_le_of_isEquiv h₁ h₂ -theorem MHJoin.swap_iff : MHJoin r₁ r₂ b a ↔ MHJoin r₂ r₁ a b := HJoin.swap_iff +theorem MJoin₂.swap_iff : MJoin₂ r₁ r₂ b a ↔ MJoin₂ r₂ r₁ a b := Join₂.swap_iff -theorem MHJoin.left_le : r₁ ≤ MHJoin r₁ r₂ := fun _ _ h => HJoin.single_left (.single h) +theorem MJoin₂.left_le : r₁ ≤ MJoin₂ r₁ r₂ := fun _ _ h => Join₂.single_left (.single h) -theorem MHJoin.swap_right_le : swap r₂ ≤ MHJoin r₁ r₂ := - fun _ _ h => HJoin.single_right (.single h) +theorem MJoin₂.swap_right_le : swap r₂ ≤ MJoin₂ r₁ r₂ := + fun _ _ h => Join₂.single_right (.single h) /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) : diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 12ae0475b..89654a19e 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -53,12 +53,12 @@ theorem Commute.to_confluent : Commute r r = Confluent r := rfl @[simp] theorem LocallyCommute.to_locallyConfluent : LocallyCommute r r = LocallyConfluent r := rfl instance : Std.Symm (@Commute α) where - symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, HJoin] + symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, Join₂] lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : - MHJoin r₂ r₁ b c := by + MJoin₂ r₂ r₁ b c := by induction h₁ using ReflTransGen.head_induction_on generalizing c with - | refl => exact HJoin.single_left (.single h₂) + | refl => exact Join₂.single_left (.single h₂) | head ha _ ih => obtain ⟨d, had, hcd⟩ := h ha h₂ obtain ⟨d', hbd', hdd'⟩ := ih had @@ -71,7 +71,7 @@ lemma Diamond.extend (h : Diamond r) : lemma DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := by intro a b₁ b₂ hab₁ hab₂ induction hab₂ using ReflTransGen.head_induction_on generalizing b₁ with - | refl => exact HJoin.single_right hab₁ + | refl => exact Join₂.single_right hab₁ | @head a a' ha hab₂ ih => obtain ⟨c, hb₁c, hac⟩ := h.extend hab₁ ha obtain ⟨d, hcd, hb₂d⟩ := ih hac @@ -82,13 +82,13 @@ theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_ @[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent -theorem Commute.isTrans_mHJoin (h : Commute r₁ r₂) : IsTrans α (MHJoin r₁ r₂) where +theorem Commute.isTrans_mJoin₂ (h : Commute r₁ r₂) : IsTrans α (MJoin₂ r₁ r₂) where trans a b c := by intro ⟨d, had, hbd⟩ ⟨d', hbd', hcd'⟩ obtain ⟨e, he, he'⟩ := h hbd' hbd exact ⟨e, had.trans he', hcd'.trans he⟩ -theorem Confluent.isTrans_mJoin (h : Confluent r) : IsTrans α (MJoin r) := Commute.isTrans_mHJoin h +theorem Confluent.isTrans_mJoin (h : Confluent r) : IsTrans α (MJoin r) := Commute.isTrans_mJoin₂ h theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by intro a b₁ b₂ hab₁ hab₂ @@ -104,17 +104,17 @@ theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := SemiCo @[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent theorem commute_equivalents : - [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (MHJoin r₁ r₂), - ReflTransGen (r₁ ⊔ swap r₂) ≤ MHJoin r₁ r₂, - ReflTransGen (r₁ ⊔ swap r₂) = MHJoin r₁ r₂].TFAE := by + [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (MJoin₂ r₁ r₂), + ReflTransGen (r₁ ⊔ swap r₂) ≤ MJoin₂ r₁ r₂, + ReflTransGen (r₁ ⊔ swap r₂) = MJoin₂ r₁ r₂].TFAE := by tfae_have 1 → 2 := SemiCommute.to_commute - tfae_have 2 → 3 := Commute.isTrans_mHJoin - tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <| sup_le MHJoin.left_le MHJoin.swap_right_le + tfae_have 2 → 3 := Commute.isTrans_mJoin₂ + tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <| sup_le MJoin₂.left_le MJoin₂.swap_right_le tfae_have 4 → 5 := fun h => h.antisymm <| - MHJoin.mHJoin_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen) + MJoin₂.mJoin₂_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen) tfae_have 5 → 1 := by intro h a b₁ b₂ h₁ h₂ - rw [MHJoin.swap_iff, ← h] + rw [MJoin₂.swap_iff, ← h] exact (ReflTransGen.mono le_sup_right _ _ <| reflTransGen_swap.mpr h₂).tail (Or.inl h₁) tfae_finish @@ -275,16 +275,16 @@ theorem StronglyConfluent.to_confluent (h : StronglyConfluent r) : Confluent r : lemma Commute.join_left (c₁ : Commute r₁ r₃) (c₂ : Commute r₂ r₃) : Commute (r₁ ⊔ r₂) r₃ := by intro x y z xy xz induction xy with - | refl => grind [HJoin] + | refl => grind [Join₂] | @tail b c _ bc ih => have ⟨w, bw, _⟩ := ih cases bc with | inl bc => obtain ⟨_, _, _⟩ := c₁ (.single bc) bw - grind [HJoin, ReflTransGen.trans] + grind [Join₂, ReflTransGen.trans] | inr bc => obtain ⟨_, _, _⟩ := c₂ (.single bc) bw - grind [HJoin, ReflTransGen.trans] + grind [Join₂, ReflTransGen.trans] theorem Commute.join_confluent (c₁ : Confluent r₁) (c₂ : Confluent r₂) (comm : Commute r₁ r₂) : Confluent (r₁ ⊔ r₂) := by diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 201c5cc9b..cda05fa1f 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -36,14 +36,14 @@ def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b} def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b} /-- Generalisation of `Join` to two relations. -/ -def HJoin (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a c ∧ r₂ b c +def Join₂ (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a c ∧ r₂ b c /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/ abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) /-- Generalisation of `MJoin` to two relations. -/ -abbrev MHJoin (r₁ r₂ : α → α → Prop) := HJoin (ReflTransGen r₁) (ReflTransGen r₂) +abbrev MJoin₂ (r₁ r₂ : α → α → Prop) := Join₂ (ReflTransGen r₁) (ReflTransGen r₂) /-- The relation `r` 'up to' the relation `s`. -/ def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s) @@ -58,7 +58,7 @@ abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → /-- Generalization of `Diamond` to two relations. -/ def DiamondCommute (r₁ r₂ : α → α → Prop) := - ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → HJoin r₂ r₁ y₁ y₂ + ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → Join₂ r₂ r₁ y₁ y₂ /-- A relation is confluent when its reflexive transitive closure has the diamond property. -/ abbrev Confluent (r : α → α → Prop) := Diamond (ReflTransGen r) @@ -73,7 +73,7 @@ abbrev SemiConfluent (r : α → α → Prop) := /-- Generalisation of `SemiConfluent` to two relations. -/ abbrev SemiCommute (r₁ r₂ : α → α → Prop) := - ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → MHJoin r₂ r₁ y₁ y₂ + ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → MJoin₂ r₂ r₁ y₁ y₂ /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/ abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → MJoin r x y @@ -84,7 +84,7 @@ abbrev LocallyConfluent (r : α → α → Prop) := /-- Generalization of `LocallyConfluent` to two relations. -/ def LocallyCommute (r₁ r₂ : α → α → Prop) := - ∀ {a b c : α}, r₁ a b → r₂ a c → MHJoin r₂ r₁ b c + ∀ {a b c : α}, r₁ a b → r₂ a c → MJoin₂ r₂ r₁ b c /-- A relation is strongly confluent when single steps are reflexive- and multi-joinable. -/ abbrev StronglyConfluent (r : α → α → Prop) := From 5b91545e2e4dd28dfeb047beb61a6545293738b8 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 11 Sep 2026 10:33:08 +0200 Subject: [PATCH 09/18] grind annotations --- Cslib/Foundations/Relation/Basic.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 12702524d..5d27b9696 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -48,6 +48,7 @@ def transLeft (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s def transRight (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r where trans hab hbc := _root_.trans hab (h _ _ hbc) +@[grind .] theorem comp_le_comp {s s' r r' : α → α → Prop} (hs : s ≤ s') (hr : r ≤ r') : Comp s r ≤ Comp s' r' := fun a c ⟨b, hab, hbc⟩ ↦ ⟨b, hs a b hab, hr b c hbc⟩ @@ -59,11 +60,13 @@ theorem swap_le_iff_le_swap {r₁ r₂ : α → α → Prop} : swap r₁ ≤ r attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen +@[grind .] theorem ReflGen.le_reflGen : r ≤ ReflGen r := fun _ _ => ReflGen.single theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := EqvGen.reflGen_le_eqvGen r _ _ h +@[grind .] theorem TransGen.le_transGen : r ≤ TransGen r := fun _ _ => TransGen.single theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := @@ -72,13 +75,15 @@ theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := EqvGen.reflTransGen_le_eqvGen r _ _ h +@[grind .] theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := EqvGen.symmGen_le_eqvGen r _ _ h -@[simp] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl +@[simp, grind =] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl +@[grind .] theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel theorem _root_.Equivalence.eqvGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : EqvGen r₁ ≤ r₂ := @@ -90,7 +95,7 @@ attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.t theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩ -@[simp] theorem join₂_eq_join : Join₂ r r = Join r := rfl +@[simp, grind =] theorem join₂_eq_join : Join₂ r r = Join r := rfl @[grind =] theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl From 5be08e04dc26f18b38fcb25afa6b351a45c0da10 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 11 Sep 2026 10:34:22 +0200 Subject: [PATCH 10/18] scope grinds --- Cslib/Foundations/Relation/Basic.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 5d27b9696..e5082bdcd 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -48,7 +48,7 @@ def transLeft (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s def transRight (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r where trans hab hbc := _root_.trans hab (h _ _ hbc) -@[grind .] +@[scoped grind .] theorem comp_le_comp {s s' r r' : α → α → Prop} (hs : s ≤ s') (hr : r ≤ r') : Comp s r ≤ Comp s' r' := fun a c ⟨b, hab, hbc⟩ ↦ ⟨b, hs a b hab, hr b c hbc⟩ @@ -60,13 +60,13 @@ theorem swap_le_iff_le_swap {r₁ r₂ : α → α → Prop} : swap r₁ ≤ r attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen -@[grind .] +@[scoped grind .] theorem ReflGen.le_reflGen : r ≤ ReflGen r := fun _ _ => ReflGen.single theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := EqvGen.reflGen_le_eqvGen r _ _ h -@[grind .] +@[scoped grind .] theorem TransGen.le_transGen : r ≤ TransGen r := fun _ _ => TransGen.single theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := @@ -75,15 +75,15 @@ theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := EqvGen.reflTransGen_le_eqvGen r _ _ h -@[grind .] +@[scoped grind .] theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := EqvGen.symmGen_le_eqvGen r _ _ h -@[simp, grind =] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl +@[simp, scoped grind =] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl -@[grind .] +@[scoped grind .] theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel theorem _root_.Equivalence.eqvGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : EqvGen r₁ ≤ r₂ := @@ -95,7 +95,7 @@ attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.t theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩ -@[simp, grind =] theorem join₂_eq_join : Join₂ r r = Join r := rfl +@[simp, scoped grind =] theorem join₂_eq_join : Join₂ r r = Join r := rfl @[grind =] theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl @@ -157,7 +157,7 @@ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTra lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a := Std.Symm.symm a b -@[simp, grind =] +@[simp, scoped grind =] theorem reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := EqvGen.reflTransGen_symmGen r @[scoped grind <=] From 5208f08daed9504145b71aa32dd5e814eb2df1ac Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 12:02:20 +0200 Subject: [PATCH 11/18] review comments --- Cslib/Foundations/Relation/Basic.lean | 2 +- Cslib/Foundations/Relation/Defs.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index e5082bdcd..f55a9a382 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -97,7 +97,7 @@ theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩ @[simp, scoped grind =] theorem join₂_eq_join : Join₂ r r = Join r := rfl -@[grind =] theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl +theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl instance [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (Join₂ r₁ r₂) where refl a := ⟨a, refl a, refl a⟩ diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index cda05fa1f..ed274e4f2 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -57,7 +57,7 @@ def Preserves (r : α → α → Prop) (P : α → Prop) : Prop := ∀ ⦃a b⦄ abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → Join r b c /-- Generalization of `Diamond` to two relations. -/ -def DiamondCommute (r₁ r₂ : α → α → Prop) := +abbrev DiamondCommute (r₁ r₂ : α → α → Prop) := ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → Join₂ r₂ r₁ y₁ y₂ /-- A relation is confluent when its reflexive transitive closure has the diamond property. -/ From b7473e1e01e1db9a2f2d9606371ee3f8ab494714 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 12:07:38 +0200 Subject: [PATCH 12/18] typeChanged annotations --- Cslib/Foundations/Relation/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index f55a9a382..353f39107 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -111,10 +111,10 @@ theorem Join₂.join₂_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ theorem Join₂.swap_iff {a b : α} : Join₂ r₁ r₂ b a ↔ Join₂ r₂ r₁ a b := by grind [Join₂] -@[deprecated _root_.refl (since := "2026-09-07")] +@[deprecated _root_.refl +typeChanged (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a -@[deprecated Join.single (since := "2026-09-07")] +@[deprecated Join.single +typeChanged (since := "2026-09-07")] theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := Join.single h theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : @@ -153,7 +153,7 @@ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTra ext a b exact ⟨ReflTransGen.mono h₁ a b, reflTransGen_closed h₂ a b⟩ -@[deprecated Relation.ReflGen.stdSymm (since := "2026-09-03")] +@[deprecated Relation.ReflGen.stdSymm +typeChanged (since := "2026-09-03")] lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a := Std.Symm.symm a b From 4716f0d3f618e78b28e17b40cfb0125e57694503 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 12:25:29 +0200 Subject: [PATCH 13/18] deprecate MJoin --- Cslib/Foundations/Relation/Basic.lean | 32 ++++++++++----------- Cslib/Foundations/Relation/Confluence.lean | 33 +++++++++++++--------- Cslib/Foundations/Relation/Defs.lean | 12 ++++---- 3 files changed, 41 insertions(+), 36 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 353f39107..6f58770b2 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -117,34 +117,32 @@ theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a @[deprecated Join.single +typeChanged (since := "2026-09-07")] theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := Join.single h -theorem _root_.Equivalence.mJoin_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : - MJoin r₁ ≤ r₂ := +theorem _root_.Equivalence.join_reflTransGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : + Join (ReflTransGen r₁) ≤ r₂ := have := h.isEquiv join_le_of_equivalence_of_le h <| reflTransGen_le_of_le hle -theorem MJoin.mJoin_le_eqvGen : MJoin r ≤ EqvGen r := - (EqvGen.is_equivalence r).mJoin_le EqvGen.le_eqvGen +theorem join_reflTransGen_le_eqvGen : Join (ReflTransGen r) ≤ EqvGen r := + (EqvGen.is_equivalence r).join_reflTransGen_le EqvGen.le_eqvGen -theorem mJoin₂_eq_mJoin : MJoin₂ r r = MJoin r := rfl - -theorem MJoin₂.mJoin₂_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : - MJoin₂ r₁ r₂ ≤ r := by +theorem join₂_reflTransGen_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : + Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r := by refine Join₂.join₂_le ?_ (ReflTransGen.swap.trans ?_) <;> apply reflTransGen_le_of_le <;> assumption -theorem MJoin₂.mJoin₂_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : - MJoin₂ r₁ r₂ ≤ r := mJoin₂_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq]) +theorem join₂_reflTransGen_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r := + join₂_reflTransGen_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq]) -theorem _root_.Equivalence.mJoin₂_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : - MJoin₂ r₁ r₂ ≤ r := +theorem _root_.Equivalence.join₂_reflTransGen_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) : + Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r := have := h.isEquiv - MJoin₂.mJoin₂_le_of_isEquiv h₁ h₂ - -theorem MJoin₂.swap_iff : MJoin₂ r₁ r₂ b a ↔ MJoin₂ r₂ r₁ a b := Join₂.swap_iff + join₂_reflTransGen_le_of_isEquiv h₁ h₂ -theorem MJoin₂.left_le : r₁ ≤ MJoin₂ r₁ r₂ := fun _ _ h => Join₂.single_left (.single h) +theorem left_le_join₂_reflTransGen : r₁ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂) := + fun _ _ h => Join₂.single_left (.single h) -theorem MJoin₂.swap_right_le : swap r₂ ≤ MJoin₂ r₁ r₂ := +theorem swap_right_le_join₂_reflTransGen : swap r₂ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂) := fun _ _ h => Join₂.single_right (.single h) /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/ diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 89654a19e..7a090b5e8 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -56,7 +56,7 @@ instance : Std.Symm (@Commute α) where symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, Join₂] lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : - MJoin₂ r₂ r₁ b c := by + Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c := by induction h₁ using ReflTransGen.head_induction_on generalizing c with | refl => exact Join₂.single_left (.single h₂) | head ha _ ih => @@ -82,13 +82,15 @@ theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_ @[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent -theorem Commute.isTrans_mJoin₂ (h : Commute r₁ r₂) : IsTrans α (MJoin₂ r₁ r₂) where +theorem Commute.isTrans_join₂_reflTransGen (h : Commute r₁ r₂) : + IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)) where trans a b c := by intro ⟨d, had, hbd⟩ ⟨d', hbd', hcd'⟩ obtain ⟨e, he, he'⟩ := h hbd' hbd exact ⟨e, had.trans he', hcd'.trans he⟩ -theorem Confluent.isTrans_mJoin (h : Confluent r) : IsTrans α (MJoin r) := Commute.isTrans_mJoin₂ h +theorem Confluent.isTrans_join_reflTransGen (h : Confluent r) : IsTrans α (Join (ReflTransGen r)) := + Commute.isTrans_join₂_reflTransGen h theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by intro a b₁ b₂ hab₁ hab₂ @@ -104,26 +106,29 @@ theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := SemiCo @[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent theorem commute_equivalents : - [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (MJoin₂ r₁ r₂), - ReflTransGen (r₁ ⊔ swap r₂) ≤ MJoin₂ r₁ r₂, - ReflTransGen (r₁ ⊔ swap r₂) = MJoin₂ r₁ r₂].TFAE := by + [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)), + ReflTransGen (r₁ ⊔ swap r₂) ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂), + ReflTransGen (r₁ ⊔ swap r₂) = Join₂ (ReflTransGen r₁) (ReflTransGen r₂)].TFAE := by tfae_have 1 → 2 := SemiCommute.to_commute - tfae_have 2 → 3 := Commute.isTrans_mJoin₂ - tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <| sup_le MJoin₂.left_le MJoin₂.swap_right_le + tfae_have 2 → 3 := Commute.isTrans_join₂_reflTransGen + tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <| + sup_le left_le_join₂_reflTransGen swap_right_le_join₂_reflTransGen tfae_have 4 → 5 := fun h => h.antisymm <| - MJoin₂.mJoin₂_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen) + join₂_reflTransGen_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen) tfae_have 5 → 1 := by intro h a b₁ b₂ h₁ h₂ - rw [MJoin₂.swap_iff, ← h] + rw [Join₂.swap_iff, ← h] exact (ReflTransGen.mono le_sup_right _ _ <| reflTransGen_swap.mpr h₂).tail (Or.inl h₁) tfae_finish -theorem churchRosser_iff_eqvGen_le_mJoin : ChurchRosser r ↔ EqvGen r ≤ MJoin r := Iff.rfl +theorem churchRosser_iff_eqvGen_le_join_reflTransGen : + ChurchRosser r ↔ EqvGen r ≤ Join (ReflTransGen r) := + Iff.rfl theorem confluent_equivalents : - [ChurchRosser r, SemiConfluent r, Confluent r, IsTrans α (MJoin r), - EqvGen r ≤ MJoin r, EqvGen r = MJoin r].TFAE := by - refine (List.tfae_cons ?_).mpr ⟨churchRosser_iff_eqvGen_le_mJoin, ?_⟩ + [ChurchRosser r, SemiConfluent r, Confluent r, IsTrans α (Join (ReflTransGen r)), + EqvGen r ≤ Join (ReflTransGen r), EqvGen r = Join (ReflTransGen r)].TFAE := by + refine (List.tfae_cons ?_).mpr ⟨churchRosser_iff_eqvGen_le_join_reflTransGen, ?_⟩ · grind · simpa [reflTransGen_symmGen] using commute_equivalents (r₁ := r) (r₂ := r) diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index ed274e4f2..1cbc1261f 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -40,9 +40,11 @@ def Join₂ (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/ +@[deprecated "use `Join (ReflTrasnGen ·)` instead" (since := "2026-09-12")] abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) /-- Generalisation of `MJoin` to two relations. -/ +@[deprecated "use Join₂ (ReflTransGen ·) (ReflTransGen ·) instead." (since := "2026-09-12")] abbrev MJoin₂ (r₁ r₂ : α → α → Prop) := Join₂ (ReflTransGen r₁) (ReflTransGen r₂) /-- The relation `r` 'up to' the relation `s`. -/ @@ -69,22 +71,22 @@ abbrev Commute (r₁ r₂ : α → α → Prop) := DiamondCommute (ReflTransGen /-- A relation is semi-confluent when single and multiple steps with common origin are multi-joinable. -/ abbrev SemiConfluent (r : α → α → Prop) := - ∀ {x y₁ y₂}, r x y₁ → ReflTransGen r x y₂ → MJoin r y₁ y₂ + ∀ {x y₁ y₂}, r x y₁ → ReflTransGen r x y₂ → Join (ReflTransGen r) y₁ y₂ /-- Generalisation of `SemiConfluent` to two relations. -/ abbrev SemiCommute (r₁ r₂ : α → α → Prop) := - ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → MJoin₂ r₂ r₁ y₁ y₂ + ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → Join₂ (ReflTransGen r₂) (ReflTransGen r₁) y₁ y₂ /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/ -abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → MJoin r x y +abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join (ReflTransGen r) x y /-- A relation is locally confluent when all reductions with a common origin are multi-joinable -/ abbrev LocallyConfluent (r : α → α → Prop) := - ∀ {a b c : α}, r a b → r a c → MJoin r b c + ∀ {a b c : α}, r a b → r a c → Join (ReflTransGen r) b c /-- Generalization of `LocallyConfluent` to two relations. -/ def LocallyCommute (r₁ r₂ : α → α → Prop) := - ∀ {a b c : α}, r₁ a b → r₂ a c → MJoin₂ r₂ r₁ b c + ∀ {a b c : α}, r₁ a b → r₂ a c → Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c /-- A relation is strongly confluent when single steps are reflexive- and multi-joinable. -/ abbrev StronglyConfluent (r : α → α → Prop) := From 2c8f99fb42202670fb4ff0a09719ae393f9ccd86 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 12:35:52 +0200 Subject: [PATCH 14/18] generalise DiamondCommute.extend --- Cslib/Foundations/Relation/Basic.lean | 3 +++ Cslib/Foundations/Relation/Confluence.lean | 11 ++++++++--- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean index 6f58770b2..9369e346c 100644 --- a/Cslib/Foundations/Relation/Basic.lean +++ b/Cslib/Foundations/Relation/Basic.lean @@ -111,6 +111,9 @@ theorem Join₂.join₂_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ theorem Join₂.swap_iff {a b : α} : Join₂ r₁ r₂ b a ↔ Join₂ r₂ r₁ a b := by grind [Join₂] +protected theorem Join₂.mono (h₁ : r₁ ≤ r₁') (h₂ : r₂ ≤ r₂') : Join₂ r₁ r₂ ≤ Join₂ r₁' r₂' := + fun x y ⟨z, hxz, hyz⟩ => ⟨z, h₁ x z hxz, h₂ y z hyz⟩ + @[deprecated _root_.refl +typeChanged (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 7a090b5e8..969f510d3 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -55,15 +55,20 @@ theorem Commute.to_confluent : Commute r r = Confluent r := rfl instance : Std.Symm (@Commute α) where symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, Join₂] -lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : - Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c := by +lemma DiamondCommute.diamond_commute_reflTransGen_left (h : DiamondCommute r₁ r₂) : + DiamondCommute (ReflTransGen r₁) r₂ := by + intro a b c h₁ h₂ induction h₁ using ReflTransGen.head_induction_on generalizing c with - | refl => exact Join₂.single_left (.single h₂) + | refl => exact Join₂.single_left h₂ | head ha _ ih => obtain ⟨d, had, hcd⟩ := h ha h₂ obtain ⟨d', hbd', hdd'⟩ := ih had exact ⟨d', hbd', hdd'.head hcd⟩ +lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : + Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c := + Join₂.mono ReflTransGen.le_reflTransGen le_rfl _ _ <| h.diamond_commute_reflTransGen_left h₁ h₂ + /-- Extending a multistep reduction by a single step preserves multi-joinability. -/ lemma Diamond.extend (h : Diamond r) : ReflTransGen r a b → r a c → Join (ReflTransGen r) b c := DiamondCommute.extend h From 59f9b050bea0b526b7fb05a08e33146c1f34a299 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 12:47:03 +0200 Subject: [PATCH 15/18] fix build combinatory logic --- Cslib/Languages/CombinatoryLogic/Basic.lean | 2 +- .../CombinatoryLogic/Confluence.lean | 16 +++---- Cslib/Languages/CombinatoryLogic/Defs.lean | 10 ++++- .../CombinatoryLogic/Evaluation.lean | 44 +++++++++++-------- 4 files changed, 42 insertions(+), 30 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index 579fb5aa4..04488c220 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -223,7 +223,7 @@ theorem Y_def (f : SKI) : (Y ⬝ f) ↠ H ⬝ f ⬝ (H ⬝ f) := YPoly.toSKI_correct [f] (by simp) /-- The fixed-point property of the Y-combinator -/ -theorem Y_correct (f : SKI) : MJoin Red (Y ⬝ f) (f ⬝ (Y ⬝ f)) := by +theorem Y_correct (f : SKI) : Join (ReflTransGen Red) (Y ⬝ f) (f ⬝ (Y ⬝ f)) := by use f ⬝ (H ⬝ f ⬝ (H ⬝ f)) constructor · exact Trans.trans (Y_def f) (H_def f (H ⬝ f)) diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index 053ab299c..a59ea5cfc 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -16,8 +16,8 @@ This file proves the **Church-Rosser** theorem for the SKI calculus, that is, if `a ↠ c`, `b ↠ d` and `c ↠ d` for some term `d`. More strongly (though equivalently), we show that the relation of having a common reduct is transitive — in the above situation, `a` and `b`, and `a` and `c` have common reducts, so the result implies the same of `b` and `c`. Note that -`MJoin Red` is symmetric (trivially) and reflexive (since `↠` is), so we in fact show that -`MJoin Red` is an equivalence. +`Join (ReflTransGen Red)` is symmetric (trivially) and reflexive (since `↠` is), so we in fact show +that `Join (ReflTransGen Red)` is an equivalence. Our proof follows the method of Tait and Martin-Löf for the lambda calculus, as presented for instance in @@ -33,7 +33,7 @@ reduction on the head and tail of a term. - `parallelReduction_diamond` : parallel reduction satisfies the diamond property, that is, it is confluent in a single step. -- `mJoin_red_equivalence` : by a general result, the diamond property for `⭢ₚ` implies the same +- `join_mRed_equivalence` : by a general result, the diamond property for `⭢ₚ` implies the same for its reflexive-transitive closure. This closure is exactly `↠`, which implies the **Church-Rosser** theorem as sketched above. -/ @@ -205,19 +205,19 @@ theorem parallelReduction_diamond : Diamond ParallelReduction := by case red_S => exact ⟨a ⬝ c ⬝ (b ⬝ c), .refl _, .refl _,⟩ theorem join_parallelReduction_equivalence : - Equivalence (MJoin ParallelReduction) := + Equivalence (Join (ReflTransGen ParallelReduction)) := Confluent.equivalence_join_reflTransGen <| Diamond.to_confluent parallelReduction_diamond /-- The **Church-Rosser** theorem in its general form. -/ -theorem mJoin_red_equivalence : Equivalence (MJoin Red) := by - rw [MJoin, ←reflTransGen_parallelReduction_mRed] +theorem join_mRed_equivalence : Equivalence (Join (ReflTransGen Red)) := by + rw [←reflTransGen_parallelReduction_mRed] exact join_parallelReduction_equivalence /-- The **Church-Rosser** theorem in the form it is usually stated. -/ theorem MRed.diamond : Confluent Red := by intro a b c hab hac - apply mJoin_red_equivalence.trans (y := a) - · exact mJoin_red_equivalence.symm (Join.single hab) + apply join_mRed_equivalence.trans (y := a) + · exact join_mRed_equivalence.symm (Join.single hab) · exact Join.single hac end SKI diff --git a/Cslib/Languages/CombinatoryLogic/Defs.lean b/Cslib/Languages/CombinatoryLogic/Defs.lean index 7d028d283..ea8aedce7 100644 --- a/Cslib/Languages/CombinatoryLogic/Defs.lean +++ b/Cslib/Languages/CombinatoryLogic/Defs.lean @@ -113,12 +113,18 @@ lemma parallel_mRed {a a' b b' : SKI} (ha : a ↠ a') (hb : b ↠ b') : lemma parallel_red {a a' b b' : SKI} (ha : a ⭢ a') (hb : b ⭢ b') : (a ⬝ b) ↠ (a' ⬝ b') := by trans a' ⬝ b <;> grind -theorem mJoin_red_head {x x' : SKI} (y : SKI) : MJoin Red x x' → MJoin Red (x ⬝ y) (x' ⬝ y) +theorem join_mRed_head {x x' : SKI} (y : SKI) : + Join (ReflTransGen Red) x x' → Join (ReflTransGen Red) (x ⬝ y) (x' ⬝ y) | ⟨z, hz, hz'⟩ => ⟨z ⬝ y, MRed.head y hz, MRed.head y hz'⟩ -theorem mJoin_red_tail (x : SKI) {y y' : SKI} : MJoin Red y y' → MJoin Red (x ⬝ y) (x ⬝ y') +@[deprecated (since := "2026-09-12")] alias mJoin_red_head := join_mRed_head + +theorem join_mRed_tail (x : SKI) {y y' : SKI} : + Join (ReflTransGen Red) y y' → Join (ReflTransGen Red) (x ⬝ y) (x ⬝ y') | ⟨z, hz, hz'⟩ => ⟨x ⬝ z, MRed.tail x hz, MRed.tail x hz'⟩ +@[deprecated (since := "2026-09-12")] alias mJoin_red_tail := join_mRed_tail + end SKI end Cslib diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean index b4c08550c..f2fa26a80 100644 --- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean +++ b/Cslib/Languages/CombinatoryLogic/Evaluation.lean @@ -178,10 +178,13 @@ theorem redexFree_iff_mred_eq {x : SKI} : x.RedexFree ↔ ∀ y, (x ↠ y) ↔ x exact Red.ne hy (h.1 (Relation.ReflTransGen.single hy)) /-- If a term has a common reduct with a normal term, it in fact reduces to that term. -/ -theorem mJoin_red_redexFree {x y : SKI} (hy : y.RedexFree) (h : MJoin Red x y) : x ↠ y := +theorem join_mRed_redexFree {x y : SKI} (hy : y.RedexFree) (h : Join (ReflTransGen Red) x y) : + x ↠ y := let ⟨w, hyw, hzw⟩ := h (redexFree_iff_mred_eq.1 hy _ |>.1 hzw : y = w) ▸ hyw +@[deprecated (since := "2026-09-12")] alias mJoin_red_redexFree := join_mRed_redexFree + /-- If `x` reduces to both `y` and `z`, and `z` is not reducible, then `y` reduces to `z`. -/ lemma confluent_redexFree {x y z : SKI} (hxy : x ↠ y) (hxz : x ↠ z) (hz : RedexFree z) : y ↠ z := let ⟨w, hyw, hzw⟩ := MRed.diamond hxy hxz @@ -195,13 +198,16 @@ lemma unique_normal_form {x y z : SKI} (redexFree_iff_mred_eq.1 hy _).1 (confluent_redexFree hxy hxz hz) /-- If `x` and `y` are normal and have a common reduct, then they are equal. -/ -lemma eq_of_mJoin_red_redexFree {x y : SKI} (h : MJoin Red x y) +lemma eq_of_join_mRed_redexFree {x y : SKI} (h : Join (ReflTransGen Red) x y) (hx : x.RedexFree) (hy : y.RedexFree) : x = y := - (redexFree_iff_mred_eq.1 hx _).1 (mJoin_red_redexFree hy h) + (redexFree_iff_mred_eq.1 hx _).1 (join_mRed_redexFree hy h) + +@[deprecated (since := "2026-09-12")] alias eq_of_mJoin_red_redexFree := eq_of_join_mRed_redexFree + /-! ### Injectivity for datatypes -/ -lemma sk_nequiv : ¬ MJoin Red S K := by +lemma sk_nequiv : ¬ Join (ReflTransGen Red) S K := by intro ⟨z, hsz, hkz⟩ have hS : RedexFree S := by simp [RedexFree] have hK : RedexFree K := by simp [RedexFree] @@ -210,19 +216,19 @@ lemma sk_nequiv : ¬ MJoin Red S K := by /-- Injectivity for booleans. -/ theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y) - (hxy : MJoin Red x y) : u = v := by - have h : MJoin Red (if u then S else K) (if v then S else K) := by - apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K) - · apply mJoin_red_equivalence.symm + (hxy : Join (ReflTransGen Red) x y) : u = v := by + have h : Join (ReflTransGen Red) (if u then S else K) (if v then S else K) := by + apply join_mRed_equivalence.trans (y := x ⬝ S ⬝ K) + · apply join_mRed_equivalence.symm apply Relation.Join.single exact hx S K - · apply mJoin_red_equivalence.trans (y := y ⬝ S ⬝ K) - · exact mJoin_red_head K <| mJoin_red_head S hxy + · apply join_mRed_equivalence.trans (y := y ⬝ S ⬝ K) + · exact join_mRed_head K <| join_mRed_head S hxy · apply Relation.Join.single exact hy S K - grind [sk_nequiv, mJoin_red_equivalence.symm h] + grind [sk_nequiv, join_mRed_equivalence.symm h] -lemma TF_nequiv : ¬ MJoin Red TT FF := fun h => +lemma TF_nequiv : ¬ Join (ReflTransGen Red) TT FF := fun h => (Bool.eq_not_self true).mp <| isBool_injective TT FF true false TT_correct FF_correct h /-- A specialisation of `Church : Nat → SKI`. -/ @@ -248,15 +254,15 @@ lemma churchK_injective : Function.Injective churchK := /-- Injectivity for Church numerals -/ theorem isChurch_injective (x y : SKI) (n m : Nat) (hx : IsChurch n x) (hy : IsChurch m y) - (hxy : MJoin Red x y) : n = m := by - suffices MJoin Red (churchK n) (churchK m) by + (hxy : Join (ReflTransGen Red) x y) : n = m := by + suffices Join (ReflTransGen Red) (churchK n) (churchK m) by apply churchK_injective - exact eq_of_mJoin_red_redexFree this (churchK_redexFree n) (churchK_redexFree m) - apply mJoin_red_equivalence.trans (y := x ⬝ K ⬝ K) + exact eq_of_join_mRed_redexFree this (churchK_redexFree n) (churchK_redexFree m) + apply join_mRed_equivalence.trans (y := x ⬝ K ⬝ K) · simp_rw [churchK_church] - exact mJoin_red_equivalence.symm <| Relation.Join.single (hx K K) - · apply mJoin_red_equivalence.trans (y := y ⬝ K ⬝ K) - · apply mJoin_red_head; apply mJoin_red_head; assumption + exact join_mRed_equivalence.symm <| Relation.Join.single (hx K K) + · apply join_mRed_equivalence.trans (y := y ⬝ K ⬝ K) + · apply join_mRed_head; apply join_mRed_head; assumption · simp_rw [churchK_church] exact Relation.Join.single (hy K K) From 0e5cb48ca9b9a067d827a725d861a0a491b9b600 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 12 Sep 2026 18:42:52 +0200 Subject: [PATCH 16/18] further cleanup --- Cslib/Foundations/Relation/Confluence.lean | 46 ++++++++++------------ 1 file changed, 21 insertions(+), 25 deletions(-) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 969f510d3..6e80581bd 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -55,37 +55,24 @@ theorem Commute.to_confluent : Commute r r = Confluent r := rfl instance : Std.Symm (@Commute α) where symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, Join₂] -lemma DiamondCommute.diamond_commute_reflTransGen_left (h : DiamondCommute r₁ r₂) : - DiamondCommute (ReflTransGen r₁) r₂ := by +lemma DiamondCommute.diamond_commute_reflTransGen_right (h : DiamondCommute r₁ r₂) : + DiamondCommute r₁ (ReflTransGen r₂) := by intro a b c h₁ h₂ - induction h₁ using ReflTransGen.head_induction_on generalizing c with - | refl => exact Join₂.single_left h₂ + induction h₂ using ReflTransGen.head_induction_on generalizing b with + | refl => exact Join₂.single_right h₁ | head ha _ ih => - obtain ⟨d, had, hcd⟩ := h ha h₂ - obtain ⟨d', hbd', hdd'⟩ := ih had - exact ⟨d', hbd', hdd'.head hcd⟩ + obtain ⟨d, hbd, hcd⟩ := h h₁ ha + obtain ⟨d', hdd', hcd'⟩ := ih hcd + exact ⟨d', hdd'.head hbd, hcd'⟩ -lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) (h₁ : ReflTransGen r₁ a b) (h₂ : r₂ a c) : - Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c := - Join₂.mono ReflTransGen.le_reflTransGen le_rfl _ _ <| h.diamond_commute_reflTransGen_left h₁ h₂ +lemma DiamondCommute.to_semiCommute (h : DiamondCommute r₁ r₂) : SemiCommute r₁ r₂ := + fun h₁ h₂ => Join₂.mono le_rfl ReflTransGen.le_reflTransGen _ _ <| + h.diamond_commute_reflTransGen_right h₁ h₂ /-- Extending a multistep reduction by a single step preserves multi-joinability. -/ -lemma Diamond.extend (h : Diamond r) : - ReflTransGen r a b → r a c → Join (ReflTransGen r) b c := DiamondCommute.extend h +lemma Diamond.to_semiConfluent (h : Diamond r) : SemiConfluent r := DiamondCommute.to_semiCommute h -lemma DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := by - intro a b₁ b₂ hab₁ hab₂ - induction hab₂ using ReflTransGen.head_induction_on generalizing b₁ with - | refl => exact Join₂.single_right hab₁ - | @head a a' ha hab₂ ih => - obtain ⟨c, hb₁c, hac⟩ := h.extend hab₁ ha - obtain ⟨d, hcd, hb₂d⟩ := ih hac - exact ⟨d, hb₁c.trans hcd, hb₂d⟩ - -/-- The diamond property implies confluence. -/ -theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_commute h - -@[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent +@[deprecated (since := "2026-09-12")] alias Diamond.extend := Diamond.to_semiConfluent theorem Commute.isTrans_join₂_reflTransGen (h : Commute r₁ r₂) : IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)) where @@ -126,6 +113,11 @@ theorem commute_equivalents : exact (ReflTransGen.mono le_sup_right _ _ <| reflTransGen_swap.mpr h₂).tail (Or.inl h₁) tfae_finish +theorem semiCommute_iff_commute : SemiCommute r₁ r₂ ↔ Commute r₁ r₂ := commute_equivalents.out 1 2 + +theorem DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := + semiCommute_iff_commute.mp h.to_semiCommute + theorem churchRosser_iff_eqvGen_le_join_reflTransGen : ChurchRosser r ↔ EqvGen r ≤ Join (ReflTransGen r) := Iff.rfl @@ -158,6 +150,10 @@ theorem confluent_iff_semiConfluent : Confluent r ↔ SemiConfluent r := @[deprecated (since := "2026-09-03")] alias Confluent_iff_SemiConfluent := confluent_iff_semiConfluent +theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_commute h + +@[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent + theorem confluent_of_unique_end {x : α} (h : ∀ y : α, ReflTransGen r y x) : Confluent r := by intro a b c hab hac exact ⟨x, h b, h c⟩ From cff88806811cab039e2a100ff8bfc26f1cfc9c9b Mon Sep 17 00:00:00 2001 From: twwar Date: Sun, 13 Sep 2026 15:29:45 +0200 Subject: [PATCH 17/18] remove MJoin2 --- Cslib/Foundations/Relation/Defs.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 1cbc1261f..07a6980e1 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -43,10 +43,6 @@ def Join₂ (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a @[deprecated "use `Join (ReflTrasnGen ·)` instead" (since := "2026-09-12")] abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) -/-- Generalisation of `MJoin` to two relations. -/ -@[deprecated "use Join₂ (ReflTransGen ·) (ReflTransGen ·) instead." (since := "2026-09-12")] -abbrev MJoin₂ (r₁ r₂ : α → α → Prop) := Join₂ (ReflTransGen r₁) (ReflTransGen r₂) - /-- The relation `r` 'up to' the relation `s`. -/ def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s) From cfb09132e91a1dbc0f76a9ceb6f684bbc7693baf Mon Sep 17 00:00:00 2001 From: twwar Date: Sun, 13 Sep 2026 15:44:29 +0200 Subject: [PATCH 18/18] symmetrise --- Cslib/Foundations/Relation/Confluence.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 6e80581bd..94b028824 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -52,8 +52,11 @@ theorem Commute.to_confluent : Commute r r = Confluent r := rfl @[simp] theorem LocallyCommute.to_locallyConfluent : LocallyCommute r r = LocallyConfluent r := rfl -instance : Std.Symm (@Commute α) where - symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁, Join₂] +instance : Std.Symm (@DiamondCommute α) where + symm _ _ h _ _ _ h₁ h₂ := Join₂.swap_iff.mp <| h h₂ h₁ + +instance : Std.Symm (@LocallyCommute α) where + symm _ _ h _ _ _ h₁ h₂ := Join₂.swap_iff.mp <| h h₂ h₁ lemma DiamondCommute.diamond_commute_reflTransGen_right (h : DiamondCommute r₁ r₂) : DiamondCommute r₁ (ReflTransGen r₂) := by @@ -65,6 +68,11 @@ lemma DiamondCommute.diamond_commute_reflTransGen_right (h : DiamondCommute r₁ obtain ⟨d', hdd', hcd'⟩ := ih hcd exact ⟨d', hdd'.head hbd, hcd'⟩ +lemma DiamondCommute.diamond_commute_reflTransGen_left (h : DiamondCommute r₁ r₂) : + DiamondCommute (ReflTransGen r₁) r₂ := by + rw [comm (r := DiamondCommute)] at h ⊢ + exact h.diamond_commute_reflTransGen_right + lemma DiamondCommute.to_semiCommute (h : DiamondCommute r₁ r₂) : SemiCommute r₁ r₂ := fun h₁ h₂ => Join₂.mono le_rfl ReflTransGen.le_reflTransGen _ _ <| h.diamond_commute_reflTransGen_right h₁ h₂ @@ -118,6 +126,11 @@ theorem semiCommute_iff_commute : SemiCommute r₁ r₂ ↔ Commute r₁ r₂ := theorem DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := semiCommute_iff_commute.mp h.to_semiCommute +instance : Std.Symm (@SemiCommute α) where + symm r₁ r₂ h := by + rw [semiCommute_iff_commute] at h ⊢ + exact symm (r := Commute) h + theorem churchRosser_iff_eqvGen_le_join_reflTransGen : ChurchRosser r ↔ EqvGen r ≤ Join (ReflTransGen r) := Iff.rfl