feat(Foundations/Data/Relation): strongly normalising elements of a type equipped with a relation (#549)

thomaskwaring · twwar · chenson2018 · web-flow · commit cdfe65513343 · 2026-05-06T20:26:29.000Z
This PR defines a predicate `SN r x` (better naming suggestions welcome)
expressing that there is no infinite chain of `r`-related elements
starting with `x`. This extends the definition of `Terminating` using
`WellFounded` to individual elements, using `Acc`.

---

I'm very open to being told this is not a useful generalisation /
abstraction, but the existing API for `Acc` does seem to make certain
proofs easier. For instance, `sn_app_left` in
`LambdaCalculus/LocallyNameless/Untyped/StrongNorm` falls out as
reduction on `M` is a subrelation of reduction on `M.app N`.

---------

Co-authored-by: twwar &lt;tom.waring@unimelb.edu.au&gt;
Co-authored-by: Chris Henson &lt;46805207+chenson2018@users.noreply.github.com&gt;
diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
@@ -203,38 +203,91 @@ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) :
   apply equivalence_join
   grind
 
+/-- An element `x` is `SN` (for strongly-normalising) for a relation `r` if it is accesible under
+the inverse of `r`. -/
+abbrev SN (r : α → α → Prop) := Acc (fun a b => r b a)
+
+lemma SN_iff_SN_of_rel (x : α) : SN r x ↔ ∀ y, r x y → SN r y := by grind [Acc]
+
+lemma SN.intro : (h : ∀ y, r x y → SN r y) → SN r x := (SN_iff_SN_of_rel x).mpr
+
+lemma SN.of_rel (hx : SN r x) (h : r x y) : SN r y := Acc.inv hx h
+
+@[grind →]
+lemma SN.of_rel_reflTransGen (hx : SN r x) (h : ReflTransGen r x y) : SN r y := by
+  induction h with
+  | refl => exact hx
+  | tail _ h ih => exact ih.of_rel h
+
+lemma SN.transGen (hx : SN r x) : SN (TransGen r) x := by
+  have eq : TransGen (Function.swap r) = (fun a b => TransGen r b a) := by
+    ext
+    exact transGen_swap
+  simpa [eq] using Acc.transGen hx
+
+lemma SN.of_le {r' : α → α → Prop} (hx : SN r x) (h : r' ≤ r) : SN r' x := by
+  refine Subrelation.accessible ?_ hx
+  exact subrelation_iff_le.mpr fun {x y} => h y x
+
+@[simp]
+lemma SN.iff_transGen (x : α) : SN (TransGen r) x ↔ SN r x :=
+  ⟨fun hx => hx.of_le <| fun _ _ => TransGen.single, transGen⟩
+
+/-- `SN r x` is equivalent to the more elementary definition, that there is no infinite sequence
+of reductions starting with `x`. -/
+theorem SN.iff_isEmpty_chain :
+    SN r x ↔ IsEmpty {f : ℕ → α | f 0 = x ∧ ∀ n, r (f n) (f (n + 1))} :=
+  acc_iff_isEmpty_descending_chain
+
+lemma SN.onFun_of_image {r : β → β → Prop} {f : α → β} (hx : SN r (f x)) :
+    SN (Function.onFun r f) x := InvImage.accessible f hx
+
+lemma SN.of_normal (hx : Normal r x) : SN r x := SN.intro fun y hy => (hx ⟨y, hy⟩).elim
+
 /-- 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. -/
 abbrev Terminating (r : α → α → Prop) := WellFounded (fun a b => r b a)
 
+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 :=
+  ⟨WellFounded.apply, WellFounded.intro⟩
+
 theorem Terminating.toTransGen (ht : Terminating r) : Terminating (TransGen r) := by
-  suffices _ : (fun a b => TransGen r b a) = TransGen (Function.swap r) by grind
-  grind [transGen_swap]
+  simp_rw [iff_forall_sn, SN.iff_transGen] at ht ⊢
+  exact ht
 
 theorem Terminating.ofTransGen : Terminating (TransGen r) → Terminating r := by
-  suffices _ : (fun a b => TransGen r b a) = TransGen (Function.swap r) by grind
-  grind [transGen_swap]
+  simp_rw [iff_forall_sn, SN.iff_transGen]
+  exact id
+
+theorem Terminating.iff_transGen : Terminating (TransGen r) ↔ Terminating r := by
+  simp_rw [iff_forall_sn, SN.iff_transGen]
 
-theorem Terminating.iff_transGen : Terminating (TransGen r) ↔ Terminating r :=
-  ⟨ofTransGen, toTransGen⟩
+theorem Terminating.iff_isEmpty_chain :
+    Terminating r ↔ IsEmpty {f : ℕ → α // ∀ n, r (f n) (f (n + 1))} :=
+  wellFounded_iff_isEmpty_descending_chain
 
-theorem Terminating.subrelation {r' : α → α → Prop} (hr : Terminating r) (h : Subrelation r' r) :
+theorem Terminating.of_le {r' : α → α → Prop} (hr : Terminating r) (h : r' ≤ r) :
     Terminating r' := by
-  rw [Terminating, wellFounded_iff_isEmpty_descending_chain] at hr ⊢
-  rw [isEmpty_subtype]
-  intro f hf
-  exact hr.elim ⟨f, fun n ↦ by exact h (hf n)⟩
-
-theorem Terminating.isNormalizing (h : Terminating r) : Normalizing r := by
-  unfold Terminating at h
-  intro t
-  apply WellFounded.induction h t
-  intro a ih
-  by_cases ha : Reducible r a
-  · obtain ⟨b, hab⟩ := ha
-    obtain ⟨n, hbn, hn⟩ := ih b hab
-    exact ⟨n, ReflTransGen.head hab hbn, hn⟩
-  · use a
+  rw [iff_forall_sn] at hr ⊢
+  exact fun x => (hr x).of_le h
+
+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
 
 theorem Terminating.isConfluent_iff_all_unique_Normal (ht : Terminating r) :
     Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -26,7 +26,7 @@ universe u v
 
 namespace LambdaCalculus.LocallyNameless.Stlc
 
-open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term
+open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term Relation
 
 variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
 
@@ -43,9 +43,9 @@ open scoped Term
 @[scoped grind]
 structure Saturated (S : Set (Term Var)) : Prop where
   lc : ∀ M ∈ S, LC M
-  sn : ∀ M ∈ S, SN M
+  sn : ∀ M ∈ S, SN FullBeta M
   neutal_lc : ∀ M, Neutral M → LC M → M ∈ S
-  multiApp : ∀ M N P, LC N → SN N → multiApp (M ^ N) P ∈ S → multiApp (M.abs.app N) P ∈ S
+  multiApp : ∀ M N P, LC N → SN FullBeta N → multiApp (M ^ N) P ∈ S → multiApp (M.abs.app N) P ∈ S
 
 /-- The semantic map maps each type to a corresponding saturated set of terms.
     For the strong normalization proof to work, we must ensure that
@@ -56,7 +56,7 @@ structure Saturated (S : Set (Term Var)) : Prop where
 -/
 @[simp, scoped grind =]
 def semanticMap : Ty Base → Set (Term Var)
-  | .base _ => { t | SN t ∧ LC t }
+  | .base _ => { t | SN FullBeta t ∧ LC t }
   | .arrow τ₁ τ₂ => { t | ∀ s, s ∈ semanticMap τ₁ → app t s ∈ semanticMap τ₂ }
 
 /-- The sets constructed by semanticMap are saturated -/
@@ -117,7 +117,7 @@ lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) :
 /-- Using soundness and the fact that the empty context
     is entailed by any environment, we can conclude that
     a well-typed term is strongly normalizing. -/
-theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by
+theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN FullBeta t := by
   apply (semanticMap_saturated τ).sn
   apply (soundness der [] (by grind) entails_context_empty)
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -24,59 +24,52 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 variable {Var : Type u} {t t' : Term Var}
 
-open FullBeta
+open FullBeta Relation
 
 attribute [grind =] Finset.union_singleton
 
-/-- A term is strongly normalizing if every reduction sequence terminates at some point.
-    This is ensured by the following type as inductive data must always be finite. -/
-inductive SN {α} : Term α → Prop
-| sn t : (∀ t', t ⭢βᶠ t' → SN t') → SN t
-
-attribute [scoped grind .] SN.sn
-
 /-- A single β-reduction step preserves strong normalization. -/
-lemma sn_step (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by
-  grind [cases SN]
+lemma sn_step (t_st_t' : t ⭢βᶠ t') (sn_t : SN FullBeta t) : SN FullBeta t' :=
+  sn_t.of_rel t_st_t'
 
 /-- Multiple β-reduction steps also preserve strong normalization. -/
-lemma sn_steps (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
-  induction t_st_t' with grind [sn_step]
+lemma sn_steps (t_st_t' : t ↠βᶠ t') (sn_t : SN FullBeta t) : SN FullBeta t' :=
+  sn_t.of_rel_reflTransGen t_st_t'
 
 /-- Free variables are strongly normalizing. -/
-lemma sn_fvar {x : Var} : SN (fvar x) := by
-  grind only [cases Xi, cases Beta, SN]
+lemma sn_fvar {x : Var} : SN FullBeta (fvar x) := by
+  rw [SN_iff_SN_of_rel]
+  grind only [cases Xi, cases Beta]
 
 /-- An application is strongly normalizing if the left and right terms are strongly normalizing,
     as well as all possible future top level abstraction application beta reductions -/
-lemma sn_app (t s : Term Var) (sn_t : SN t) (sn_s : SN s)
-    (hβ : ∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) : SN (t.app s) := by
+lemma sn_app (t s : Term Var) (sn_t : SN FullBeta t) (sn_s : SN FullBeta s)
+    (hβ : ∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN FullBeta (t' ^ s')) :
+    SN FullBeta (t.app s) := by
   induction sn_t generalizing s with
-  | sn t ht ih_t =>
+  | intro t ht ih_t =>
     induction sn_s with
-    | sn s hs ih_s =>
+    | intro s hs ih_s =>
       constructor
       intro u hstep
       cases hstep with
       | base h => cases h; grind
       | appL _ h_s_red => apply ih_s _ h_s_red
                           grind [Relation.ReflTransGen.head]
-      | appR _ h_t_red => apply ih_t _ h_t_red _ (SN.sn s hs)
+      | appR _ h_t_red => apply ih_t _ h_t_red _ (SN.intro hs)
                           grind [Relation.ReflTransGen.head]
 
 /-- The left side of a strongly normalizing application is strongly normalizing. -/
-lemma sn_app_left (M N : Term Var) (lc_N : Term.LC N) (sn_MN : SN (M.app N)) :
-    SN M := by
-  generalize Heq : M.app N = P
-  rw [Heq] at sn_MN
-  induction sn_MN generalizing M N with grind
+lemma sn_app_left (M N : Term Var) (lc_N : Term.LC N) (sn_MN : SN FullBeta (M.app N)) :
+    SN FullBeta M := by
+  refine sn_MN.onFun_of_image (f := (·.app N)) |>.of_le fun _ _ => ?_
+  exact Xi.appR lc_N
 
 /-- The right side of a strongly normalizing application is strongly normalizing. -/
-lemma sn_app_right (M N : Term Var) (lc_N : Term.LC M) (sn_MN : SN (M.app N)) :
-    SN N := by
-  generalize Heq : M.app N = P
-  rw [Heq] at sn_MN
-  induction sn_MN generalizing M N with grind
+lemma sn_app_right (M N : Term Var) (lc_M : Term.LC M) (sn_MN : SN FullBeta (M.app N)) :
+    SN FullBeta N := by
+  refine sn_MN.onFun_of_image (f := M.app) |>.of_le fun _ _ => ?_
+  exact Xi.appL lc_M
 
 /-- A neutral term is a term of the form v t₁ … t_n where
     v is a variable and t₁ … t_n are strongly normalizing terms. -/
@@ -87,7 +80,7 @@ inductive Neutral : Term Var → Prop
 /-- Just a free variable is neutral. -/
 | fvar : ∀ x, Neutral (fvar x)
 /-- Applying a strongly normalizing term to a neutral term yields a neutral term. -/
-| app : ∀ t1 t2, Neutral t1 → SN t2 → Neutral (app t1 t2)
+| app : ∀ t1 t2, Neutral t1 → SN FullBeta t2 → Neutral (app t1 t2)
 
 --attribute [scoped grind .] Neutral.bvar Neutral.fvar Neutral.app
 
@@ -100,17 +93,19 @@ lemma neutral_steps (Hneut : Neutral t) (Hsteps : t ↠βᶠ t') : Neutral t' :=
   induction Hsteps <;> grind [neutral_step]
 
 /-- Neutral terms are strongly normalizing. -/
-lemma sn_neutral (Hneut : Neutral t) : SN t := by
+lemma sn_neutral (Hneut : Neutral t) : SN FullBeta t := by
   induction Hneut with
   | app => grind [→ neutral_steps, sn_app]
-  | _ => grind only [SN, cases Xi]
+  | _ =>
+    rw [SN_iff_SN_of_rel]
+    grind only [cases Xi]
 
 /-- A lambda abstraction is strongly normalizing if its body is strongly normalizing. -/
-lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN (M ^ N)) (lc_N : LC N) :
-    SN (abs M) := by
+lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN FullBeta (M ^ N))
+    (lc_N : LC N) : SN FullBeta (abs M) := by
   generalize h : (M ^ N) = M_open at sn_MN
   induction sn_MN generalizing M N with
-  | sn =>
+  | intro =>
     constructor
     intro _ h_step
     cases h_step with
@@ -123,8 +118,9 @@ lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN (M ^
       1. N is locally closed,
       1. M ^ N P₁ … Pₙ is locally closed -/
 lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
-    (sn_N : SN N) (sn_MNPs : SN (multiApp (M ^ N) Ps))
-    (lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) : SN (multiApp (M.abs.app N) Ps) := by
+    (sn_N : SN FullBeta N) (sn_MNPs : SN FullBeta (multiApp (M ^ N) Ps))
+    (lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) :
+    SN FullBeta (multiApp (M.abs.app N) Ps) := by
   induction Ps with
   | nil =>
     apply sn_app
