1 files changed, 121 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.