(* 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.