From e842635aa9910d35b66df971da2ff2822536e1ef Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Mon, 9 Dec 2024 16:37:37 +0100
Subject: [PATCH 1/8] WIP: alternative proof of strong normalization, following
 Lemma 3.2.1

---
 .../StrongNormalisation.v                     | 361 +++++++++++++++++-
 1 file changed, 348 insertions(+), 13 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index b4b3a97..4ce6185 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -1,4 +1,5 @@
 From FormArith.SimplyTypedLambdaCalculus Require Import Definitions.
+Import List.ListNotations.
 
 
 Inductive SN: term -> Prop :=
@@ -73,6 +74,353 @@ Proof.
   now inversion 1.
 Qed.
 
+Fixpoint atomic' (t: term):=
+  match t with 
+  | Var _ => True (* unsure if this case should be included or not? *)
+  | App l _ => atomic' l
+| _ => False
+  end.
+
+Definition atomic (t: term) := atomic' t /\ SN t.
+
+Lemma SN_subst (t: term) (σ: var -> term):
+  SN t -> forall (u: term), t = u.[σ] -> SN u.
+Proof.
+  induction 1 as [? _ IHt]; intros; subst.
+
+  apply Strong.
+  intros t ?.
+
+  apply IHt with t.[σ].
+  - now apply beta_subst.
+  - reflexivity.
+Qed.
+
+(*Lemma 3.2.1 (3) refers to terms of this specific shape*)
+Fixpoint nested_app t l :=
+  match l with 
+  | nil => t
+  | cons t' l' => App (nested_app t l') t'
+  end.
+
+Lemma atomic_step t s : atomic' t -> t ->β s -> atomic' s.
+Proof.
+  induction t in s |- *; cbn.
+  - inversion 2.
+  - intros Hat Hstep. inversion Hstep; subst.
+    + contradiction.
+    + cbn. apply IHt1; assumption.
+    + cbn. assumption.
+  - tauto.
+Qed.
+
+Lemma atomic_app_r t u : atomic t -> SN u -> atomic (App t u).
+Proof.
+  intros [Hat Hsnt] Hsnu.
+  split.
+  - tauto.
+  - induction Hsnt in Hat, u, Hsnu |-*.
+    induction Hsnu in H0 |- *.
+    constructor. intros t' Hstep.
+    inversion Hstep; subst.
+    + contradiction.
+    + apply H0.
+      * assumption.
+      * eapply atomic_step; eassumption.
+      * constructor. assumption.
+    + apply H2. 1: assumption. assumption.
+Qed.
+
+Lemma SN_ind_pair (P : term -> term -> Prop):
+  (forall t u, (forall t' u', ((t = t' /\ u ->β u') \/ (t ->β t' /\ u = u')) -> P t' u') -> P t u)
+    -> forall t u, SN t -> SN u -> P t u.
+Proof.
+  intros IH ? ? Hsnt.
+  revert u.
+
+  induction Hsnt as [? _ IHt].
+  intros ? Hsnt.
+
+  induction Hsnt as [? ? IHv].
+  apply IH.
+
+  intros ? ? [[? ?] | [? ?]]; subst.
+  - now apply IHv.
+  - apply IHt; [ assumption |].
+    now apply Strong.
+Qed.
+
+(*
+  Enumerate all the possible next steps of a term.
+  This is helpful (and probably only helpful) for the max_steps lemma.
+*)
+Fixpoint enumerate_steps (t : term) : list term :=
+  match t with 
+  | Var _ => []
+  | Lam s => List.map Lam (enumerate_steps s)
+  | App s t => List.map (fun s => App s t) (enumerate_steps s)
+                ++ List.map (fun t => App s t) (enumerate_steps t)
+                ++ match s with
+                   | Lam s' => [s'.[t/]]
+                   | __ => []
+                   end
+  end.
+
+(*
+  enumerate_steps is sound and complete:
+ *)
+Lemma enumerate_steps_spec t: forall t', List.In t' (enumerate_steps t) <-> t ->β t'.
+Proof.
+  induction t as [x | s IHs t IHt | s IHs].
+  - intros u; cbn. split.
+    + firstorder.
+    + inversion 1.
+  - intros u; cbn. split.
+    + intros Hin. apply List.in_app_or in Hin as [Hin | Hin]. 2: apply List.in_app_or in Hin as [Hin | Hin].
+      * rewrite List.in_map_iff in Hin. destruct Hin as  [s' [<- Hs']].
+        apply IHs in Hs'.
+        now constructor.
+      * rewrite List.in_map_iff in Hin. destruct Hin as [t' [<- Ht']].
+        apply IHt in Ht'.
+        now constructor.
+      * destruct s; try firstorder.
+        now constructor.
+    + intros Hstep. inversion Hstep; subst.
+      * apply List.in_or_app. right. apply List.in_or_app. right.
+        firstorder.
+      * apply List.in_or_app. left.
+        apply (List.in_map (fun s' => App s' t)).
+        now apply IHs.
+      * apply List.in_or_app. right. apply List.in_or_app. left.
+        apply (List.in_map (fun t' => App s t')).
+        now apply IHt.
+  - intros u; cbn. split.
+    + intros Hin. apply List.in_map_iff in Hin.
+      destruct Hin as [s' [<- Hs']].
+      apply IHs in Hs'.
+      now constructor.
+    + inversion 1; subst.
+      apply List.in_map. now apply IHs.
+Qed.
+
+(*
+  This version is slightly nicer to use in the following proof:
+*)
+Lemma enumerate_Forall_beta t : List.Forall (fun t' => t ->β t') (enumerate_steps t).
+Proof.
+  apply List.Forall_forall.
+  apply enumerate_steps_spec.
+Qed.
+
+(*
+  reduction_sequences are lists where any element beta-reduces to the next element.
+  This helps us reason about the number of reduction steps any term can take.
+ *)
+Fixpoint reduction_sequence (l : list term) : Prop :=
+  match l with 
+  | nil => True
+  | cons t nil => True
+  | cons s (cons t l' as ll) => s ->β t /\ reduction_sequence ll
+  end.
+
+Require Import Lia.
+
+(*
+  Any strongly normalizing term has a maximum number of steps it can reduce.
+  We state this by stating a maximal length for any reduction sequence.
+
+  Intuitively, this is by induction on SN, which gives us the induction hypothesis for each possible next step.
+   The correctness proof follows since for any reduction sequence starting in t and with first step t', the remaining sequence must be a reduction sequence for t', so the induction hypothesis applies.
+  In practice, it is much more difficult, since we need to determine the maximum of the (existentially quantified) numbers of steps for each next term.
+*)
+Lemma max_steps (t: term) : SN t -> exists n, forall l, reduction_sequence (t :: l) -> length l <= n.
+Proof.
+  (*The proof is by induction on SN, which is also why we can't (easily) state this as a function.*)
+  intros Hsn. induction Hsn as [t Hsn IH].
+  (*First, we apply the induction hypothesis to all terms in `enumerate_steps` (i.e. all the terms t can reduce to).*)
+  assert (List.Forall (fun t' => t ->β t' /\ exists n, forall l, reduction_sequence (t' :: l) -> length l <= n) (enumerate_steps t)) as H.
+  + pose proof (enumerate_Forall_beta t) as H.
+    induction H.
+    * constructor.
+    * constructor. 2: assumption.
+      firstorder.
+  + (*Unfortunately, the maximal lengths for all t' are currently hidden underneath existential quantifiers, and not easily accessible.
+      We begin by moving them into an existentially quantified list.*)
+    assert (exists l', length l' = length (enumerate_steps t) /\ List.Forall (fun (p : term * nat) => let (t', n) := p in forall l, reduction_sequence (t' :: l) -> length l <= n) (List.combine (enumerate_steps t) l')) as [l' [Hlen Hl']].
+    * induction H as [|t' l Ht' HForall IHForall].
+      -- exists nil. firstorder.
+      -- destruct Ht' as [_ [n Hn]].
+         destruct IHForall as [l' Hl'].
+         exists (cons n l').
+         split.
+         ++ cbn. firstorder.
+         ++ constructor; firstorder.
+    * (* We now have l', the list of the maximal number of steps for each term in `enumerate_steps t`.*)
+      (* Clearly, we need at least one more step:*)
+      exists (S(List.list_max l')).
+      clear - l' Hlen Hl'.
+      (* For the correctness proof, we inspect the reduction sequence:*)
+      intros l Hred.
+      destruct l as [|t' l]. 1: cbn; lia. (*empty reduction sequences are trivial.*)
+      (* The first step in the reduction sequence must be a valid reduction step, so we must also have the next term in enumerate_steps.
+         Intuitively, we should thus be able to apply Hl'; but this requires some more difficulty:
+      *)
+      destruct Hred as [Hbeta Hred].
+      rewrite <- enumerate_steps_spec in Hbeta.
+      (* We first need to obtain the index of t', so that we can recover its associated number of steps.*)
+      apply List.In_nth with (d := Var 0) in Hbeta. destruct Hbeta  as (ind & Hind & Hbeta).
+      pose (List.nth ind l' 0) as n'.
+      (* n' is the max number of steps of t', but we need to recover this fact.
+         It is stored in Hl', so we need to instantiate the `Forall` with the corresponding index:
+      *)
+      pose (List.nth ind (List.combine (enumerate_steps t) l') (Var 0, 0)) as p.
+      assert (p = (t', n')) as Heq by (subst; now apply List.combine_nth).
+      assert (List.In p (List.combine (enumerate_steps t) l')) as Hp.
+      { apply List.nth_In.
+        pose proof (List.combine_length (enumerate_steps t) l').
+        lia.
+      }
+      rewrite List.Forall_forall in Hl'. apply Hl' in Hp.
+      rewrite Heq in Hp.
+      (* After all this, we have recovered what is essentially the induction hypothesis for t'.
+        Since (t :: t' :: l) is a valid reduction sequence for t, (t' :: l) must be a valid reduction sequence for t'; thus, the IH applies.
+       *)
+      specialize (Hp l).
+      assert (n' <= List.list_max l'). (*This is more or less the definition of list_max, but apparently, it is not in the library directly?*)
+      { assert (List.list_max l' <= List.list_max l') as H by constructor.
+        rewrite List.list_max_le in H.
+        rewrite List.Forall_forall in H.
+        apply H.
+        apply List.nth_In. congruence.
+      }
+      apply Hp in Hred.
+      cbn. lia.
+Qed.
+
+(* The standard strong induction on natural numbers *)
+Lemma nat_strong_ind:
+  forall P: nat -> Prop, (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n.
+Proof.
+  intros P Hind n.
+  enough (forall m, m <= n -> P m) as H.
+  - apply H. constructor.
+  - induction n.
+    + intros m. destruct m.
+      * intros _. apply Hind.
+        lia.
+      * lia.
+    + intros m Hm.
+      inversion Hm.
+      * subst. apply Hind.
+        intros m' Hm'.
+        apply IHn. lia.
+      * subst. now apply IHn.
+Qed.
+
+(* Lemma 3.2.1 statement (3) for the base case, where the entire term is of some atomic type.
+   Formalizing this proof is difficult:
+   While intuitively, any reduction step is either within any subterm (not changing the specified shape) or reduction of the leftmost application,
+   the main difficulty in Coq stems from the fact that we do not know the size of the term (i.e. the number of applications).
+
+   The current attempt uses the maximal numbers of steps (as determined by max_steps),
+   but is stuck at destructing the actual reduction step. Presumably, induction is needed, but I have not yet found a version that yields suitable induction hypotheses.
+*)
+Lemma base_case t u l : SN (nested_app t.[u/] l) -> SN u -> forall t', nested_app (App (Lam t) u) l ->β t' -> SN t'.
+Proof.
+  intros Hsn Hsnu.
+  (*determine the maximum number of steps for t*)
+  assert (exists nt, forall l, reduction_sequence (t :: l) -> length l <= nt) as [nt Hnt].
+  { admit. } (*chore: we don't have a lemma to do this yet, so induction on l?*)
+  (*determine the maximum number of steps for u*)
+  assert (exists nu, forall l, reduction_sequence (u :: l) -> length l <= nu) as [nu Hnu].
+  { apply max_steps. assumption. }
+  (*determine the maximum number of steps for all terms in l*)
+  assert (exists l', length l' = length l /\ List.Forall (fun (p : term * nat) => let (t, n) := p in forall l, reduction_sequence (t :: l) -> length l <= n) (List.combine l l')) as [l' Hl'].
+  { induction l.
+    - exists nil; firstorder.
+    - cbn in Hsn.
+      assert (SN a) as Ha.
+      { eapply SN_sub_term. 1: exact Hsn. constructor. }
+      assert (SN (nested_app t.[u/] l)) as Hsn'.
+      { eapply SN_sub_term. 1: exact Hsn. constructor. }
+      specialize (IHl Hsn').
+      destruct IHl as [l' Hl'].
+      apply max_steps in Ha.
+      destruct Ha as [n Hn].
+      exists (cons n l').
+      cbn. firstorder.
+  }
+  (*We wish to do induction on the sum of all these step numbers: This will allow us to use the induction hypothesis for any step in any of these terms.*)
+  remember (nt + nu + List.list_sum l') as n.
+  (*We do induction on n with everything else quantified.*)
+  induction n as [n IH] using nat_strong_ind in t, u, l, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn |- *.
+  intros t' Hstep.
+
+  (*below, my current best attempt at doing this proof, using induction on the derivation of the step. However, the induction hypothesis is not of a suitable shape.*)
+  (*some subgoals are marked as chore and admitted: they should be provable but just require a bit of work.*)
+  remember (nested_app (App (Lam t) u) l) as trm.
+  induction Hstep in t, u, l, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn, Heqtrm |- *.
+  - subst.
+    destruct l.
+    + cbn in Heqtrm. inversion Heqtrm; subst. exact Hsn.
+    + cbn in Heqtrm. inversion Heqtrm; subst.
+      destruct l; cbn in *; congruence.
+  - subst.
+    (* this _should_ be an application of IHHstep somehow, but the hypothesis is not of the right shape.
+       this may be doable by strengthening the statement to wrap it in another nested_app, then proving things about nested_app and append?
+    *)
+    admit.
+  - destruct l.
+    + cbn in Heqtrm. inversion Heqtrm; subst.
+      admit. (*chore*)
+    + cbn in Heqtrm. inversion Heqtrm; subst.
+      destruct l'. 1: cbn in *; firstorder; congruence.
+      change (SN (nested_app (App (Lam t) u) (t' :: l))).
+      eapply IH with (l := cons t1 l).
+      8: now constructor.
+      2-5: eassumption.
+      3: reflexivity.
+      (*chore : since t1 ->β t', there is an n' < n with the desired property; instantiate ?l' with n'::l'. the second subgoal will be annoying.*)
+      all: admit.
+  - destruct l; cbn in Heqtrm; congruence.
+Admitted.
+
+(*Lemma 3.2.1 of the lecture notes.*)
+Lemma reducible_is_SN_variant_1 (A : type):
+  (forall (t: term), reducible A t -> SN t) /\
+  (forall (t: term), atomic t -> reducible A t) /\
+  (forall (t u: term) l, reducible A (nested_app (t.[u .: ids]) l) -> SN u -> reducible A (nested_app (App (Lam t) u) l)).
+Proof.
+  induction A as [ | A1 IHA1 A2 IHA2 ].
+  - split. 2: split.
+    (*the first two statements are easy in the base case.*)
+    + intros t Ht. constructor. intros t'.
+      apply SN_inverted. assumption.
+    + intros t [_ Hsnt]. now destruct Hsnt.
+    + intros t u l H Hsnu. cbn in *. 
+      constructor.
+      (*the third statement is very difficult: see above.*)
+      now apply base_case.
+  - split. 2: split.
+    + cbn. intros t Hred.
+      apply SN_sub_term with (t := App t (Var 0)).
+      2: constructor.
+      apply IHA2, Hred.
+      apply IHA1. split. 
+      * cbn. tauto.
+      * constructor. intros ? H. inversion H.
+    + cbn. intros t Hat u Hred.
+      apply IHA2. split.
+      * apply Hat.
+      * apply IHA1 in Hred.
+        apply atomic_app_r; assumption.
+    + intros t u l Hred Hsnu u' Hred'.
+      change (reducible A2 (nested_app (App (Lam t) u) (cons u' l))).
+      apply IHA2.
+      * cbn. now apply Hred.
+      * assumption.
+Qed.
+
 Lemma reducible_is_SN (A : type):
   (forall (t: term), reducible A t -> SN t) /\
     (forall (t u: term), reducible A t -> t ~> u -> reducible A u) /\
@@ -120,19 +468,6 @@ Proof.
         now apply IHA2 with u.
 Qed.
 
-Lemma SN_subst (t: term) (σ: var -> term):
-  SN t -> forall (u: term), t = u.[σ] -> SN u.
-Proof.
-  induction 1 as [? _ IHt]; intros; subst.
-
-  apply Strong.
-  intros t ?.
-
-  apply IHt with t.[σ].
-  - now apply beta_subst.
-  - reflexivity.
-Qed.
-
 Lemma SN_ind_pair (P : term -> term -> Prop):
   (forall t u, (forall t' u', ((t = t' /\ u ~> u') \/ (t ~> t' /\ u = u')) -> P t' u') -> P t u)
     -> forall t u, SN t -> SN u -> P t u.

From 5a3ee778fe5cc9cad7f8b16b0fa5ea40a322cb2d Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 17:13:57 +0100
Subject: [PATCH 2/8] WIP: proper proof structure for base case of Lemma 3.2.1

---
 .../StrongNormalisation.v                     | 50 ++++++++++++-------
 1 file changed, 31 insertions(+), 19 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 4ce6185..97e7171 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -356,31 +356,43 @@ Proof.
   induction n as [n IH] using nat_strong_ind in t, u, l, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn |- *.
   intros t' Hstep.
 
-  (*below, my current best attempt at doing this proof, using induction on the derivation of the step. However, the induction hypothesis is not of a suitable shape.*)
-  (*some subgoals are marked as chore and admitted: they should be provable but just require a bit of work.*)
+  change l with (app nil l) in *.
+  change (SN (nested_app t' nil)).
+  cbn in Hstep.
+  remember nil as outer.
+  
   remember (nested_app (App (Lam t) u) l) as trm.
-  induction Hstep in t, u, l, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn, Heqtrm |- *.
+  induction Hstep in t, u, l, outer, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn, Heqtrm |- *.
   - subst.
     destruct l.
-    + cbn in Heqtrm. inversion Heqtrm; subst. exact Hsn.
-    + cbn in Heqtrm. inversion Heqtrm; subst.
+    + cbn in Heqtrm. inversion Heqtrm; subst. rewrite List.app_nil_r in Hsn. assumption.
++ cbn in Heqtrm. inversion Heqtrm; subst.
       destruct l; cbn in *; congruence.
   - subst.
-    (* this _should_ be an application of IHHstep somehow, but the hypothesis is not of the right shape.
-       this may be doable by strengthening the statement to wrap it in another nested_app, then proving things about nested_app and append?
-    *)
-    admit.
-  - destruct l.
-    + cbn in Heqtrm. inversion Heqtrm; subst.
-      admit. (*chore*)
-    + cbn in Heqtrm. inversion Heqtrm; subst.
-      destruct l'. 1: cbn in *; firstorder; congruence.
-      change (SN (nested_app (App (Lam t) u) (t' :: l))).
-      eapply IH with (l := cons t1 l).
-      8: now constructor.
-      2-5: eassumption.
+    destruct l; cbn in *.
+    + inversion Heqtrm; subst.
+      inversion Hstep; subst.
+      constructor. eapply IH; admit.
+    + assert (nested_app (App s' t0) outer = nested_app s' (outer ++ [t0])) as -> by admit.
+      inversion Heqtrm; subst.
+      eapply IHHstep.
+      2: exact Hsnu.
+      2: exact Hnt.
+      2: exact Hnu.
+      3, 4: reflexivity.
+      1, 2: assert ((outer ++ [t1]) ++ l = outer ++ (t1 :: l))%list as -> by admit.
+      all: assumption.
+  - destruct l; cbn in *.
+    + inversion Heqtrm; subst.
+      constructor. eapply IH; admit.
+    + inversion Heqtrm; subst.
+      change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
+      assert ((nested_app (nested_app (App (Lam t) u) (t' :: l)) outer) = nested_app (App (Lam t) u) (outer ++ (t' :: l))) as -> by admit.
+      eapply IH.
+      2: exact Hsn.
+      2: exact Hsnu.
+      2, 3: eassumption.
       3: reflexivity.
-      (*chore : since t1 ->β t', there is an n' < n with the desired property; instantiate ?l' with n'::l'. the second subgoal will be annoying.*)
       all: admit.
   - destruct l; cbn in Heqtrm; congruence.
 Admitted.

From e944a1b20e6b58748a37160d74359d5d5d5aff22 Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 17:24:50 +0100
Subject: [PATCH 3/8] WIP: resolve some simple subgoals

---
 .../StrongNormalisation.v                     | 24 +++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 97e7171..359576f 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -317,6 +317,13 @@ Proof.
       * subst. now apply IHn.
 Qed.
 
+Lemma nested_app_app t inner outer : (nested_app (nested_app t inner) outer) = nested_app t (outer ++ inner).
+Proof.
+  induction outer as [| t'  outer IH].
+  - reflexivity.
+  - cbn. rewrite IH. reflexivity.
+Qed.
+
 (* Lemma 3.2.1 statement (3) for the base case, where the entire term is of some atomic type.
    Formalizing this proof is difficult:
    While intuitively, any reduction step is either within any subterm (not changing the specified shape) or reduction of the leftmost application,
@@ -330,7 +337,15 @@ Proof.
   intros Hsn Hsnu.
   (*determine the maximum number of steps for t*)
   assert (exists nt, forall l, reduction_sequence (t :: l) -> length l <= nt) as [nt Hnt].
-  { admit. } (*chore: we don't have a lemma to do this yet, so induction on l?*)
+  { apply max_steps.
+    induction l as [| s l IH].
+    - eapply SN_subst. 2: reflexivity.
+      exact Hsn.
+    - apply IH.
+      eapply SN_sub_term.
+      + exact Hsn.
+      + constructor.
+  }
   (*determine the maximum number of steps for u*)
   assert (exists nu, forall l, reduction_sequence (u :: l) -> length l <= nu) as [nu Hnu].
   { apply max_steps. assumption. }
@@ -373,21 +388,22 @@ Proof.
     + inversion Heqtrm; subst.
       inversion Hstep; subst.
       constructor. eapply IH; admit.
-    + assert (nested_app (App s' t0) outer = nested_app s' (outer ++ [t0])) as -> by admit.
+    + change (App s' t0) with (nested_app s' [t0]).
+      rewrite nested_app_app.
       inversion Heqtrm; subst.
       eapply IHHstep.
       2: exact Hsnu.
       2: exact Hnt.
       2: exact Hnu.
       3, 4: reflexivity.
-      1, 2: assert ((outer ++ [t1]) ++ l = outer ++ (t1 :: l))%list as -> by admit.
+      1, 2: assert ((outer ++ [t1]) ++ l = outer ++ (t1 :: l))%list as -> by (rewrite <- List.app_assoc; reflexivity).
       all: assumption.
   - destruct l; cbn in *.
     + inversion Heqtrm; subst.
       constructor. eapply IH; admit.
     + inversion Heqtrm; subst.
       change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
-      assert ((nested_app (nested_app (App (Lam t) u) (t' :: l)) outer) = nested_app (App (Lam t) u) (outer ++ (t' :: l))) as -> by admit.
+      rewrite (nested_app_app).
       eapply IH.
       2: exact Hsn.
       2: exact Hsnu.

From 355bf7c16d7088794c9e31559c60438c37415f48 Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 18:38:23 +0100
Subject: [PATCH 4/8] WIP: more progress on base case of 3.2.1

---
 .../StrongNormalisation.v                     | 102 +++++++++++++++++-
 1 file changed, 99 insertions(+), 3 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 359576f..0b03da1 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -324,6 +324,78 @@ Proof.
   - cbn. rewrite IH. reflexivity.
 Qed.
 
+Lemma max_steps_decr t n: (forall l, reduction_sequence (t :: l) -> length l <= n) -> forall t', t ->β t' -> forall l, reduction_sequence (t' :: l) -> length l <= pred n.
+Proof.
+  intros Hmax t' Hstep.
+  destruct n.
+  - exfalso.
+    specialize (Hmax [t']%list).
+    cbn in Hmax. firstorder. lia.
+  - cbn.
+    intros l.
+    specialize (Hmax (t' :: l)%list).
+    cbn in Hmax.
+    intros Hmx'.
+    apply PeanoNat.Nat.succ_le_mono.
+    apply Hmax.
+    split; assumption.
+Qed.
+
+Lemma max_steps_nonzero t t' n: (t ->β t') -> (forall l, reduction_sequence (t :: l) -> length l <= n) -> n > 0.
+Proof.
+  intros Hstep Hlen.
+  specialize (Hlen [t']%list).
+  cbn in Hlen. firstorder.
+Qed.
+
+Lemma max_steps_list_decr t1 t2 l l' outer :
+  t1 ->β t2 -> 
+  length l' = length (outer ++ t1 :: l) -> 
+      List.Forall
+        (fun p : term * nat =>
+         let (t, n) := p in
+         forall l : list term,
+         match l with
+         | []%list => True
+         | (t0 :: _)%list => t ->β t0 /\ reduction_sequence l
+         end -> length l <= n) (List.combine (outer ++ t1 :: l) l') -> 
+  exists l'',
+  List.list_sum l'' < List.list_sum l'
+  /\ length l'' = length (outer ++ t1 :: l)
+  /\ List.Forall
+  (fun p : term * nat =>
+   let (t0, n) := p in
+   forall l0 : list term,
+   match l0 with
+   | []%list => True
+   | (t2 :: _)%list => t0 ->β t2 /\ reduction_sequence l0
+   end -> length l0 <= n) (List.combine (outer ++ t1 :: l) l'').
+Proof.
+  intros Hstep Hlen Hl'.
+  assert (List.In t1 (outer ++ t1 :: l)) as Hin.
+  - auto with datatypes.
+  - apply List.In_nth with (d := Var 0) in Hin as (ind & Hind & Hin).
+    rewrite (List.Forall_forall) in Hl'.
+    pose (List.nth ind l' 0) as n.
+    assert (List.In (t1, n) (List.combine (outer ++ t1 :: l) l')) as H.
+    { assert ((t1, n) = List.nth ind (List.combine (outer ++ t1 :: l) l') (Var 0, 0)) as Hnth.
+      - rewrite <- Hin.
+        rewrite List.combine_nth.
+        + repeat f_equal.
+          congruence.
+        + rewrite Hlen. congruence.
+      - rewrite Hnth. apply List.nth_In.
+        rewrite List.combine_length.
+        lia.
+    }
+    apply Hl' in H.
+    pose proof (max_steps_decr t1 n H t2 Hstep) as Hdecr.
+    pose proof (max_steps_nonzero t1 t2 n Hstep H) as Hnz.
+    
+    (*ideally, we would like to have some kind of list update function here with the desired properties. We don't.*)
+    (*induction on outer won't work: we don't get from List.nth ind (t1 :: l) _ = t1 that ind = 0. *)
+Admitted.
+
 (* Lemma 3.2.1 statement (3) for the base case, where the entire term is of some atomic type.
    Formalizing this proof is difficult:
    While intuitively, any reduction step is either within any subterm (not changing the specified shape) or reduction of the leftmost application,
@@ -387,7 +459,15 @@ Proof.
     destruct l; cbn in *.
     + inversion Heqtrm; subst.
       inversion Hstep; subst.
-      constructor. eapply IH; admit.
+      constructor. eapply IH.
+      3, 5: eassumption.
+      5: reflexivity.
+      4: rewrite List.app_nil_r in Hl'; exact Hl'.
+      3: apply (max_steps_decr t); eassumption.
+      1: apply (max_steps_nonzero t _ nt) in H0.
+      1: lia.
+      1: assumption.
+      admit.
     + change (App s' t0) with (nested_app s' [t0]).
       rewrite nested_app_app.
       inversion Heqtrm; subst.
@@ -400,16 +480,32 @@ Proof.
       all: assumption.
   - destruct l; cbn in *.
     + inversion Heqtrm; subst.
-      constructor. eapply IH; admit.
+      constructor. eapply IH.
+      7: reflexivity.
+      6: rewrite List.app_nil_r in Hl'; exact Hl'.
+      3: now apply (SN_inverted u).
+      3: eassumption.
+      3: apply (max_steps_decr u); eassumption.
+      1: apply (max_steps_nonzero u _ nu) in Hstep.
+      1: lia.
+      1: assumption.
+      admit.
     + inversion Heqtrm; subst.
       change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
       rewrite (nested_app_app).
+      destruct Hl' as [Hl'1 Hl'2].
+      pose proof (max_steps_list_decr t1 t' l l' outer Hstep Hl'1 Hl'2) as (l'' & Hdecr & Hl'').
       eapply IH.
       2: exact Hsn.
       2: exact Hsnu.
       2, 3: eassumption.
       3: reflexivity.
-      all: admit.
+      3: {
+        clear - Hstep.
+         induction outer; now constructor.
+      }
+      2: exact Hl''.
+      lia.
   - destruct l; cbn in Heqtrm; congruence.
 Admitted.
 

From 0026516d6f320c9c2e2823cb91c34a6dbd53eea1 Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 18:54:08 +0100
Subject: [PATCH 5/8] WIP: resolve one more admitted goal

---
 .../SimplyTypedLambdaCalculus/StrongNormalisation.v   | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 0b03da1..9f09765 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -467,7 +467,14 @@ Proof.
       1: apply (max_steps_nonzero t _ nt) in H0.
       1: lia.
       1: assumption.
-      admit.
+      clear - Hsn H0.
+      eapply SN_inverted. 1: exact Hsn.
+      induction outer as [| a outer IHouter].
+      * cbn. now apply beta_subst.
+      * cbn. constructor. 
+        apply IHouter.
+        eapply SN_sub_term. 1: exact Hsn.
+        cbn. constructor.
     + change (App s' t0) with (nested_app s' [t0]).
       rewrite nested_app_app.
       inversion Heqtrm; subst.
@@ -489,7 +496,7 @@ Proof.
       1: apply (max_steps_nonzero u _ nu) in Hstep.
       1: lia.
       1: assumption.
-      admit.
+      admit. (* requires (u ->β u') -> (t.[u/] ->β* t.[u'/]), which we have not yet shown *)
     + inversion Heqtrm; subst.
       change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
       rewrite (nested_app_app).

From c6a0460c3aa6fe1182f8c512fe8b807251ea03b8 Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 19:17:34 +0100
Subject: [PATCH 6/8] WIP: resolve more admitted cases

---
 .../StrongNormalisation.v                     | 70 +++++++++++++------
 1 file changed, 49 insertions(+), 21 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 9f09765..202972e 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -1,4 +1,4 @@
-From FormArith.SimplyTypedLambdaCalculus Require Import Definitions.
+From FormArith.SimplyTypedLambdaCalculus Require Import Definitions ChurchRosser.
 Import List.ListNotations.
 
 
@@ -103,7 +103,7 @@ Fixpoint nested_app t l :=
   | cons t' l' => App (nested_app t l') t'
   end.
 
-Lemma atomic_step t s : atomic' t -> t ->β s -> atomic' s.
+Lemma atomic_step t s : atomic' t -> t ~> s -> atomic' s.
 Proof.
   induction t in s |- *; cbn.
   - inversion 2.
@@ -131,8 +131,8 @@ Proof.
     + apply H2. 1: assumption. assumption.
 Qed.
 
-Lemma SN_ind_pair (P : term -> term -> Prop):
-  (forall t u, (forall t' u', ((t = t' /\ u ->β u') \/ (t ->β t' /\ u = u')) -> P t' u') -> P t u)
+Lemma SNaa_ind_pair (P : term -> term -> Prop):
+  (forall t u, (forall t' u', ((t = t' /\ u ~> u') \/ (t ~> t' /\ u = u')) -> P t' u') -> P t u)
     -> forall t u, SN t -> SN u -> P t u.
 Proof.
   intros IH ? ? Hsnt.
@@ -169,7 +169,7 @@ Fixpoint enumerate_steps (t : term) : list term :=
 (*
   enumerate_steps is sound and complete:
  *)
-Lemma enumerate_steps_spec t: forall t', List.In t' (enumerate_steps t) <-> t ->β t'.
+Lemma enumerate_steps_spec t: forall t', List.In t' (enumerate_steps t) <-> t ~> t'.
 Proof.
   induction t as [x | s IHs t IHt | s IHs].
   - intros u; cbn. split.
@@ -206,7 +206,7 @@ Qed.
 (*
   This version is slightly nicer to use in the following proof:
 *)
-Lemma enumerate_Forall_beta t : List.Forall (fun t' => t ->β t') (enumerate_steps t).
+Lemma enumerate_Forall_beta t : List.Forall (fun t' => t ~> t') (enumerate_steps t).
 Proof.
   apply List.Forall_forall.
   apply enumerate_steps_spec.
@@ -220,7 +220,7 @@ Fixpoint reduction_sequence (l : list term) : Prop :=
   match l with 
   | nil => True
   | cons t nil => True
-  | cons s (cons t l' as ll) => s ->β t /\ reduction_sequence ll
+  | cons s (cons t l' as ll) => s ~> t /\ reduction_sequence ll
   end.
 
 Require Import Lia.
@@ -238,7 +238,7 @@ Proof.
   (*The proof is by induction on SN, which is also why we can't (easily) state this as a function.*)
   intros Hsn. induction Hsn as [t Hsn IH].
   (*First, we apply the induction hypothesis to all terms in `enumerate_steps` (i.e. all the terms t can reduce to).*)
-  assert (List.Forall (fun t' => t ->β t' /\ exists n, forall l, reduction_sequence (t' :: l) -> length l <= n) (enumerate_steps t)) as H.
+  assert (List.Forall (fun t' => t ~> t' /\ exists n, forall l, reduction_sequence (t' :: l) -> length l <= n) (enumerate_steps t)) as H.
   + pose proof (enumerate_Forall_beta t) as H.
     induction H.
     * constructor.
@@ -246,7 +246,7 @@ Proof.
       firstorder.
   + (*Unfortunately, the maximal lengths for all t' are currently hidden underneath existential quantifiers, and not easily accessible.
       We begin by moving them into an existentially quantified list.*)
-    assert (exists l', length l' = length (enumerate_steps t) /\ List.Forall (fun (p : term * nat) => let (t', n) := p in forall l, reduction_sequence (t' :: l) -> length l <= n) (List.combine (enumerate_steps t) l')) as [l' [Hlen Hl']].
+    assert (exists l', length l' = length (enumerate_steps t) /\ List.Forall (fun (p : prod term nat) => let (t', n) := p in forall l, reduction_sequence (t' :: l) -> length l <= n) (List.combine (enumerate_steps t) l')) as [l' [Hlen Hl']].
     * induction H as [|t' l Ht' HForall IHForall].
       -- exists nil. firstorder.
       -- destruct Ht' as [_ [n Hn]].
@@ -317,6 +317,27 @@ Proof.
       * subst. now apply IHn.
 Qed.
 
+Lemma subst_steps t u u': u ~> u' -> t.[u/] ~>* t.[u'/].
+Proof.
+  intros Hstep.
+  apply par_red_to_beta_star.
+  apply par_red_subst_par_red.
+  2: apply par_red_refl.
+  intros [| v].
+  - asimpl. now apply beta_to_par_red.
+  - asimpl. apply par_red_refl.
+Qed.
+
+Lemma SN_inverted_star t t': SN t -> t ~>* t' -> SN t'.
+Proof.
+  intros Hsn Hsteps.
+  induction Hsteps.
+  - eapply SN_inverted; eassumption.
+  - assumption.
+  - firstorder.
+Qed.
+  
+
 Lemma nested_app_app t inner outer : (nested_app (nested_app t inner) outer) = nested_app t (outer ++ inner).
 Proof.
   induction outer as [| t'  outer IH].
@@ -324,7 +345,7 @@ Proof.
   - cbn. rewrite IH. reflexivity.
 Qed.
 
-Lemma max_steps_decr t n: (forall l, reduction_sequence (t :: l) -> length l <= n) -> forall t', t ->β t' -> forall l, reduction_sequence (t' :: l) -> length l <= pred n.
+Lemma max_steps_decr t n: (forall l, reduction_sequence (t :: l) -> length l <= n) -> forall t', t ~> t' -> forall l, reduction_sequence (t' :: l) -> length l <= pred n.
 Proof.
   intros Hmax t' Hstep.
   destruct n.
@@ -341,7 +362,7 @@ Proof.
     split; assumption.
 Qed.
 
-Lemma max_steps_nonzero t t' n: (t ->β t') -> (forall l, reduction_sequence (t :: l) -> length l <= n) -> n > 0.
+Lemma max_steps_nonzero t t' n: (t ~> t') -> (forall l, reduction_sequence (t :: l) -> length l <= n) -> n > 0.
 Proof.
   intros Hstep Hlen.
   specialize (Hlen [t']%list).
@@ -349,26 +370,26 @@ Proof.
 Qed.
 
 Lemma max_steps_list_decr t1 t2 l l' outer :
-  t1 ->β t2 -> 
+  t1 ~> t2 -> 
   length l' = length (outer ++ t1 :: l) -> 
       List.Forall
-        (fun p : term * nat =>
+        (fun p : prod term nat =>
          let (t, n) := p in
          forall l : list term,
          match l with
          | []%list => True
-         | (t0 :: _)%list => t ->β t0 /\ reduction_sequence l
+         | (t0 :: _)%list => t ~> t0 /\ reduction_sequence l
          end -> length l <= n) (List.combine (outer ++ t1 :: l) l') -> 
   exists l'',
   List.list_sum l'' < List.list_sum l'
   /\ length l'' = length (outer ++ t1 :: l)
   /\ List.Forall
-  (fun p : term * nat =>
+  (fun p : prod term nat =>
    let (t0, n) := p in
    forall l0 : list term,
    match l0 with
    | []%list => True
-   | (t2 :: _)%list => t0 ->β t2 /\ reduction_sequence l0
+   | (t2 :: _)%list => t0 ~> t2 /\ reduction_sequence l0
    end -> length l0 <= n) (List.combine (outer ++ t1 :: l) l'').
 Proof.
   intros Hstep Hlen Hl'.
@@ -404,7 +425,7 @@ Admitted.
    The current attempt uses the maximal numbers of steps (as determined by max_steps),
    but is stuck at destructing the actual reduction step. Presumably, induction is needed, but I have not yet found a version that yields suitable induction hypotheses.
 *)
-Lemma base_case t u l : SN (nested_app t.[u/] l) -> SN u -> forall t', nested_app (App (Lam t) u) l ->β t' -> SN t'.
+Lemma base_case t u l : SN (nested_app t.[u/] l) -> SN u -> forall t', nested_app (App (Lam t) u) l ~> t' -> SN t'.
 Proof.
   intros Hsn Hsnu.
   (*determine the maximum number of steps for t*)
@@ -422,7 +443,7 @@ Proof.
   assert (exists nu, forall l, reduction_sequence (u :: l) -> length l <= nu) as [nu Hnu].
   { apply max_steps. assumption. }
   (*determine the maximum number of steps for all terms in l*)
-  assert (exists l', length l' = length l /\ List.Forall (fun (p : term * nat) => let (t, n) := p in forall l, reduction_sequence (t :: l) -> length l <= n) (List.combine l l')) as [l' Hl'].
+  assert (exists l', length l' = length l /\ List.Forall (fun (p : prod term nat) => let (t, n) := p in forall l, reduction_sequence (t :: l) -> length l <= n) (List.combine l l')) as [l' Hl'].
   { induction l.
     - exists nil; firstorder.
     - cbn in Hsn.
@@ -496,7 +517,14 @@ Proof.
       1: apply (max_steps_nonzero u _ nu) in Hstep.
       1: lia.
       1: assumption.
-      admit. (* requires (u ->β u') -> (t.[u/] ->β* t.[u'/]), which we have not yet shown *)
+      clear - Hsn Hsnu Hstep.
+      eapply SN_inverted_star. 1: exact Hsn.
+      induction outer as [| a outer IHouter].
+      * cbn. now apply subst_steps.
+      * cbn. apply beta_star_app. 2: apply beta_star_refl.
+        apply IHouter.
+        eapply SN_sub_term. 1: exact Hsn.
+        cbn. constructor.
     + inversion Heqtrm; subst.
       change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
       rewrite (nested_app_app).
@@ -514,7 +542,7 @@ Proof.
       2: exact Hl''.
       lia.
   - destruct l; cbn in Heqtrm; congruence.
-Admitted.
+Qed.
 
 (*Lemma 3.2.1 of the lecture notes.*)
 Lemma reducible_is_SN_variant_1 (A : type):
@@ -703,4 +731,4 @@ Proof.
   intros.
   apply reducible_var with Γ.
   now apply Typing_Var.
-Qed.
+Qed

From ee0c0cf7e1a5a9a0e663c614ff751b4867893e1a Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 21:03:29 +0100
Subject: [PATCH 7/8] Prove remaining case.

---
 .../StrongNormalisation.v                     | 144 +++++++++++++-----
 1 file changed, 108 insertions(+), 36 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 202972e..8747ce4 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -369,6 +369,38 @@ Proof.
   cbn in Hlen. firstorder.
 Qed.
 
+Fixpoint update_nth {A : Type} n (l : list A) (a : A) :=
+  match l with 
+  | nil => nil
+  | cons x l' => match n with 
+                 | 0 => cons a l'
+                 | S n' => cons x (update_nth n' l' a)
+                 end
+  end.
+
+Lemma update_decr ind n l : ind < length l -> n = List.nth ind l 0 -> n > 0 -> List.list_sum (update_nth ind l (pred n)) < List.list_sum l.
+Proof.
+  intros Hlen Hind Hgt0.
+  induction l as [| x l IH] in ind, Hlen, Hind, Hgt0 |- *.
+  - cbn in Hlen. lia.
+  - cbn in Hlen.
+    destruct ind as [| ind].
+    + cbn in *; subst.
+      lia.
+    + cbn in *. specialize (IH ind).
+      apply PeanoNat.lt_S_n in Hlen.
+      firstorder. unfold List.list_sum in H. lia.
+Qed.
+
+Lemma update_length {A : Type} (l: list A) n v : length (update_nth n l v) = length l.
+Proof.
+  induction l as [| x l IH] in n |- *.
+  - destruct n; reflexivity.
+  - destruct n.
+    + cbn. reflexivity.
+    + cbn. congruence.
+Qed.
+
 Lemma max_steps_list_decr t1 t2 l l' outer :
   t1 ~> t2 -> 
   length l' = length (outer ++ t1 :: l) -> 
@@ -382,7 +414,7 @@ Lemma max_steps_list_decr t1 t2 l l' outer :
          end -> length l <= n) (List.combine (outer ++ t1 :: l) l') -> 
   exists l'',
   List.list_sum l'' < List.list_sum l'
-  /\ length l'' = length (outer ++ t1 :: l)
+  /\ length l'' = length (outer ++ t2 :: l)
   /\ List.Forall
   (fun p : prod term nat =>
    let (t0, n) := p in
@@ -390,32 +422,72 @@ Lemma max_steps_list_decr t1 t2 l l' outer :
    match l0 with
    | []%list => True
    | (t2 :: _)%list => t0 ~> t2 /\ reduction_sequence l0
-   end -> length l0 <= n) (List.combine (outer ++ t1 :: l) l'').
+   end -> length l0 <= n) (List.combine (outer ++ t2 :: l) l'').
 Proof.
   intros Hstep Hlen Hl'.
-  assert (List.In t1 (outer ++ t1 :: l)) as Hin.
-  - auto with datatypes.
-  - apply List.In_nth with (d := Var 0) in Hin as (ind & Hind & Hin).
-    rewrite (List.Forall_forall) in Hl'.
-    pose (List.nth ind l' 0) as n.
-    assert (List.In (t1, n) (List.combine (outer ++ t1 :: l) l')) as H.
-    { assert ((t1, n) = List.nth ind (List.combine (outer ++ t1 :: l) l') (Var 0, 0)) as Hnth.
-      - rewrite <- Hin.
-        rewrite List.combine_nth.
-        + repeat f_equal.
-          congruence.
-        + rewrite Hlen. congruence.
-      - rewrite Hnth. apply List.nth_In.
-        rewrite List.combine_length.
-        lia.
-    }
-    apply Hl' in H.
-    pose proof (max_steps_decr t1 n H t2 Hstep) as Hdecr.
-    pose proof (max_steps_nonzero t1 t2 n Hstep H) as Hnz.
-    
-    (*ideally, we would like to have some kind of list update function here with the desired properties. We don't.*)
-    (*induction on outer won't work: we don't get from List.nth ind (t1 :: l) _ = t1 that ind = 0. *)
-Admitted.
+  pose (length outer) as ind.
+  assert (ind < length (outer ++ t1 :: l)) as Hind.
+  {
+    clear.
+    induction outer; cbn in *; lia.
+  }
+  assert (List.nth ind (outer ++ t1 :: l) (Var 0) = t1) as Hin.
+  {
+    clear.
+    induction outer; cbn in *.
+    - reflexivity.
+    - assumption.
+  }
+  rewrite (List.Forall_forall) in Hl'.
+  pose (List.nth ind l' 0) as n.
+  assert (List.In (t1, n) (List.combine (outer ++ t1 :: l) l')) as H.
+  { assert ((t1, n) = List.nth ind (List.combine (outer ++ t1 :: l) l') (Var 0, 0)) as Hnth.
+    - rewrite <- Hin.
+      rewrite List.combine_nth.
+      + repeat f_equal.
+        congruence.
+      + rewrite Hlen. congruence.
+    - rewrite Hnth. apply List.nth_In.
+      rewrite List.combine_length.
+      lia.
+  }
+  apply Hl' in H.
+  pose proof (max_steps_decr t1 n H t2 Hstep) as Hdecr.
+  pose proof (max_steps_nonzero t1 t2 n Hstep H) as Hnz.
+
+  exists (update_nth ind l' (pred n)).
+  split. 1: {
+    apply update_decr.
+    - lia.
+    - reflexivity.
+    - assumption.
+  }
+  split. 1: {
+    rewrite update_length.
+    rewrite Hlen.
+    clear.
+    induction outer; cbn.
+    - reflexivity.
+    - congruence.
+  }
+  rewrite <- List.Forall_forall in Hl'.
+  clear - Hdecr Hl' Hlen.
+  unfold ind in *.
+
+  induction outer in l', Hl', n, Hlen, Hdecr |- *.
+  - cbn in *. destruct l'.
+    + constructor.
+    + constructor.
+      * exact Hdecr.
+      * inversion Hl'; subst. assumption.
+  - destruct l'; cbn in *.
+    + congruence.
+    + inversion Hl'.
+      constructor.
+      * assumption.
+      * apply IHouter; try assumption.
+        now inversion Hlen.
+Qed.
 
 (* Lemma 3.2.1 statement (3) for the base case, where the entire term is of some atomic type.
    Formalizing this proof is difficult:
@@ -530,17 +602,17 @@ Proof.
       rewrite (nested_app_app).
       destruct Hl' as [Hl'1 Hl'2].
       pose proof (max_steps_list_decr t1 t' l l' outer Hstep Hl'1 Hl'2) as (l'' & Hdecr & Hl'').
+      constructor.
       eapply IH.
-      2: exact Hsn.
-      2: exact Hsnu.
-      2, 3: eassumption.
-      3: reflexivity.
-      3: {
-        clear - Hstep.
-         induction outer; now constructor.
-      }
-      2: exact Hl''.
-      lia.
+      3: exact Hsnu.
+      3: exact Hnt.
+      3: exact Hnu.
+      4: reflexivity.
+      3: exact Hl''.
+      1: lia.
+      eapply SN_inverted. 1: exact Hsn.
+      clear - Hstep.
+      induction outer; now constructor.
   - destruct l; cbn in Heqtrm; congruence.
 Qed.
 
@@ -731,4 +803,4 @@ Proof.
   intros.
   apply reducible_var with Γ.
   now apply Typing_Var.
-Qed
+Qed.

From 7ba5d9ce7f0c10a8dd853c2a9a291b3219956f6a Mon Sep 17 00:00:00 2001
From: Jonathan Baumann <jonathan.baumann@ens-paris-saclay.fr>
Date: Tue, 10 Dec 2024 21:25:18 +0100
Subject: [PATCH 8/8] reduce dependency on auto-generated names

---
 .../StrongNormalisation.v                     | 52 +++++++++----------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index 8747ce4..4b43610 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -105,11 +105,11 @@ Fixpoint nested_app t l :=
 
 Lemma atomic_step t s : atomic' t -> t ~> s -> atomic' s.
 Proof.
-  induction t in s |- *; cbn.
+  induction t as [|t1 IH1 t2 IH2|] in s |- *; cbn.
   - inversion 2.
   - intros Hat Hstep. inversion Hstep; subst.
     + contradiction.
-    + cbn. apply IHt1; assumption.
+    + cbn. apply IH1; assumption.
     + cbn. assumption.
   - tauto.
 Qed.
@@ -119,23 +119,23 @@ Proof.
   intros [Hat Hsnt] Hsnu.
   split.
   - tauto.
-  - induction Hsnt in Hat, u, Hsnu |-*.
-    induction Hsnu in H0 |- *.
+  - induction Hsnt as [t Hsnt IHsnt] in Hat, u, Hsnu |-*.
+    induction Hsnu as [u Hsnu IHsnu].
     constructor. intros t' Hstep.
     inversion Hstep; subst.
     + contradiction.
-    + apply H0.
+    + apply IHsnt.
       * assumption.
       * eapply atomic_step; eassumption.
       * constructor. assumption.
-    + apply H2. 1: assumption. assumption.
+    + now apply IHsnu.
 Qed.
 
-Lemma SNaa_ind_pair (P : term -> term -> Prop):
+Lemma SN_ind_pair (P : term -> term -> Prop):
   (forall t u, (forall t' u', ((t = t' /\ u ~> u') \/ (t ~> t' /\ u = u')) -> P t' u') -> P t u)
     -> forall t u, SN t -> SN u -> P t u.
 Proof.
-  intros IH ? ? Hsnt.
+  intros IH t u Hsnt.
   revert u.
 
   induction Hsnt as [? _ IHt].
@@ -304,7 +304,7 @@ Proof.
   intros P Hind n.
   enough (forall m, m <= n -> P m) as H.
   - apply H. constructor.
-  - induction n.
+  - induction n as [| n IHn].
     + intros m. destruct m.
       * intros _. apply Hind.
         lia.
@@ -389,7 +389,7 @@ Proof.
       lia.
     + cbn in *. specialize (IH ind).
       apply PeanoNat.lt_S_n in Hlen.
-      firstorder. unfold List.list_sum in H. lia.
+      firstorder. unfold List.list_sum in *. lia.
 Qed.
 
 Lemma update_length {A : Type} (l: list A) n v : length (update_nth n l v) = length l.
@@ -474,7 +474,7 @@ Proof.
   clear - Hdecr Hl' Hlen.
   unfold ind in *.
 
-  induction outer in l', Hl', n, Hlen, Hdecr |- *.
+  induction outer as [| x outer IHouter] in l', Hl', n, Hlen, Hdecr |- *.
   - cbn in *. destruct l'.
     + constructor.
     + constructor.
@@ -516,7 +516,7 @@ Proof.
   { apply max_steps. assumption. }
   (*determine the maximum number of steps for all terms in l*)
   assert (exists l', length l' = length l /\ List.Forall (fun (p : prod term nat) => let (t, n) := p in forall l, reduction_sequence (t :: l) -> length l <= n) (List.combine l l')) as [l' Hl'].
-  { induction l.
+  { induction l as [| a l IHl].
     - exists nil; firstorder.
     - cbn in Hsn.
       assert (SN a) as Ha.
@@ -531,7 +531,7 @@ Proof.
       cbn. firstorder.
   }
   (*We wish to do induction on the sum of all these step numbers: This will allow us to use the induction hypothesis for any step in any of these terms.*)
-  remember (nt + nu + List.list_sum l') as n.
+  remember (nt + nu + List.list_sum l') as n eqn:Heqn.
   (*We do induction on n with everything else quantified.*)
   induction n as [n IH] using nat_strong_ind in t, u, l, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn |- *.
   intros t' Hstep.
@@ -541,26 +541,26 @@ Proof.
   cbn in Hstep.
   remember nil as outer.
   
-  remember (nested_app (App (Lam t) u) l) as trm.
-  induction Hstep in t, u, l, outer, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn, Heqtrm |- *.
+  remember (nested_app (App (Lam t) u) l) as trm eqn:Heqtrm.
+  induction Hstep as [| ta tb tc Hstep IHstep | ta tb tc Hstep IHstep | ta tb Hstep IHstep] in t, u, l, outer, Hsn, Hsnu, nt, Hnt, nu, Hnu, l', Hl', Heqn, Heqtrm |- *.
   - subst.
-    destruct l.
+    destruct l as [| ? l].
     + cbn in Heqtrm. inversion Heqtrm; subst. rewrite List.app_nil_r in Hsn. assumption.
-+ cbn in Heqtrm. inversion Heqtrm; subst.
+    + cbn in Heqtrm. inversion Heqtrm; subst.
       destruct l; cbn in *; congruence.
   - subst.
-    destruct l; cbn in *.
+    destruct l as [| t1 l]; cbn in *.
     + inversion Heqtrm; subst.
-      inversion Hstep; subst.
+      inversion Hstep as [| | | H1 H2 Hstep' H3 H4]; subst.
       constructor. eapply IH.
       3, 5: eassumption.
       5: reflexivity.
       4: rewrite List.app_nil_r in Hl'; exact Hl'.
       3: apply (max_steps_decr t); eassumption.
-      1: apply (max_steps_nonzero t _ nt) in H0.
+      1: apply (max_steps_nonzero t _ nt) in Hstep'.
       1: lia.
       1: assumption.
-      clear - Hsn H0.
+      clear - Hsn Hstep'.
       eapply SN_inverted. 1: exact Hsn.
       induction outer as [| a outer IHouter].
       * cbn. now apply beta_subst.
@@ -568,17 +568,17 @@ Proof.
         apply IHouter.
         eapply SN_sub_term. 1: exact Hsn.
         cbn. constructor.
-    + change (App s' t0) with (nested_app s' [t0]).
+    + change (App tb tc) with (nested_app tb [tc]).
       rewrite nested_app_app.
       inversion Heqtrm; subst.
-      eapply IHHstep.
+      eapply IHstep.
       2: exact Hsnu.
       2: exact Hnt.
       2: exact Hnu.
       3, 4: reflexivity.
       1, 2: assert ((outer ++ [t1]) ++ l = outer ++ (t1 :: l))%list as -> by (rewrite <- List.app_assoc; reflexivity).
       all: assumption.
-  - destruct l; cbn in *.
+  - destruct l as [| t1 l]; cbn in *.
     + inversion Heqtrm; subst.
       constructor. eapply IH.
       7: reflexivity.
@@ -598,10 +598,10 @@ Proof.
         eapply SN_sub_term. 1: exact Hsn.
         cbn. constructor.
     + inversion Heqtrm; subst.
-      change (SN (nested_app (nested_app (App (Lam t) u) (t' :: l)) outer)).
+      change (SN (nested_app (nested_app (App (Lam t) u) (tc :: l)) outer)).
       rewrite (nested_app_app).
       destruct Hl' as [Hl'1 Hl'2].
-      pose proof (max_steps_list_decr t1 t' l l' outer Hstep Hl'1 Hl'2) as (l'' & Hdecr & Hl'').
+      pose proof (max_steps_list_decr t1 tc l l' outer Hstep Hl'1 Hl'2) as (l'' & Hdecr & Hl'').
       constructor.
       eapply IH.
       3: exact Hsnu.