Simple build and README.

1 files changed, 219 insertions, 0 deletions

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.