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.