pair-eta/theories/compile.v

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

Module Compile.
  Fixpoint F {n} (a : Tm n) : Tm n :=
    match a with
    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
    | Const k => Const k
    | Univ i => Univ i
    | Abs a => Abs (F a)
    | App a b => App (F a) (F b)
    | VarTm i => VarTm i
    | Pair a b => Pair (F a) (F b)
    | Proj t a => Proj t (F a)
    | Bot => Bot
    end.

  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
    F (ren_Tm ξ a)= ren_Tm ξ (F a).
  Proof. move : m ξ. elim : n  / a => //=; scongruence. Qed.

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

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

  Lemma substing n b (a : Tm (S n)) :
    subst_Tm (scons (F b) VarTm) (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 {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).

  Lemma BindInj n p0 p1 (A0 A1 : Tm n) 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 h0 h1] h2].
    apply abs_eq in h2.
    evar (t : Tm (S n)).
    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
    subst t. rewrite -/ren_Tm.
    move : h2. move /join_transitive => /[apply]. asimpl => h2.
    tauto.
  Qed.

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

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

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

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

  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
    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.

Module Equiv.
  Inductive R {n} : Tm n -> Tm n ->  Prop :=
  (***************** Beta ***********************)
  | AppAbs a b :
    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
  | ProjPair p a b :
    R (Proj p (Pair a b)) (if p is PL then a else b)

  (****************** Eta ***********************)
  | AppEta a :
    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
  | PairEta a :
    R a (Pair (Proj PL a) (Proj PR a))

  (*************** Congruence ********************)
  | Var i : R (VarTm i) (VarTm i)
  | AbsCong a b :
    R a b ->
    R (Abs a) (Abs b)
  | AppCong a0 a1 b0 b1 :
    R a0 a1 ->
    R b0 b1 ->
    R (App a0 b0) (App a1 b1)
  | PairCong a0 a1 b0 b1 :
    R a0 a1 ->
    R b0 b1 ->
    R (Pair a0 b0) (Pair a1 b1)
  | ProjCong p a0 a1 :
    R a0 a1 ->
    R (Proj p a0) (Proj p a1)
  | BindCong p A0 A1 B0 B1:
    R A0 A1 ->
    R B0 B1 ->
    R (TBind p A0 B0) (TBind p A1 B1)
  | UnivCong i :
    R (Univ i) (Univ i).
End Equiv.

Module EquivJoin.
  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
  Proof.
    move => h. elim : n a b /h => n.
    - move => a b.
      rewrite /Join.R /join /=.
      eexists. split. apply relations.rtc_once.
      apply Par.AppAbs; auto using Par.refl.
      rewrite Compile.substing.
      apply relations.rtc_refl.
    - move => p a b.
      apply Join.FromPar.
      simpl. apply : Par.ProjPair'; auto using Par.refl.
      case : p => //=.
    - move => a. apply Join.FromPar => /=.
      apply : Par.AppEta'; auto using Par.refl.
      by autorewrite with compile.
    - move => a. apply Join.FromPar => /=.
      apply : Par.PairEta; auto using Par.refl.
    - hauto l:on use:Join.FromPar, Par.Var.
    - hauto lq:on use:Join.AbsCong.
    - qauto l:on use:Join.AppCong.
    - qauto l:on use:Join.PairCong.
    - qauto use:Join.ProjCong.
    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
    - hauto l:on.
  Qed.
End EquivJoin.

Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
Proof.
  move => h. elim : n a b /h.
  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
    rewrite -Compile.substing.
    apply RPar'.AppAbs => //.
  - hauto q:on use:RPar'.ProjPair'.
  - qauto ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
  - hauto lq:on ctrs:RPar'.R.
Qed.

Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.