103 lines
3 KiB
Coq
103 lines
3 KiB
Coq
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 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.
|