From 5fdc1f88327dcbcf1835442529ccec808d8276ce Mon Sep 17 00:00:00 2001 From: lengyijun Date: Tue, 21 Jul 2026 12:35:43 +0800 Subject: [PATCH 1/2] feat: Add lemma SN.to_WN: SN implies Normalizable `SN.to_WN (hx : SN r x) : Normalizable r x` Proves that strong normalization implies weak normalization by induction on the SN structure, constructing the normal form via the single reduction step when a successor exists. --- Cslib/Foundations/Relation/Confluence.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index b6f57c79d..4d3f90b35 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -187,6 +187,14 @@ lemma SN.onFun_of_image {r : β → β → Prop} {f : α → β} (hx : SN r (f x lemma SN.of_normal (hx : Normal r x) : SN r x := SN.intro fun y hy => (hx ⟨y, hy⟩).elim +lemma SN.to_WN (hx : SN r x) : Normalizable r x := by + induction hx with | intro x h ih => + by_cases hy: (∃ y, r x y) + · obtain ⟨y, hy⟩ := hy + obtain ⟨z, hz, hnormal⟩ := ih y hy + exact ⟨z, .trans (.single hy) hz, hnormal⟩ + · exists x + lemma Terminating.apply (hr : Terminating r) (x : α) : SN r x := WellFounded.apply hr x lemma Terminating.iff_forall_sn : Terminating r ↔ ∀ x, SN r x := From e3c603f6f9de9a0fd32535373cde01fd2727d49a Mon Sep 17 00:00:00 2001 From: lengyijun Date: Sun, 9 Aug 2026 20:38:33 +0800 Subject: [PATCH 2/2] reprove SN.isNormalizable --- Cslib/Foundations/Relation/Confluence.lean | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean index 4d3f90b35..855c1258a 100644 --- a/Cslib/Foundations/Relation/Confluence.lean +++ b/Cslib/Foundations/Relation/Confluence.lean @@ -187,7 +187,7 @@ lemma SN.onFun_of_image {r : β → β → Prop} {f : α → β} (hx : SN r (f x lemma SN.of_normal (hx : Normal r x) : SN r x := SN.intro fun y hy => (hx ⟨y, hy⟩).elim -lemma SN.to_WN (hx : SN r x) : Normalizable r x := by +theorem SN.normalizable (hx : SN r x) : Normalizable r x := by induction hx with | intro x h ih => by_cases hy: (∃ y, r x y) · obtain ⟨y, hy⟩ := hy @@ -228,17 +228,8 @@ lemma Terminating.subtype_sn (r : α → α → Prop) : Terminating (α := {x // SN r x}) (fun a b => r a b) := iff_forall_sn.mpr fun x => x.property.onFun_of_image -theorem SN.isNormalizable (hx : SN r x) : Normalizable r x := by - -- restrict to the subtype where all elements are `SN`, so `flip r` is well-founded - obtain ⟨⟨y, hsn⟩, hred : ReflTransGen r x y, hnorm⟩ := - (Terminating.subtype_sn r).has_min - (s := Subtype.val ⁻¹' ({y | ReflTransGen r x y})) ⟨⟨x, hx⟩, ReflTransGen.refl⟩ - use y, hred - intro ⟨z, hyz⟩ - exact hnorm ⟨z, hsn.of_rel hyz⟩ (.tail hred hyz) hyz - theorem Terminating.isNormalizing (hr : Terminating r) : Normalizing r := - fun x => (hr.apply x).isNormalizable + fun x => (hr.apply x).normalizable theorem Terminating.isConfluent_iff_all_unique_Normal (ht : Terminating r) : Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n := by