Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax fp_red.
Require Import ssreflect ssrbool.
From Hammer Require Import Tactics.
From stdpp Require Import relations (rtc(..)).

Module Compile.
  Definition compileTag p := if p is TPi then 0 else 1.

  Fixpoint F (a : Tm) : PTm :=
    match a with
    | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B))
    | Univ i => PConst (3 + i)
    | Abs _ a => PAbs (F a)
    | App a b => PApp (F a) (F b)
    | VarTm i => VarPTm i
    | Pair a b => PPair (F a) (F b)
    | Proj t a => PProj t (F a)
    | If a b c => PApp (PApp (F a) (F b)) (F c)
    | BVal b => if b then (PAbs (PAbs (VarPTm (shift var_zero)))) else (PAbs (PAbs (VarPTm var_zero)))
    | Bool => PConst 2
    end.

  Lemma renaming (a : Tm) (ξ : nat -> nat) :
    F (ren_Tm ξ a)= ren_PTm ξ (F a).
  Proof. move : ξ. elim : a => //=; hauto lq:on. Qed.

  #[local]Hint Rewrite Compile.renaming : compile.

  Lemma morphing (a : Tm) ρ0 ρ1 :
    (forall i, ρ0 i = F (ρ1 i)) ->
    subst_PTm ρ0 (F a) = F (subst_Tm ρ1 a).
  Proof.
    move : ρ0 ρ1. elim : a =>//=.
    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
    - hauto lq:on rew:off.
    - hauto lq:on rew:off.
    - hauto lq:on.
    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
    - hauto lq:on rew:off.
    - hauto lq:on rew:off.
  Qed.

  Lemma substing b (a : Tm) :
    subst_PTm (scons (F b) VarPTm) (F a) = F (subst_Tm (scons b VarTm) a).
  Proof.
    apply morphing.
    case => //=.
  Qed.

End Compile.

#[export] Hint Rewrite Compile.renaming Compile.morphing : compile.


Module Join.
  Definition R (a b : Tm) := join (Compile.F a) (Compile.F b).

  Lemma compileTagInj p0 p1 :
    Compile.compileTag p0 = Compile.compileTag p1 -> p0 = p1.
  Proof.
    case : p0 ; case : p1 => //.
  Qed.

  Lemma BindInj p0 p1 (A0 A1 : Tm) B0 B1  :
    R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
  Proof.
    rewrite /R /= !join_pair_inj.
    move => [[/join_const_inj /compileTagInj h0 h1] h2].
    apply abs_eq in h2.
    evar (t : PTm ).
    have : join (PApp (ren_PTm shift (PAbs (Compile.F B1))) (VarPTm var_zero)) t by
      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
    subst t. rewrite -/ren_PTm.
    move : h2. move /join_transitive => /[apply]. asimpl; rewrite subst_id => h2.
    tauto.
  Qed.

  Lemma BindCong p A0 A1 B0 B1 :
    R A0 A1 ->
    R B0 B1 ->
    R (TBind p A0 B0) (TBind p A1 B1).
  Proof.
    move => h0 h1. rewrite /R /=.
    apply join_pair_inj.
    split. apply join_pair_inj. split. apply join_refl. done.
    by apply Join.AbsCong.
  Qed.

  Lemma UnivInj i j : R (Univ i : Tm) (Univ j) -> i = j.
  Proof. hauto l:on use:join_const_inj. Qed.

  Lemma transitive (a b c : Tm) :
    R a b -> R b c -> R a c.
  Proof. hauto l:on use:join_transitive unfold:R. Qed.

  Lemma symmetric (a b : Tm) :
    R a b -> R b a.
  Proof. hauto l:on use:join_symmetric. Qed.

  Lemma reflexive (a : Tm) :
    R a a.
  Proof. hauto l:on use:join_refl. Qed.

  Lemma substing (a b : Tm) (ρ : nat -> Tm) :
    R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
  Proof.
    rewrite /R.
    rewrite /join.
    move => [C [h0 h1]].
    repeat (rewrite <- Compile.morphing with (ρ0 := funcomp Compile.F ρ); last by reflexivity).
    hauto lq:on use:join_substing.
  Qed.

End Join.