Set Implicit Arguments.
Require Import Morphisms Omega FinFun.
From Undecidability.HOU Require Export std.std calculus.syntax calculus.semantics calculus.confluence.

Section Equivalence.
  Context {X: Const}.
  Notation "s ≡ t" := (equiv (@step X) s t) (at level 70).

  Section CompatibilityProperties.

    Global Instance equiv_lam_proper:
      Proper (equiv step ++> equiv step) (@lam X).
    Proof.
      intros ? ? (v & H1 & H2) % church_rosser; eauto.
      rewrite H1, H2. reflexivity.
    Qed.

    Global Instance equiv_app_proper:
      Proper (equiv step ++> equiv step ++> equiv step) (@app X).
    Proof.
      intros ? ? (v & H1 & H2) % church_rosser ? ? (v' & H3 & H4) % church_rosser;
        eauto.
      rewrite H1, H2, H3, H4. reflexivity.
    Qed.

    Lemma ren_equiv s t delta:
      s ≡ t -> ren delta s ≡ ren delta t.
    Proof.
      intros (v & ? & ?) % church_rosser; eauto.
      transitivity (ren delta v); [| symmetry].
      all: eapply equiv_star, ren_steps; eauto.
    Qed.

    Global Instance ren_equiv_proper:
      Proper (eq ++> equiv step ++> equiv step) (@ren X).
    Proof.
      intros ? zeta -> s t H; now eapply ren_equiv.
    Qed.

    Lemma subst_equiv s t sigma:
      s ≡ t -> sigma • s ≡ sigma • t.
    Proof.
      intros (v & ? & ?) % church_rosser; eauto.
      transitivity (sigma • v); [| symmetry].
      all: eapply equiv_star, subst_steps; eauto.
    Qed.

    Global Instance subst_equiv_proper:
      Proper (eq ++> equiv step ++> equiv step) (@subst_exp X).
    Proof.
      intros ? zeta -> s t H; now eapply subst_equiv.
    Qed.

    Lemma subst_pointwise_equiv (s: exp X) sigma tau:
      (forall x, x ∈ vars s -> sigma x ≡ tau x) -> sigma • s ≡ tau • s.
    Proof.
      induction s in sigma, tau |-*; cbn -[vars]; eauto.
      - intros H; eapply equiv_lam_proper, IHs.
        intros []; cbn -[vars]. reflexivity.
        intros ? % vars_varof % varofLambda % varof_vars % H.
        unfold funcomp.
        now eapply ren_equiv.
      - intros H; rewrite IHs1, IHs2; eauto.
    Qed.

  End CompatibilityProperties.

  Section InjectivityProperties.

    Lemma equiv_var_eq (x y: fin):
      var x ≡ var y -> x = y.
    Proof.
      intros; eapply equiv_unique_normal_forms in H; eauto.
      congruence.
    Qed.

    Lemma equiv_const_eq (x y: X):
      const x ≡ const y -> x = y.
    Proof.
      intros; eapply equiv_unique_normal_forms in H; eauto.
      congruence.
    Qed.

    Lemma equiv_lam_elim (s t: exp X):
      lambda s ≡ lambda t -> s ≡ t.
    Proof.
      intros (v & [] %steps_lam & [] %steps_lam) % church_rosser; intuition; subst.
      injection H as ->; eauto.
    Qed.

    Lemma equiv_app_elim (s s' t t': exp X):
      s t ≡ s' t' -> isAtom (head s) -> isAtom (head s') -> s ≡ s' /\ t ≡ t'.
    Proof.
      intros (v & [] % steps_app & [] % steps_app) % church_rosser H3; eauto.
      * do 2 destruct H, H0; intuition; subst;
          injection H as -> ->; eauto.
      * do 2 destruct H; destruct H0; intuition; subst.
        all: destruct (head s'); cbn in *; intuition.
      * do 2 destruct H0; destruct H; intuition; subst.
        all: destruct (head s); cbn in *; intuition.
      * destruct H, H0; intuition.
        all: destruct (head s); cbn in *; intuition.
    Qed.

    Lemma equiv_anti_ren delta (s t: exp X):
      Injective delta -> ren delta s ≡ ren delta t -> s ≡ t.
    Proof.
      intros ? (v & H1 & H2) % church_rosser; eauto.
      eapply steps_anti_ren in H1 as [].
      eapply steps_anti_ren in H2 as [].
      intuition; subst.
      eapply anti_ren in H4; eauto.
      subst; eauto.
    Qed.

  End InjectivityProperties.

  Section DisjointnessProperties.

    Lemma equiv_neq_var_app (x: nat) (s t: exp X):
      var x ≡ s t -> isAtom (head s) -> False.
    Proof.
      intros EQ.
      destruct (head s) as [y | | | ] eqn: H'; intuition.
      all: eapply church_rosser in EQ as (v & L & R); eauto.
      all: inv L; firstorder using normal_var.
      all: eapply steps_app in R as [R|R].
      1, 3: destruct R as (? & ? & ? & ?); discriminate.
      all: destruct R; intuition; rewrite H' in *; syn.
    Qed.

    Lemma equiv_neq_lambda_app (s' s t: exp X):
      lambda s' ≡ s t -> isAtom (head s) -> False.
    Proof.
      intros EQ.
      destruct (head s) as [y | | | ] eqn: H'; intuition.
      all: eapply church_rosser in EQ as (v & L & R); eauto.
      all: eapply steps_lam in L as (v' & ? & ?); subst.
      all: eapply steps_app in R as [R|R].
      1, 3: destruct R as (? & ? & ? & ?); discriminate.
      all: destruct R; intuition; rewrite H' in *; syn.
    Qed.

    Lemma equiv_neq_var_lambda (x: nat) s: ~ var x ≡ lambda s.
    Proof.
      intros (v & ? & ?) % church_rosser; eauto.
      inv H; firstorder using normal_var.
      eapply steps_lam in H0 as []; intuition; discriminate.
    Qed.

    Lemma equiv_neq_var_const (x: nat) c: ~ var x ≡ const c.
    Proof.
      intros (v & ? & ?) % church_rosser; eauto.
      inv H; firstorder using normal_var.
      inv H0. inv H.
    Qed.

    Lemma equiv_neq_const_lam s c: ~ const c ≡ lambda s.
    Proof.
      intros (v & ? & ?) % church_rosser; eauto.
      inv H; firstorder using normal_var.
      eapply steps_lam in H0 as []; intuition; discriminate.
      inv H1.
    Qed.

    Lemma equiv_neq_const_app (s t: exp X) c:
      const c ≡ s t -> isAtom (head s) -> False.
    Proof.
      intros EQ.
      destruct (head s) as [y | | | ] eqn: H'; intuition.
      all: eapply church_rosser in EQ as (v & L & R); eauto.
      all: inv L; firstorder using normal_const.
      all: eapply steps_app in R as [R|R].
      1, 3: destruct R as (? & ? & ? & ?); discriminate.
      all: destruct R; intuition; rewrite H' in *; syn.
    Qed.

  End DisjointnessProperties.

  Section HuetDefinition.
    Variable (s t v1 v2: exp X).
    Hypothesis (E1: s ▷ v1) (E2: t ▷ v2).

    Lemma equiv_huet_forward:
      s ≡ t -> v1 = v2.
    Proof.
      destruct E1 as [H1 N1], E2 as [H2 N2].
      intros H; eapply equiv_unique_normal_forms; eauto.
      now rewrite <-H1, <-H2.
    Qed.

    Lemma equiv_huet_backward:
      v1 = v2 -> s ≡ t.
    Proof.
      intros; subst; destruct E1, E2; eapply equiv_join; eauto.
    Qed.
  End HuetDefinition.

End Equivalence.

Notation "s ≡ t" := (equiv step s t) (at level 70).

Hint Resolve equiv_neq_var_app equiv_neq_var_lambda equiv_neq_var_const
     equiv_neq_const_app equiv_neq_const_lam equiv_neq_lambda_app.

Ltac ClearRefl H :=
  let T := type of H in
  match T with
  | ?X ≡ ?X => clear H
  | _ => idtac
  end.

Ltac Injection H :=
  let T := type of H in
  let H1 := fresh "H" in
  let H2 := fresh "H" in
  match T with
  | var _ ≡ var _ => eapply equiv_var_eq in H as H1; ClearRefl H1
  | const _ ≡ const _ => eapply equiv_const_eq in H as H1; ClearRefl H1
  | lambda _ ≡ lambda _ => eapply equiv_lam_elim in H as H1; ClearRefl H1
  | app _ _ ≡ app _ _ => eapply equiv_app_elim in H as [H1 H2]; [| atom..]; ClearRefl H1; ClearRefl H2
  end.

Ltac Discriminate :=
  match goal with
  | [H: var _ ≡ const _ |- _] => eapply equiv_neq_var_const in H as []
  | [H: const _ ≡ var _ |- _] => symmetry in H; eapply equiv_neq_var_const in H as []
  | [H: var _ ≡ app _ _ |- _] => solve [eapply equiv_neq_var_app in H as []; atom]
  | [H: app _ _ ≡ var _ |- _] => solve [symmetry in H; eapply equiv_neq_var_app in H as []; atom]
  | [H: var _ ≡ lambda _ |- _] => eapply equiv_neq_var_lambda in H as []
  | [H: lambda _ ≡ var _ |- _] => symmetry in H; eapply equiv_neq_var_lambda in H as []
  | [H: const _ ≡ lambda _ |- _] => eapply equiv_neq_const_lam in H as []
  | [H: lambda _ ≡ const _ |- _] => symmetry in H; eapply equiv_neq_const_lam in H as []
  | [H: const _ ≡ app _ _ |- _] => solve [eapply equiv_neq_const_app in H as []; atom]
  | [H: app _ _ ≡ const _ |- _] => solve [symmetry in H; eapply equiv_neq_const_app in H as []; atom]
  | [H: lambda _ ≡ app _ _ |- _] => solve [eapply equiv_neq_lambda_app in H as []; atom]
  | [H: app _ _ ≡ lambda _ |- _] => solve [symmetry in H; eapply equiv_neq_lambda_app in H as []; atom]
  | [H: var _ ≡ var _ |- _] => solve [eapply equiv_var_eq in H as ?; discriminate]
  | [H: const _ ≡ const _ |- _] => solve [eapply equiv_const_eq in H as ?; discriminate]
  end.

Lemma equiv_head_equal X (s t: exp X):
  s ≡ t -> isAtom (head s) -> isAtom (head t) -> head s = head t.
Proof.
  induction s in t |-*; destruct t; intros; try Discriminate; Injection H; subst; eauto.
  - cbn in *; intuition.
  - cbn; eapply IHs1; eauto.
Qed.