Simple build and README.

4 files changed, 1214 insertions, 0 deletions

diff --git a/theories/Equivalence.v b/theories/Equivalence.v
new file mode 100644
index 0000000..0fff549
--- /dev/null
+++ b/theories/Equivalence.v
@@ -0,0 +1,121 @@
+Require Import L.
+Require Import Evaluation.
+Require Import UniformConfluence.
+
+(** * Equivalence 
+
+    Reduction equivalence captures the idea of two lambda terms
+    meaning the same thing. Clearly if term [a] reduces to term [b],
+    then they are equivalent. However, if term [a] and [b] both reduce
+    to term [c], then we would also want to consider [a] and [b] to be
+    semantically equivalent. *)
+
+Inductive reduction_equivalent : term -> term -> Prop :=
+| reduction_equivalence_refl s t : s = t -> reduction_equivalent s t
+| reduction_equivalence_one_step s t : one_step_reduces_to s t -> reduction_equivalent s t
+| reduction_equivalence_sym s t: reduction_equivalent s t -> reduction_equivalent t s
+| reduction_equivalence_trans s u t : reduction_equivalent s u -> reduction_equivalent u t ->
+                                      reduction_equivalent s t.
+
+(** * Church-Rosser Properties
+
+    The following properties useful for studying the reduction
+    equivalence defined above. They resemble the properties used to
+    study semantic equivalence in Church and Rosser's original
+    unsolvable problem in arithmetic. *)
+
+Lemma reduction_implies_equivalence :
+  forall (s t: term), reduces_to s t -> reduction_equivalent s t.
+Proof.
+  intros s t Hred. induction Hred.
+  - apply reduction_equivalence_refl. reflexivity.
+  - apply reduction_equivalence_trans with (u:=u).
+    apply reduction_equivalence_one_step. apply H. apply IHHred.
+Qed.
+
+Lemma reduction_equivalent_iff_common_reduction :
+  forall (s t: term), reduction_equivalent s t <->
+                        exists (u: term), reduces_to s u /\ reduces_to t u.
+Proof.
+  intros s t. split.
+  - intros Heq. induction Heq.
+    + exists s. split. apply reduces_to_refl. rewrite H. apply reduces_to_refl.
+    + exists t. split. apply reduces_to_incr with (u:=t). apply H.
+      apply reduces_to_refl. apply reduces_to_refl.
+    + inversion IHHeq. exists x. split. apply H. apply H.
+    + (* apply uniform confluence *)
+      inversion IHHeq1 as [x [Hsx Hux]].
+      inversion IHHeq2 as [y [Huy Hty]].
+      specialize reduction_is_confluent with (s:=u) (t1:=x) (t2:=y) as Hconf.
+      assert (exists (u: term), reduces_to x u /\ reduces_to y u) as Hconf'.
+      { apply Hconf. apply Hux. apply Huy. }
+      inversion Hconf' as [w Hw]. exists w. split.
+      * apply reduction_is_transitive with (s:=x). apply Hsx. apply Hw.
+      * apply reduction_is_transitive with (s:=y). apply Hty. apply Hw.
+  - intros Hred. inversion Hred as [u [Hsu Htu]].
+    apply reduction_equivalence_trans with (u:=u).
+    apply reduction_implies_equivalence. apply Hsu.
+    apply reduction_equivalence_sym. apply reduction_implies_equivalence. apply Htu.
+Qed.
+
+Lemma reduction_equivalence_is_applicative :
+  forall (s t s' t': term), reduction_equivalent s s' -> reduction_equivalent t t' ->
+                            reduction_equivalent (app s t) (app s' t').
+Proof.
+  intros s t s' t' Hss' Htt'.
+  apply reduction_equivalent_iff_common_reduction in Hss'. inversion Hss' as [u Hss'u].
+  apply reduction_equivalent_iff_common_reduction in Htt'. inversion Htt' as [v Hss'v].
+  apply reduction_equivalent_iff_common_reduction. exists (app u v). split.
+  Search "applicative". apply reduction_applicative. apply Hss'u. apply Hss'v.
+  apply reduction_applicative. apply Hss'u. apply Hss'v.
+Qed.
+
+Lemma not_application_means_equivalent_iff_reduces :
+  forall (s t: term), variable t \/ abstraction t ->
+                      (reduction_equivalent s t <-> reduces_to s t).
+Proof.
+  intros s t Htype. split.
+  - intros Hequiv.
+    apply reduction_equivalent_iff_common_reduction in Hequiv as Hcommon.
+    inversion Hcommon as [u Hu]. induction t.
+    + assert (u = var n) as Huvar.
+      { specialize var_reduces_to_var with (n:=n) (t:=u) as Hvarred.
+        apply Hvarred. apply Hu. }
+      rewrite Huvar in Hu. apply Hu.
+    + destruct Htype.
+      * inversion H as [n Hn]. discriminate Hn.
+      * inversion H as [v Hv]. discriminate Hv.
+    + inversion Hu as [Hredsu Hredtu]. apply abs_reduces_to_abs in Hredtu.
+      rewrite Hredtu in Hredsu. apply Hredsu.
+  - apply reduction_implies_equivalence.
+Qed.
+
+Lemma reduction_equivalent_abstractions :
+  forall (s t: term), evaluates_to s t <-> reduction_equivalent s t /\ abstraction t.
+Proof.
+  intros s t. split.
+  - intros Hred.
+    apply evaluation_iff_reduction_to_abstraction in Hred as [Hred Habs].
+    split. apply reduction_implies_equivalence. apply Hred. apply Habs.
+  - intros [Heq Habs]. apply reduction_equivalent_iff_common_reduction in Heq.
+    inversion Heq as [u [Hsu Htu]]. induction Htu.
+    + apply evaluation_iff_reduction_to_abstraction. split. apply Hsu. apply Habs.
+    + inversion Habs as [x Hx]. rewrite Hx in H. inversion H.
+Qed.
+
+Lemma equivalence_to_evaluation :
+  forall (s t u: term), reduction_equivalent s t ->
+                        (evaluates_to s u <-> evaluates_to t u).
+Proof.
+  assert (forall (s t u: term), reduction_equivalent s t ->
+                                evaluates_to s u -> evaluates_to t u) as Htgt.
+  { intros s t u Hequiv Hevalsu.
+    apply reduction_equivalent_abstractions in Hevalsu as [Hequivsu Habsu].
+    apply reduction_equivalent_abstractions. split.
+    - apply reduction_equivalence_trans with (u:=s).
+      apply reduction_equivalence_sym. apply Hequiv. apply Hequivsu.
+    - apply Habsu. }
+  intros s t u Hst. split.
+  - apply Htgt. apply Hst.
+  - apply Htgt. apply reduction_equivalence_sym. apply Hst.
+Qed.
diff --git a/theories/Evaluation.v b/theories/Evaluation.v
new file mode 100644
index 0000000..48b8fdc
--- /dev/null
+++ b/theories/Evaluation.v
@@ -0,0 +1,553 @@
+(* begin hide *)
+Require Import Arith.
+Require Import Nat.
+Require Import Coq.Program.Equality. (* dependent induction *)
+Require Import Lia.
+Require Import Bool.
+(* end hide *)
+Require Import L.
+
+(** Evaluation captures the idea of computation in lambda calculus.
+    When simplifying terms by hand, we look for applications of
+    abstractions to perform reductions. It's not obvious a-priori what
+    order these applications should be performed in, or whether the
+    results are always the same. *)
+
+(** The _evaluation_ relation is defined in terms of substitution. It
+    makes no obvious choices about the order of substitutions. *)
+
+Inductive evaluates_to: term -> term -> Prop :=
+| refl s t u: (s = lambda u) -> (t = lambda u) -> evaluates_to s t
+| eval s t u v w:
+  evaluates_to s (lambda u) -> evaluates_to t v ->
+  evaluates_to (subst u 0 v) w -> evaluates_to (app s t) w.
+
+Definition evaluates (s: term) : Prop :=
+  exists t, evaluates_to s t.
+
+(** * Evaluation Properties 
+
+    Evaluation is slightly tricky to analyze because it has
+    flexibility in the terms which are actually substituted. Proving
+    statements about evaluation usually involves analyzing the actual
+    reductions which can occur, and the details of this are deferred
+    until later.  Some simple statements about evaluation, particularly
+    in relation to closed terms and abstractions are easy to show from
+    the inductive definition. *)
+
+Lemma only_can_evaluate_to_abstr :
+  forall (s t: term), evaluates_to s t -> abstraction t.
+Proof.
+  intros s t Heval.
+  induction Heval.
+  - unfold abstraction. exists u. apply H0.
+  - apply IHHeval3.
+Qed.
+
+Lemma evaluation_preserves_closure :
+  forall (s t: term), closed s -> evaluates_to s t -> closed t.
+Proof.
+  intros s t Hclosed Heval. induction Heval.
+  + rewrite H0. rewrite <- H. apply Hclosed.
+  + inversion Hclosed as [Hsclosed Htclosed].
+    apply IHHeval3. apply subst_preserves_closed with (s := lambda u).
+    reflexivity.
+    apply IHHeval1. apply Hsclosed.
+    apply IHHeval2. apply Htclosed.
+Qed.
+
+Lemma if_app_evaluates_then_both_evaluate :
+  forall (s t: term), evaluates (app s t) -> evaluates s /\ evaluates t.
+Proof.
+  intros s t.
+  intros Heval. inversion Heval as [s' Heval']. inversion Heval'.
+  - discriminate H.
+  - unfold evaluates. split.
+    + exists (lambda u). apply H1.
+    + exists v. apply H2.
+Qed.
+
+Lemma evaluate_not_closed_wrt_app :
+  exists (s t: term), evaluates s /\ evaluates t /\ ~ (evaluates (app s t)).
+Proof.
+  exists (lambda (var 1)). exists (lambda (var 1)).
+  assert (evaluates (lambda (var 1))) as Hlv1eval.
+  { unfold evaluates. exists (lambda (var 1)).
+    apply refl with (u := var 1). reflexivity. reflexivity. }
+  split. apply Hlv1eval. split. apply Hlv1eval.
+  unfold "~". intros Happeval. inversion Happeval.
+  inversion H.
+  - discriminate H0.
+  - inversion H2. 
+    + injection H6 as Hu0def.
+      injection H7 as Hudef.
+      rewrite <- Hu0def in Hudef.
+      rewrite Hudef in H5. simpl in H5.
+      inversion H5. discriminate H6.
+Qed.
+
+Lemma evaluation_is_transitive :
+  forall (a b c: term),
+    evaluates_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  intros a b c Hab Hbc. dependent induction Hbc.
+  - rewrite H0. rewrite H in Hab. apply Hab.
+  - apply only_can_evaluate_to_abstr in Hab.
+    inversion Hab as [x Hx]. discriminate Hx.
+Qed.
+
+(** * Reduction
+    
+    To study the evaluation of lambda terms we need to understand the
+    behaviours of chains of valid substitutions. This is done with the
+    concept of a _reduction_. It turns out that an evaluation exists
+    exactly when there is a reduction to an abstraction. *)
+
+(** Larger reductions are built from _one-step reductions_ which are
+    simply substitutions.
+
+    A term _[n]-step reduces_ to another if a sequence of [n] one-step
+    reductions translate the initial term into the final one.
+
+    One term _reduces_ to another if the two terms are literally equal
+    or can be built from one-step reductions. *)
+
+Inductive one_step_reduces_to : term -> term -> Prop :=
+| one_step_sub s t : one_step_reduces_to (app (lambda s) (lambda t)) (subst s 0 (lambda t))
+| one_step_appl s s' t : one_step_reduces_to s s' -> one_step_reduces_to (app s t) (app s' t)
+| one_step_appr s t t' : one_step_reduces_to t t' -> one_step_reduces_to (app s t) (app s t').
+
+Inductive n_step_reduces_to : nat -> term -> term -> Prop :=
+| n_step_refl s : n_step_reduces_to 0 s s
+| n_step_incr n s u t : one_step_reduces_to s u -> n_step_reduces_to n u t ->
+                        n_step_reduces_to (S n) s t.
+
+Inductive reduces_to : term -> term -> Prop :=
+| reduces_to_refl s : reduces_to s s
+| reduces_to_incr s u t : one_step_reduces_to s u -> reduces_to u t ->
+                          reduces_to s t.
+
+(** There are a variety of properties which we can prove about
+    reductions alone. *)
+
+(** ** [n]-Step Reduction Properties *)
+
+Lemma n_step_transitivity :
+  forall (n m : nat) (x y z: term),
+    n_step_reduces_to n x y -> n_step_reduces_to m y z ->
+    n_step_reduces_to (n + m) x z.
+Proof.
+  intros n. induction n. 
+  - intros m x y z Hxy Hyz. simpl. inversion Hxy. apply Hyz.
+  - intros m x y z Hxy Hyz. inversion Hxy.
+    rewrite plus_Sn_m. apply n_step_incr with (u:=u).
+    apply H0. apply IHn with (y:=y). apply H1. apply Hyz.
+Qed.
+
+Lemma n_step_additive :
+  forall (n m: nat) (s u t: term),
+    n_step_reduces_to n s u -> n_step_reduces_to m u t ->
+    n_step_reduces_to (n + m) s t.
+Proof.
+  intros n m. induction n.
+  - intros s u t Hnsu Hmut.
+    Search "+". rewrite Nat.add_0_l. destruct m.
+    + inversion Hnsu. apply Hmut.
+    + inversion Hnsu. apply Hmut.
+  - intros s u t Hsnsu Hmut.
+    Search "+". rewrite plus_Sn_m.
+    inversion Hsnsu. apply n_step_incr with (u := u0).
+    apply H0. apply IHn with (u := u). apply H1. apply Hmut.
+Qed.
+
+(** ** Reduction Properties *)
+
+Lemma reduction_is_transitive :
+  forall (r s t : term), reduces_to r s -> reduces_to s t -> reduces_to r t.
+Proof.
+  intros r s t Hrs Hst.
+  dependent induction Hrs.
+  - apply Hst.
+  - apply reduces_to_incr with (s:=s) (u:=u) (t:=t).
+    apply H. apply IHHrs. apply Hst.
+Qed.
+
+Lemma reduction_left_applicative :
+  forall (s t t': term), reduces_to t t' -> reduces_to (app s t) (app s t').
+Proof.
+  intros s t t' Htt'. induction Htt'.
+  - apply reduces_to_refl.
+  - apply reduces_to_incr with (u := app s u).
+    apply one_step_appr. apply H. apply IHHtt'.
+Qed.
+
+Lemma reduction_right_applicative :
+  forall (s s' t: term), reduces_to s s' -> reduces_to (app s t) (app s' t).
+Proof.
+  intros s s' t Hss'. induction Hss'.
+  - apply reduces_to_refl.
+  - apply reduces_to_incr with (u := app u t).
+    apply one_step_appl. apply H. apply IHHss'.
+Qed.
+
+Lemma reduction_applicative :
+  forall (s s' t t': term), reduces_to s s' -> reduces_to t t' ->
+                            reduces_to (app s t) (app s' t').
+Proof.
+  intros s s' t t' Hss' Htt'.
+  apply reduction_is_transitive with (s := app s t').
+  apply reduction_left_applicative. apply Htt'.
+  apply reduction_right_applicative. apply Hss'.
+Qed.
+
+Lemma reduction_is_realized :
+  forall (s t: term), reduces_to s t <->
+                      exists (n : nat), n_step_reduces_to n s t.
+Proof.
+  intros s t. split.
+  - intros Hst. induction Hst.
+    + exists 0. apply n_step_refl.
+    + inversion IHHst as [k Hut]. exists (S k).
+      apply n_step_incr with (n := k) (s:=s) (u := u) (t := t).
+      apply H. apply Hut.
+  - assert (forall (n: nat), forall (x y: term),
+               n_step_reduces_to n x y -> reduces_to x y) as Hsteps.
+    { intros n. induction n.
+      - intros x y Hnxy. inversion Hnxy. apply reduces_to_refl.
+      - intros x y Hsnxy. inversion Hsnxy.
+        apply reduces_to_incr with (u := u).
+        apply H0. apply IHn in H1. apply H1. }
+    intros Hred. inversion Hred. apply Hsteps in H. apply H.
+Qed.
+
+(** ** Properties of Possible Terms in Reduction
+
+    Often it is useful to reason about the possible terms that can be
+    the inputs and outputs of reductions. Below are some useful lemmas
+    in that vein. *)
+
+Lemma must_one_step_reduce_from_application :
+  forall (s t: term), one_step_reduces_to s t ->
+                      exists (s1 s2: term), s = app s1 s2.
+Proof.
+  intros s t Hst. inversion Hst.
+  - exists (lambda s0). exists (lambda t0). reflexivity.
+  - exists s0. exists t0. reflexivity.
+  - exists s0. exists t0. reflexivity.
+Qed.
+
+Lemma var_n_step_reduces_to_var :
+  forall (n k: nat) (s: term), n_step_reduces_to n (var k) s ->
+                               s = var k /\ n = 0.
+Proof.
+  intros n k s Hred. inversion Hred.
+  - split. reflexivity. reflexivity.
+  - apply must_one_step_reduce_from_application in H.
+    inversion H. inversion H4. discriminate H5.
+Qed.
+
+Lemma var_reduces_to_var :
+  forall (n: nat) (t: term), reduces_to (var n) t -> t = var n.
+Proof.
+  intros n t Hred.
+  apply reduction_is_realized in Hred. inversion Hred as [k Hkred].
+  specialize var_n_step_reduces_to_var with (n := k) (k := n) (s:=t) as Hvar.
+  destruct Hvar. apply Hkred. apply H.
+Qed.
+
+Lemma abs_reduces_to_abs :
+  forall (u t: term), reduces_to (lambda u) t -> t = lambda u.
+Proof.
+  intros u t Hred. apply reduction_is_realized in Hred.
+  inversion Hred as [k Hk]. inversion Hk. reflexivity. inversion H.
+Qed.
+
+(** * Relationships between Evaluation and Reduction 
+
+    Below are a few useful relationships between evaluation and
+    reduction. There are also some rules for extending evaluations
+    with reductions. Using these rules we can show that evaluation is
+    the same as a reduction to an abstraction. *)
+
+Lemma one_step_reduction_extends_evaluation :
+  forall (a b c: term),
+    one_step_reduces_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  (* We want to use the one step reduction to extend the evaluation's
+     reach. We induct upon the one step reduction.
+
+     1. [base, substitution]. Here we have as evidence that
+        - a = app (lambda sa) (lambda ta)
+        - b = subst sa 0 (lambda ta)
+        and we want to show that
+        evaluates_to b c -> evaluates_to a c.
+        It's trivial to show that (evaluates_to a b), and the case
+        follows by the transitivity of evaluates_to.
+
+     2. [inductive, left-application]. Here we have as evidence:
+        - one_step_reduces_to ar ar'
+       - one_step_reduces_to (app al ar) (app al ar')
+        and the inductive hypothesis:
+        - forall t, one_step_reduces_to ar ar' ->
+                 evaluates_to ar' t -> evaluates_to ar t.
+        We want to show that
+        forall t, evaluates_to (app al ar') t ->
+               evaluates_to (app al ar) t.
+        In the evidence for evaluates_to (app al ar') t, we know that
+        there is some v used as input to the substitution for which
+        evaluates_to ar' v. By the inductive hypothesis, we then have
+        that evaluates_to ar v. That is enough to build the evidence
+        for evaluates_to (app al ar) t.
+
+     3. [inductive, right-application]. This is the same as the second
+     case, except instead of pulling-back the evidence for the
+     (evaluates_to t v) term, we pull back the evidence for the
+     (evaluates_to s (lambda u)) using the inductive hypothesis. *)
+  assert (forall (a b: term), one_step_reduces_to a b ->
+    forall (c: term), evaluates_to b c -> evaluates_to a c) as Htgt.
+  { intros a b Honestep. induction Honestep.
+    - intros c. intros Hbc. apply eval with (u := s) (v := lambda t) (w := c).
+      apply refl with (u := s). reflexivity. reflexivity.
+      apply refl with (u := t). reflexivity. reflexivity.
+      apply Hbc.
+    - intros c Hbc. inversion Hbc.
+      + discriminate H.
+      + apply IHHonestep in H1. apply eval with (u := u) (v := v).
+        apply H1. apply H2. apply H4.
+    - intros c Hbc. inversion Hbc.
+      + discriminate H.
+      + apply IHHonestep in H2. apply eval with (u := u) (v := v).
+        apply H1. apply H2. apply H4. }
+  intros a b c Hab. apply Htgt. apply Hab.
+Qed.
+
+Lemma reduction_extends_evaluation :
+  forall (a b c: term),
+    reduces_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  intros a b c Hab. induction Hab.
+  + intros Hbc. apply Hbc.
+  + induction Hab.
+    - intros Hs0c. apply one_step_reduction_extends_evaluation with (b:=s0).
+      apply H. apply Hs0c.
+    - intros Htc. apply IHHab in Htc.
+      apply one_step_reduction_extends_evaluation with (b:=s0).
+      apply H. apply Htc.
+Qed.
+
+Proposition evaluation_iff_reduction_to_abstraction :
+  forall (s t: term), evaluates_to s t <->
+                      reduces_to s t /\ abstraction t.
+Proof.
+  split.
+  - intros Heval. split.
+    + induction Heval.
+      * rewrite H. rewrite H0. apply reduces_to_refl.
+      * assert (abstraction v) as Hvabstr.
+        { apply only_can_evaluate_to_abstr in Heval2. apply Heval2. }
+        assert (one_step_reduces_to (app (lambda u) v) (subst u 0 v)) as Huvsubst.
+        { inversion Hvabstr. specialize one_step_sub with (s := u) (t := x) as Hsub.
+          rewrite <- H in Hsub. apply Hsub. }
+        assert (reduces_to (app s t) (subst u 0 v)) as Hstred.
+        { apply reduction_is_transitive with (s := app (lambda u) v).
+          apply reduction_applicative. apply IHHeval1. apply IHHeval2.
+          apply reduces_to_incr with (u := subst u 0 v). apply Huvsubst.
+          apply reduces_to_refl. }
+        apply reduction_is_transitive with (s := subst u 0 v).
+        apply Hstred. apply IHHeval3.
+    + apply only_can_evaluate_to_abstr in Heval. apply Heval.
+  - intros [Hred Habstr].
+    apply reduction_extends_evaluation with (a:=s) (b:=t) (c:=t).
+    apply Hred. inversion Habstr as [u Hu]. apply refl with (u:=u).
+    apply Hu. apply Hu.
+Qed.
+
+(* lia: "linear integer arithmetic" (rocq manual 2025)
+   lia is used for deciding simple inequalities in integer arithmetic.
+
+   ltac: "L_{tac}" or "Tactic Language" (rocq manual 2025)
+   ltac is used for building tactics to streamline proofs.
+   it is deprecated for ltac2, as ltac grew organically and is
+   disorganized.
+
+   helpful examples for using ltac are in the reference manual and in
+   "Logical Foundations: More Automation" *)
+
+(** * Tactics 
+
+    In most computations, we want to apply the top most substitution
+    to prove that a reduction holds. Writing all the correct terms is
+    a nuisance. We can use tactics to automate this process. *)
+
+(** First we apply the [n]-step patterns, and then use one step
+    reduction rules later. *)
+
+Ltac find_n_step_incr :=
+  match goal with
+  | |- n_step_reduces_to _ (app (lambda ?x) ?y) _ => apply n_step_incr with (u:=subst x 0 y)
+  | |- n_step_reduces_to _ (app ?x ?y) (app ?x ?z) => apply n_step_incr with (u:=app x z)
+  | |- n_step_reduces_to _ (app ?x ?z) (app ?y ?z) => apply n_step_incr with (u:=app y z)
+ end.
+
+Example find_n_step_sub :
+  n_step_reduces_to 1 (app (lambda (var 0)) (lambda (var 1))) (lambda (var 1)).
+Proof. find_n_step_incr. apply one_step_sub. simpl. apply n_step_refl. Qed.
+
+Example find_n_step_appl :
+  n_step_reduces_to 1 (app (app (lambda (var 0)) (lambda (var 1))) (var 2))
+    (app (lambda (var 1)) (var 2)).
+Proof.
+  find_n_step_incr. apply one_step_appl. apply one_step_sub.
+  apply n_step_refl.
+Qed.
+
+Example find_n_step_appr :
+  n_step_reduces_to 1 (app (var 2) (app (lambda (var 0)) (lambda (var 1))))
+    (app (var 2) (lambda (var 1))).
+Proof.
+  find_n_step_incr. apply one_step_appr. apply one_step_sub.
+  apply n_step_refl.
+Qed.
+
+Inductive opt {T: Type} : Type :=
+| None
+| Some (x: T).
+
+Fixpoint left_reduce_opt (s: term) :=
+  match s with
+  | var n => None
+  | app (lambda s) t => Some (subst s 0 t)
+  | app s t => match (left_reduce_opt s) with
+               | Some s' => Some (app s' t)                 
+               | None => match (left_reduce_opt t) with
+                         | None => None
+                         | Some t' => Some (app s t')
+                         end                           
+               end
+  | lambda s => match (left_reduce_opt s) with
+                | Some s' => Some (lambda s')
+                | None => None
+                end
+  end.
+
+Definition left_reduce (s: term) :=
+  match (left_reduce_opt s) with
+  | Some s' => s'
+  | None => s
+  end.
+
+Ltac find_n_step_naive :=
+  match goal with
+  | |- n_step_reduces_to _ ?x _ => apply n_step_incr with (u:=left_reduce x);
+                                   unfold left_reduce; simpl
+  end.
+
+(** After the [n]-step rule is applied, we use similar rules to prove
+    the one step reduction goals that are produced from the previous
+    tactic. *)
+
+Ltac find_one_step :=
+  match goal with
+  | |- one_step_reduces_to (app (lambda ?s) (lambda ?t)) _ => apply one_step_sub; simpl
+  | |- one_step_reduces_to (app ?x ?y) (app ?x ?z) => apply one_step_appr; simpl
+  | |- one_step_reduces_to (app ?x ?z) (app ?y ?z) => apply one_step_appl; simpl
+  end.
+
+(** * Examples 
+
+    Using the reduction rules defined above we can demonstrate some
+    properties of special combinators. *)
+
+(** ** False Returns Second of Two *)
+
+Lemma Fst_evaluates_iff_both_evaluate :
+  forall (s t: term), evaluates (app (app c_F s) t) <-> evaluates s /\ evaluates t.
+Proof.
+  intros s t. split.
+  - intros HFeval. inversion HFeval. inversion H.
+    + discriminate H0.
+    + split.
+      * inversion H2.
+        { discriminate H6. }
+        { unfold evaluates. exists v0. apply H9. }
+      * unfold evaluates. exists v. apply H3.
+  - intros [Hseval Hteval]. unfold evaluates.
+    unfold evaluates in Hseval. inversion Hseval as [s' Hs'].
+    unfold evaluates in Hteval. inversion Hteval as [t' Ht'].
+    exists t'.
+    apply eval with (s := (app c_F s)) (u := var 0)
+                    (t := t) (v := t').
+    apply eval with (s := c_F) (u := lambda (var 0))
+                    (t := s) (v := s').
+    apply refl with (u := lambda (var 0)).
+    reflexivity. reflexivity. apply Hs'. simpl.
+    apply refl with (u := var 0). reflexivity. reflexivity.
+    apply Ht'. simpl.
+    apply only_can_evaluate_to_abstr in Ht'.
+    unfold abstraction in Ht'. inversion Ht' as [u' Hu'].
+    apply refl with (u := u'). apply Hu'. apply Hu'.      
+Qed.
+
+(** ** Looping Does not Halt *)
+
+Lemma omega_omega_does_not_evaluate :
+  ~ evaluates (app c_omega c_omega).
+Proof.
+  (* It must be the case that the final evaluation is produced by a
+     substitution rule. In that case, it must be that - u = (app (var
+     0) (var 0)), and - v = lambda (app (var 0) (var 0)) = c_omega.
+     However, we see that (subst u 0 v) = c_omega, producing the
+     desired contradiction.
+
+     This was difficult because the (app c_omega c_omega) needs to be
+     generalized: we need to retain the information that s = (app
+     c_omega c_omega) to reach the contradiction. *)
+  unfold "~". unfold evaluates. intros Heval.  inversion Heval as [x Hx].
+  dependent induction Hx.
+  - assert (u = app (var 0) (var 0)) as Hudef.
+    { inversion Hx1. injection H0 as Hu0equ. injection H as Hu0def.
+      rewrite Hu0equ. rewrite Hu0def. reflexivity. }
+    assert (v = c_omega) as Hvdef.
+    { inversion Hx2. unfold c_omega. injection H as Hu0def.
+      rewrite H0. rewrite Hu0def. reflexivity. }
+    apply IHHx3. rewrite Hudef. rewrite Hvdef. simpl. reflexivity.
+Qed.
+
+(** ** Recursion Operator *)
+
+Definition c_C :=
+  lambda (lambda (app (var 0) (lambda (app (app (app (var 2) (var 2)) (var 1)) (var 0))))).
+
+Definition rho (s: term) :=
+  lambda (app (app (app c_C c_C) s) (var 0)).
+
+Lemma rho_is_recursive :
+  forall (u v: term),
+    combinator u -> combinator v ->
+    n_step_reduces_to 3 (app (rho u) v) (app (app u (rho u)) v).
+Proof.
+  intros u v. unfold combinator. unfold closed. unfold abstraction.
+  intros [Hubound Huabstr] [Hvbound Hvabstr].
+  inversion Huabstr as [u' Hu']. inversion Hvabstr as [v' Hv'].
+  unfold rho. rewrite Hu'. rewrite Hv'.
+  find_n_step_naive. find_one_step.
+  find_n_step_naive. find_one_step. find_one_step. find_one_step.
+  find_n_step_naive. find_one_step. find_one_step.
+  assert (forall (s: term), subst u' 1 s = u') as Hu'subst.
+  { intros s. rewrite Hu' in Hubound. simpl in Hubound.
+    apply bounds_block_subst with (k:=1). apply Hubound. }
+  rewrite Hu'subst. apply n_step_refl.
+Qed.
+
+Lemma rho_is_combinator_if_s_closed :
+  forall (s: term), closed s -> combinator (rho s).
+Proof.
+  unfold closed. intros s Hclosed.
+  unfold combinator. split.
+  unfold closed. simpl.
+  { split. split. lia.
+    apply bound_relaxes with (m:=0) (n:=1). auto. apply Hclosed.
+    auto. }
+  unfold rho. unfold abstraction.
+  exists (app (app (app c_C c_C) s) (var 0)). reflexivity.
+Qed.
diff --git a/theories/L.v b/theories/L.v
new file mode 100644
index 0000000..e9b8417
--- /dev/null
+++ b/theories/L.v
@@ -0,0 +1,321 @@
+(* begin hide *)
+Require Import Arith.
+Require Import Nat.
+Require Import Coq.Program.Equality. (* dependent induction *)
+Require Import Lia.
+(* end hide *)
+
+(** The _weak call-by-value lambda calulus_ is a simple variant of
+    lambda calculus with simple abstractions and reduction rules. It
+    enjoys strong uniform-confluence properties and is easy to reason
+    with in machine proofs. *)
+
+(** Like all lambda calculi, the language is built from variables,
+    applications and abstractions. *)
+
+Inductive term :=
+| var (n: nat)
+| app (s: term) (t: term)
+| lambda (s: term).
+
+(** The substitution rule describes how the bound variable in an
+    abstraction is interpreted. The target variable increments up when
+    passing through an abstraction. *)
+
+Fixpoint subst (s: term) (n: nat) (t: term) :=
+  match s with
+  | var i => match (eqb n i) with true => t | false => var i end
+  | app u v => app (subst u n t) (subst v n t)
+  | lambda u => lambda (subst u (S n) t)
+  end.
+
+(** Terms are _closed_ if they are unaffected by substitutions.  A
+    term is _bound_ by some [n] if it is unaffected by substitutions
+    of variables of size [n] or greater. *)
+
+Fixpoint bound (s: term) (n: nat) : Prop :=
+  match s with
+  | var i => i < n
+  | app u v => (bound u n) /\ (bound v n)
+  | lambda u => bound u (S n)
+  end.
+
+Definition closed (s: term) := bound s 0.
+
+Definition variable (s: term) :=
+  exists (n: nat), s = var n.
+
+Definition application (s: term) :=
+  exists (u v: term), s = app u v.
+
+Definition abstraction (s: term) :=
+  exists (u: term), s = lambda u.
+
+(** A _combinator_ (called a _procedure_ by Forster and Smolka) is a
+    closed abstraction. It is a function whose contents are not
+    changed by higher level substitutions. *)
+
+Definition combinator (s: term) := closed s /\ abstraction s.
+
+(** * Boundedness Properties
+
+    Below are some useful properties of boundedness. *)
+
+Lemma bound_relaxes :
+  forall (s: term) (m n: nat),
+    m < n -> bound s m -> bound s n.
+Proof.
+  intros s.
+  induction s as [k | u IHu v IHv | u IH].
+  - simpl. intros m n. intros Hmn Hkm. 
+    apply Nat.lt_trans with (p := n) (n := k) (m := m).
+    apply Hkm. apply Hmn.
+  - intros m n. simpl. intros Hmn HumAvm.
+    destruct HumAvm as [Hum Hvm]. split.
+    apply IHu with (m := m) (n := n). apply Hmn. apply Hum.
+    apply IHv with (m := m) (n := n). apply Hmn. apply Hvm.
+  - intros m n Hmn. simpl. apply IH with (m := S m) (n := S n).
+    rewrite <- Nat.succ_lt_mono with (m := n) (n := m). apply Hmn.
+Qed.
+      
+Lemma bound_subst :
+  forall (s t: term) (i n: nat),
+    bound s n -> bound t n -> bound (subst s i t) n.
+Proof. intros s t. induction s as [j  | u IHu v IHv | u IHu].
+       - simpl. intros i n Hij Hbound. destruct (i =? j).
+         + apply Hbound. + simpl. apply Hij.
+       - intros i n. simpl. intros HunAvn Htn.
+         destruct HunAvn as [Hun Hvn]. split.
+         apply IHu. apply Hun. apply Htn.
+         apply IHv. apply Hvn. apply Htn.
+       - intros i n. simpl. intros HuSn Htn.
+         apply IHu with (i := S i) (n := S n).
+         apply HuSn. apply bound_relaxes with (m := n) (n := S n).
+         apply Nat.lt_succ_diag_r. apply Htn.
+Qed.
+
+Lemma subst_drops_bound :
+  forall (s t: term) (n: nat),
+    bound s (S n) -> bound t n -> bound (subst s n t) n.
+Proof.
+  intros s t.
+  induction s as [k | u IHu v IHv | u IHu].
+  - intros n Hsbound Htbound. simpl. simpl in Hsbound.
+    destruct (n =? k) eqn:E.
+    * apply Htbound.
+    * rewrite Nat.lt_succ_r in Hsbound.
+      rewrite Nat.eqb_neq in E.
+      apply Nat.le_lteq in Hsbound.
+      destruct Hsbound.
+      { simpl. apply H. }
+      { unfold "<>" in E. apply eq_sym in H.
+        apply E in H. exfalso. apply H. }
+  - intros n Hsbound Htbound. simpl. simpl in Hsbound.
+    destruct Hsbound as [Hubound Hvbound]. split.
+    + apply IHu. apply Hubound. apply Htbound.
+    + apply IHv. apply Hvbound. apply Htbound.
+  - intros n. intros Hsbound Htbound. simpl. simpl in Hsbound.
+    apply IHu with (n := S n). apply Hsbound.
+    apply bound_relaxes with (m := n) (n := S n).
+    apply Nat.lt_succ_diag_r. apply Htbound.
+Qed.
+
+Lemma app_closed_iff :
+  forall (s t: term), closed (app s t) <-> closed s /\ closed t.
+Proof. intros s t. unfold closed. simpl. split.
+       - intros H. apply H.
+       - intros H. apply H.
+Qed.
+
+Lemma subst_preserves_closed :
+  forall (u s t: term), s = lambda u -> closed s -> closed t ->
+                        closed (subst u 0 t).
+Proof.
+  induction u.
+  - intros s t Hsu Hsclosed Htclosed. simpl. destruct n.
+    + apply Htclosed.
+    + rewrite Hsu in Hsclosed. inversion Hsclosed.
+      apply Nat.leb_le in H0. simpl in H0. discriminate H0.
+  - intros s t Hsu Hsclosed Htclosed. simpl. apply app_closed_iff.
+    rewrite Hsu in Hsclosed. inversion Hsclosed as [Hu1 Hu2]. split.
+    + apply IHu1 with (s := lambda u1). reflexivity. apply Hu1. apply Htclosed.
+    + apply IHu2 with (s := lambda u2). reflexivity. apply Hu2. apply Htclosed.
+  - intros s t Hsu Hsclosed Htclosed. simpl. rewrite Hsu in Hsclosed.
+    unfold closed in Hsclosed. simpl in Hsclosed.
+    unfold closed. simpl.
+    apply subst_drops_bound. apply Hsclosed.
+    apply bound_relaxes with (m:=0) (n:=1).
+    apply Nat.lt_succ_diag_r. apply Htclosed.
+Qed.
+
+Lemma bounds_block_subst :
+  forall (s t: term) (k: nat), bound s k -> subst s k t  = s.
+Proof.
+  intros s. induction s.
+  - intros t k. simpl. intros Hbound. destruct (k =? n) eqn:E.    
+    + apply Nat.lt_neq in Hbound.
+      apply Nat.eqb_eq in E. apply Nat.eq_sym in E.
+      apply Hbound in E. exfalso. apply E.
+    + reflexivity.
+  - intros t k Hbound. inversion Hbound as [Hs1bound Hs2bound]. simpl.
+    rewrite IHs1. rewrite IHs2. reflexivity. apply Hs2bound. apply Hs1bound.
+  - intros t k Hbound. simpl in Hbound. simpl.
+    rewrite IHs. reflexivity. apply Hbound.
+Qed.
+
+
+(** * Simple Combinators 
+
+    Below are some examples of simple combinators written in the weak
+    call-by-value language. 
+
+    - [I]: identity
+    - [T]: true branch (returns first of two inputs)
+    - [F]: false branch (returns second of two inputs)
+    - [omega]: self-applicator
+    - [Omega]: infinite loop
+ *)
+
+Definition c_I := lambda (var 0).
+
+Definition c_T := lambda (lambda (var 1)).
+
+Definition c_F := lambda (lambda (var 0)).
+
+Definition c_omega := lambda (app (var 0) (var 0)).
+
+Definition c_Omega := lambda (app c_omega c_omega).
+
+(** * Reflections
+
+    It is helpful in several proofs to have reflections of equality,
+    boundedness, closure and combinators as boolean methods. They are
+    included below. *)
+
+(** ** Equality  *)
+
+Fixpoint term_eqb (x: term) (y: term) :=
+  match x with
+  | var i => match y with
+             | var j => (eqb i j)
+             | _ => false
+             end
+  | app ux vx => match y with
+                 | app uy vy => andb (term_eqb ux uy) (term_eqb vx vy)
+                 | _ => false
+                 end
+  | lambda ux => match y with
+                 | lambda uy => term_eqb ux uy
+                 | _ => false
+                 end
+  end.
+
+Ltac absurd := simpl; intros H; inversion H.
+
+Lemma term_eqb_compat :
+  forall (x y: term), term_eqb x y = true <-> x = y.
+Proof.
+  induction x.
+  - destruct y.
+    + simpl. rewrite PeanoNat.Nat.eqb_eq.
+      split.
+      * intros H. rewrite H. reflexivity.
+      *intros H. injection H as Heq. apply Heq.
+    + simpl. split. absurd. absurd.
+    + simpl. split. absurd. absurd.
+  - destruct y.
+    + simpl. split. absurd. absurd.
+    + simpl. split.
+      * intros Heq.
+        apply eq_sym in Heq. apply Bool.andb_true_eq in Heq.
+        destruct Heq as [H1 H2].
+        apply eq_sym in H1. apply IHx1 in H1. rewrite H1.
+        apply eq_sym in H2. apply IHx2 in H2. rewrite H2.
+        reflexivity.
+      * intros Heq. inversion Heq. rewrite <- H0. rewrite <- H1.
+        apply andb_true_intro. split.
+        { apply IHx1. reflexivity. } { apply IHx2. reflexivity. }
+    + simpl. split. absurd. absurd.
+  - destruct y.
+    + simpl. split. absurd. absurd.
+    + simpl. split. absurd. absurd.
+    + simpl. rewrite IHx. split.
+      * intros H. rewrite H. reflexivity.
+      * intros H. injection H as Heq. apply Heq.
+Qed.
+
+(** ** Boundedness *)
+
+Fixpoint is_bound (x: term) (n: nat) :=
+  match x with
+  | var i => ltb i n
+  | app u v => andb (is_bound u n) (is_bound v n)
+  | lambda u => is_bound u (S n)
+  end.
+
+Lemma is_bound_compat :
+  forall (x: term) (n: nat), is_bound x n = true <-> bound x n.
+Proof.
+  induction x as [k | u Hu v Hv | u Hu]. 
+  - intros n. simpl. apply PeanoNat.Nat.ltb_lt.
+  - intros n. simpl. rewrite <- Hu. rewrite <- Hv.
+    apply Bool.andb_true_iff.
+  - intros n. simpl. rewrite <- Hu. apply iff_refl.
+Qed.
+
+(** ** Closure *)
+
+Definition is_closed (x: term) := is_bound x 0.
+
+Corollary is_closed_compat :
+  forall (x: term), is_closed x = true <-> closed x.
+Proof.
+  unfold is_closed. unfold closed. intros x.
+  apply is_bound_compat.
+Qed.
+
+(** ** Abstraction *)
+
+Definition is_abstraction (x: term) : bool :=
+  match x with
+  | lambda u => true
+  | _ => false
+  end.
+
+Lemma is_abstraction_compat :
+  forall (x: term), is_abstraction x = true <-> abstraction x.
+Proof.
+  destruct x.
+  - simpl. split.
+    + intros H. inversion H.
+    + intros H. inversion H as [u Hu]. inversion Hu.
+  - simpl. split.
+    + intros H. inversion H.
+    + intros H. inversion H as [u Hu]. inversion Hu.
+  - simpl. split.
+    + intros _. exists x. reflexivity.
+    + reflexivity.
+Qed.
+
+(** ** Combinator *)
+
+Definition is_combinator (x: term) :=
+  andb (is_abstraction x) (is_closed x).
+
+Lemma is_combinator_compat :
+  forall (x: term), is_combinator x = true <-> combinator x.
+Proof.
+  intros x. unfold is_combinator. unfold combinator.
+  rewrite <- is_closed_compat. rewrite <- is_abstraction_compat.
+  rewrite Bool.andb_comm. apply Bool.andb_true_iff.
+Qed.
+
+(** ** Substitution *)
+
+Definition predicate (x: term) :=
+  match x with
+  | lambda u => u
+  | _ => x
+  end.
+
+Definition combine (f x: term) := subst (predicate f) 0 x.
diff --git a/theories/UniformConfluence.v b/theories/UniformConfluence.v
new file mode 100644
index 0000000..f176430
--- /dev/null
+++ b/theories/UniformConfluence.v
@@ -0,0 +1,219 @@
+(* begin hide *)
+Require Import Arith.
+Require Import Nat.
+Require Import Coq.Program.Equality. (* dependent induction *)
+Require Import Lia.
+(* end hide *)
+Require Import L.
+Require Import Evaluation.
+
+(** * Uniform Confluence 
+    
+    It turns out that it doesn't matter too much what order we choose
+    to perform reductions on subterms. Two different choices will
+    always have a common ancestor downstream. This fact enables the
+    study of several more complicated values of the lamdba calculus.
+*)
+
+(** The uniform confluence of the one-step reduction follows from the
+    restrictiveness of the relation: the source can only be an
+    application and the evaluator only has a choice whether to reduce
+    the left or right hand first before performing a canonical
+    substitution. *)
+Theorem uniform_confluence :
+  forall (s t1 t2: term),
+    one_step_reduces_to s t1 -> one_step_reduces_to s t2 ->
+    t1 = t2 \/ exists (u: term), one_step_reduces_to t1 u /\
+                                   one_step_reduces_to t2 u.
+Proof.
+  intros s. induction s as [n | s1 IHs1 s2 IHs2 | x].
+  - intros t1 t2 Ht1.
+    apply must_one_step_reduce_from_application in Ht1.
+    inversion Ht1 as [x Hx]. inversion Hx as [y Hy].
+    discriminate Hy.
+  - intros t1 t2 Hst1 Hst2.
+    inversion Hst1 as [u1 v1 | u1 v1 v1' | u1 u1' v1].
+    + inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
+      * assert (u1 = u2) as Hu1equ2.
+        { rewrite <- H2 in H. injection H as Heq. apply Heq. }
+        assert (v1 = v2) as Hv1eqv2.
+        { rewrite <- H3 in H0. injection H0 as Heq. apply Heq. }
+        left. rewrite Hu1equ2. rewrite Hv1eqv2. reflexivity.
+      * apply must_one_step_reduce_from_application in H2.
+        inversion H2. inversion H6. rewrite H7 in H. discriminate H.
+      * apply must_one_step_reduce_from_application in H2.
+        inversion H2. inversion H6. rewrite H7 in H0. discriminate H0.
+    + inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
+      * apply must_one_step_reduce_from_application in H.
+        rewrite <- H3 in H. inversion H. inversion H6. discriminate H7.
+      * assert (v1 = v2 \/ exists (u: term),one_step_reduces_to v1 u /\
+                                    one_step_reduces_to v2 u) as Hs1uconf.
+        { apply IHs1. apply H. apply H3. }
+        destruct Hs1uconf.
+        ** left. rewrite H7. reflexivity.
+        ** right. inversion H7 as [x Hx]. exists (app x s2). split.
+           *** apply one_step_appl. apply Hx.
+           *** apply one_step_appl. apply Hx.
+      * right. exists (app v1 v2). split.
+        ** apply one_step_appr. apply H3.
+        ** apply one_step_appl. apply H.
+    + inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
+      * apply must_one_step_reduce_from_application in H.
+        rewrite <- H4 in H. inversion H. inversion H6. discriminate H7.
+      * right. exists (app v2 v1). split.
+        ** apply one_step_appl. apply H3.
+        ** apply one_step_appr. apply H.
+      * assert (v1 = v2 \/ exists (u: term),one_step_reduces_to v1 u /\
+                                              one_step_reduces_to v2 u) as Hs2uconf.
+        { apply IHs2. apply H. apply H3. }
+        destruct Hs2uconf.
+        ** left. rewrite H7. reflexivity.
+        ** right. inversion H7 as [x Hx]. exists (app s1 x). split.
+           *** apply one_step_appr. apply Hx.
+           *** apply one_step_appr. apply Hx.
+  - intros t1 t2 Ht1. apply must_one_step_reduce_from_application in Ht1.
+    inversion Ht1. inversion H. discriminate H0.
+Qed.
+
+
+
+
+
+Theorem measured_uniform_confluence :
+  forall (s t1 t2: term) (m n: nat),
+    n_step_reduces_to m s t1 -> n_step_reduces_to n s t2 ->
+    exists (u: term) (k l: nat),
+      n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
+        m + k = n + l /\ k <= n /\ l <= m.
+Proof.
+  assert (forall (c m n: nat) (s t1 t2: term),
+             m <= c -> n <= c -> n_step_reduces_to m s t1 ->
+             n_step_reduces_to n s t2 -> exists (u: term) (k l: nat),
+                 n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
+                   (m + k = n + l) /\ k <= n /\ l <= m) as Hequiv.
+  { induction c.
+    - intros m n s t1 t2 Hm Hn Hst1 Hst2.
+      apply Nat.le_0_r in Hm. apply Nat.le_0_r in Hn.
+      rewrite Hm in Hst1. inversion Hst1.
+      rewrite Hn in Hst2. inversion Hst2.
+      exists s. exists 0. exists 0.
+      split. rewrite <- H1. apply n_step_refl.
+      split. rewrite <- H3. apply n_step_refl. lia.
+    - intros m n s t1 t2 Hm Hn Hst1 Hst2.
+      inversion Hst1 as [s' Hmeq Hs'eq Ht1eq |
+                          m' s' u1 t1' Hu1onestep
+                            Hu1nstep Hmeq Hs'eq Ht1eq].
+      + exists t2. exists n. exists 0.
+        split. rewrite <- Ht1eq. apply Hst2. split. apply n_step_refl. lia.
+      + inversion Hst2 as [s'' Hneq Hs''eq Ht2eq |
+                            n' s'' u2 t2' Hu2onestep
+                              Hu2nstep Hneq Hs''eq Ht2eq].
+        * exists t1. exists 0. exists m.
+          split. apply n_step_refl. split. rewrite <- Ht2eq. apply Hst1. lia.
+        * (* branch on c = 0 (one step reduction case) *)
+          destruct (1 <=? c) eqn:E.
+          (* c > 0 case: extend diamonds to form induction *)          
+          { assert (c > 0) as Hcgt0. { apply Nat.leb_le in E. lia. }
+            (* build top diamond with uniform confluence *)
+            assert (u1 = u2 \/ exists (w: term),
+                       one_step_reduces_to u1 w /\
+                         one_step_reduces_to u2 w) as Hw.
+            { apply uniform_confluence with (s:=s).
+              apply Hu1onestep. apply Hu2onestep. }
+            destruct Hw.
+            - (* u1 = u2 case *)
+              assert (exists (u: term) (k l: nat),
+                         n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
+                           m' + k = n' + l /\ k <= n' /\ l <= m') as Heq.
+              { apply IHc with (s:=u1). lia. lia. apply Hu1nstep.
+                rewrite H. apply Hu2nstep. }
+              inversion Heq as [u Hequ]. inversion Hequ as [k Hequk].
+              inversion Hequk as [l Hequkl].
+              exists u. exists k. exists l.
+              split. apply Hequkl. split. apply Hequkl. lia.
+            - (* u1 <> u2 case: three more diamonds to form inductive diamond *)
+              inversion H as [w Hw].
+              (* left diamond: t1, w flow to r1 *)
+              assert (exists (r1: term) (k1 l1: nat),
+                         n_step_reduces_to k1 t1 r1 /\ n_step_reduces_to l1 w r1 /\
+                           m' + k1 = 1 + l1 /\ k1 <= 1 /\ l1 <= m') as Hleft.
+              { apply IHc with (s:=u1). lia. lia.
+                apply Hu1nstep. apply n_step_incr with (u:=w). apply Hw.
+                apply n_step_refl. }
+              (* right diamond: t2, w flow to r2 *)
+              assert (exists (r2: term) (k2 l2: nat),
+                         n_step_reduces_to k2 t2 r2 /\ n_step_reduces_to l2 w r2 /\
+                           n' + k2 = 1 + l2 /\ k2 <= 1 /\ l2 <= n') as Hright.
+              { apply IHc with (s:=u2). lia. lia.
+                apply Hu2nstep. apply n_step_incr with (u:=w). apply Hw.
+                apply n_step_refl. }
+              (* bottom diamond: r1, r2 flow from w into x. *)
+              inversion Hleft as [r1 Hleftr1]. inversion Hleftr1 as [k1 Hleftr1k1].
+              inversion Hleftr1k1 as [l1 HleftAll].
+              inversion Hright as [r2 Hrightr2]. inversion Hrightr2 as [k2 Hrightr2k2].
+              inversion Hrightr2k2 as [l2 HrightAll].
+              assert (exists (x: term) (p1 p2: nat),
+                         n_step_reduces_to p1 r1 x /\ n_step_reduces_to p2 r2 x /\
+                           l1 + p1 = l2 + p2 /\ p1 <= l2 /\ p2 <= l1) as Hbottom.
+              { apply IHc with (s:=w). lia. lia. apply HleftAll. apply HrightAll. }
+              (* showing the four diamonds evidence x is as expected *)
+              inversion Hbottom as [x Hx]. inversion Hx as [p1 Hxp1].
+              inversion Hxp1 as [p2 HbottomAll].
+              exists x. exists (k1 + p1). exists (k2 + p2).
+              split. apply n_step_transitivity with (y:=r1).
+              apply HleftAll. apply HbottomAll.
+              split. apply n_step_transitivity with (y:=r2).
+              apply HrightAll. apply HbottomAll. lia. }
+          (* c = 0: special case of one step reductions *)
+          { assert (c = 0) as Hceq0. { apply Nat.leb_gt in E. lia. }
+            assert (m <= 1) as Hmleq1. { lia. }
+            assert (m = 1) as Hmeq1.
+            { apply Nat.le_1_r in Hmleq1. inversion Hmleq1.
+              - rewrite H in Hmeq. discriminate Hmeq.
+              - apply H. }
+            assert (n <= 1) as Hnleq1. { lia. }
+            assert (n = 1) as Hneq1.
+            { apply Nat.le_1_r in Hnleq1. inversion Hnleq1.
+              - rewrite H in Hneq. discriminate Hneq.
+              - apply H. }
+            assert (m' = 0) as Hm'eq0. { lia. }
+            assert (n' = 0) as Hn'eq0. { lia. }
+            assert (one_step_reduces_to s t1) as Hleft.
+            { rewrite Hm'eq0 in Hu1nstep. inversion Hu1nstep.
+              rewrite <- H1. apply Hu1onestep. }
+            assert (one_step_reduces_to s t2) as Hright.
+            { rewrite Hn'eq0 in Hu2nstep. inversion Hu2nstep.
+              rewrite <- H1. apply Hu2onestep. }
+            specialize uniform_confluence with (s:=s) (t1:=t1) (t2:=t2) as Huc.
+            assert (t1 = t2 \/ (exists u : term, one_step_reduces_to t1 u /\
+                                                   one_step_reduces_to t2 u))
+              as HucFinal.
+            { apply Huc. apply Hleft. apply Hright. }
+            destruct HucFinal.
+            - exists t1. exists 0. exists 0.
+              split. apply n_step_refl. split. rewrite H. apply n_step_refl. lia.
+            - inversion H as [u Hu].
+              exists u. exists 1. exists 1.
+              split. apply n_step_incr with (u:=u). apply Hu. apply n_step_refl.
+              split. apply n_step_incr with (u:=u). apply Hu. apply n_step_refl.
+              lia. } }
+  (* now we simply rewrite in terms of the original statement *)
+  intros s t1 t2 m n Hst1 Hst2.
+  apply Hequiv with (c := m + n) (s:=s).
+  lia. lia. apply Hst1. apply Hst2.
+Qed.
+
+Corollary reduction_is_confluent :
+  forall (s t1 t2: term), reduces_to s t1 -> reduces_to s t2 ->
+                          exists (u: term), reduces_to t1 u /\ reduces_to t2 u.
+Proof.
+  intros s t1 t2 Hst1 Hst2.
+  apply reduction_is_realized in Hst1. inversion Hst1 as [m Hm].
+  apply reduction_is_realized in Hst2. inversion Hst2 as [n Hn].
+  specialize measured_uniform_confluence with (s:=s) (t1:=t1) (t2:=t2) (m:=m) (n:=n) as Huc.
+  apply Huc in Hm. inversion Hm as [u Hu]. inversion Hu as [k Huk]. inversion Huk as [l Hukl].
+  exists u. split.
+  apply reduction_is_realized. exists k. apply Hukl.
+  apply reduction_is_realized. exists l. apply Hukl.
+  apply Hn.
+Qed.