Finish (well, almost) the proof of uniform normalization

theories/Conservation.v

@@ -237,28 +237,28 @@ Proof.
   - (* We have reached a point where the terms were joined back, thus all the
        missing redexes were contracted. Since neither path requires any work,
        we conclude that c = d and we are done by our inductive hypothesis. *)
-    assert (c = e) by admit; subst.
-    assert (d = e) by admit; subst.
+    assert (c = e) by eauto with arith cps; subst.
+    assert (d = e) by eauto with arith cps; subst.
     assumption.
   (* Case: r is a strict subset of p. *)
   - (* Here c can move to d. So we performed all the missing redexes and a few
        more! As our hypothesis says that c is SN, we can finish already by doing
        the additional redexes alone. *)
-    assert (e = d) by admit; subst.
+    assert (d = e) by eauto with arith cps; subst.
     apply H; unfold transp.
     eauto with cps.
   (* Case: p is a strict subset of r. *)
   - (* Here we are performing some, but not all, of the missing redexes, and
        nothing more. We proceed by our second inductive hypothesis, as we will
        now need less work to develop all the missing redexes. We have enough
        information to state that p is a subset of r. *)
-    assert (e = c) by admit; subst.
+    assert (c = e) by eauto with arith cps; subst.
     apply H0 with (redexes_weight [] rp) rp; auto.
     (* Naturally, any partial development reduces the maximum number of steps
        required to develop the term. *)
     apply development_reduces_weight with p [].
     + (* Clearly, from H6 and H11. *)
-      admit.
+      eapply subset_residuals_zero_marks; eauto with arith.
     + eauto with cps.
     + assumption.
     + constructor.

theories/Residuals.v

@@ -72,6 +72,25 @@ Proof.
   rewrite IHe1, IHe2; auto.
 Qed.
 
+Lemma mark_is_injective:
+  forall a b,
+  mark a = mark b ->
+  a = b.
+Proof.
+  induction a; intros.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; now inversion H.
+  - destruct b; simpl in H; inversion H.
+    f_equal; auto.
+Qed.
+
+Global Hint Resolve mark_is_injective: cps.
+
 Fixpoint redexes_lift i k e: redexes :=
   match e with
   | redexes_jump r f xs =>
@@ -349,6 +368,8 @@ Proof.
       eapply IHa1; eauto.
 Qed.
 
+Global Hint Resolve residuals_is_unique: cps.
+
 Lemma compatible_residuals:
   forall g a b c,
   residuals g a b c ->
@@ -1014,6 +1035,28 @@ Proof.
       apply IHresiduals2.
 Qed.
 
+Lemma residuals_zero_marks:
+  forall g r s t,
+  residuals g r s t ->
+  redexes_count s = 0 ->
+  r = t.
+Proof.
+  induction 1; simpl; intros.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - discriminate.
+  - f_equal.
+    + now rewrite IHresiduals1 by lia.
+    + now rewrite IHresiduals2 by lia.
+Qed.
+
+Global Hint Resolve residuals_zero_marks: cps.
+
 (* -------------------------------------------------------------------------- *)
 
 Inductive redexes_context: Set :=
@@ -1116,6 +1159,30 @@ Inductive subset: relation redexes :=
 
 Global Hint Constructors subset: cps.
 
+Lemma subset_residuals_zero_marks:
+  forall g r s t,
+  residuals g r s t ->
+  redexes_count t = 0 ->
+  subset r s.
+Proof.
+  induction 1; simpl; intros.
+  - constructor.
+  - constructor.
+  - constructor.
+  - constructor.
+  - constructor.
+  - constructor.
+  - destruct r.
+    + discriminate.
+    + constructor.
+  - constructor.
+  - constructor.
+    + apply IHresiduals1.
+      lia.
+    + apply IHresiduals2.
+      lia.
+Qed.
+
 Lemma partial_development:
   forall t s,
   subset t s ->