264 lines
9.3 KiB
Coq
264 lines
9.3 KiB
Coq
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural.
|
|
From Hammer Require Import Tactics.
|
|
Require Import ssreflect.
|
|
Require Import Psatz.
|
|
Require Import Coq.Logic.FunctionalExtensionality.
|
|
|
|
Derive Inversion wff_inv with (forall Γ, ⊢ Γ) Sort Prop.
|
|
|
|
Lemma T_Abs Γ (a : PTm ) A B :
|
|
(cons A Γ) ⊢ a ∈ B ->
|
|
Γ ⊢ PAbs a ∈ PBind PPi A B.
|
|
Proof.
|
|
move => ha.
|
|
have [i hB] : exists i, (cons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
|
|
have hΓ : ⊢ (cons A Γ) by sfirstorder use:wff_mutual.
|
|
hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
|
|
Qed.
|
|
|
|
|
|
Lemma App_Inv Γ (b a : PTm) U :
|
|
Γ ⊢ PApp b a ∈ U ->
|
|
exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
|
|
Proof.
|
|
move E : (PApp b a) => u hu.
|
|
move : b a E. elim : Γ u U / hu => //=.
|
|
- move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
|
|
exists A,B.
|
|
repeat split => //=.
|
|
have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
|
|
hauto lq:on use:bind_inst, E_Refl.
|
|
- hauto lq:on rew:off ctrs:LEq.
|
|
Qed.
|
|
|
|
|
|
Lemma Abs_Inv Γ (a : PTm) U :
|
|
Γ ⊢ PAbs a ∈ U ->
|
|
exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
|
|
Proof.
|
|
move E : (PAbs a) => u hu.
|
|
move : a E. elim : Γ u U / hu => //=.
|
|
- move => Γ a A B i hP _ ha _ a0 [*]. subst.
|
|
exists A, B. repeat split => //=.
|
|
hauto lq:on use:E_Refl, Su_Eq.
|
|
- hauto lq:on rew:off ctrs:LEq.
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
|
|
Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
|
|
Proof.
|
|
move => a b Γ A ha.
|
|
move /App_Inv : ha.
|
|
move => [A0][B0][ha][hb]hS.
|
|
move /Abs_Inv : ha => [A1][B1][ha]hS0.
|
|
have hb' := hb.
|
|
move /E_Refl in hb.
|
|
have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
|
|
have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
|
|
move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
|
|
move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
|
|
move => h.
|
|
apply : E_Conv; eauto.
|
|
apply : E_AppAbs; eauto.
|
|
eauto using T_Conv.
|
|
Qed.
|
|
|
|
Lemma T_Eta Γ A a B :
|
|
A :: Γ ⊢ a ∈ B ->
|
|
A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B.
|
|
Proof.
|
|
move => ha.
|
|
have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual.
|
|
have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff.
|
|
have hΓ : ⊢ Γ by hauto lq:on inv:Wff.
|
|
eapply T_App' with (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
|
|
apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift.
|
|
econstructor; eauto. sauto l:on use:renaming.
|
|
apply T_Var => //.
|
|
by constructor.
|
|
Qed.
|
|
|
|
Lemma E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
|
|
Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
|
|
(cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
|
|
Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
|
|
Proof.
|
|
move => h0 h1.
|
|
have : Γ ⊢ A0 ∈ PUniv i by hauto l:on use:regularity.
|
|
have : ⊢ Γ by sfirstorder use:wff_mutual.
|
|
move : E_Bind h0 h1; repeat move/[apply].
|
|
firstorder.
|
|
Qed.
|
|
|
|
Lemma E_App Γ (b0 b1 a0 a1 : PTm ) A B :
|
|
Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
|
|
Γ ⊢ a0 ≡ a1 ∈ A ->
|
|
Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
|
|
Proof.
|
|
move => h.
|
|
have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto l:on use:regularity.
|
|
move : E_App h. by repeat move/[apply].
|
|
Qed.
|
|
|
|
Lemma E_Proj2 Γ (a b : PTm) A B :
|
|
Γ ⊢ a ≡ b ∈ PBind PSig A B ->
|
|
Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
|
|
Proof.
|
|
move => h.
|
|
have [i] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto l:on use:regularity.
|
|
move : E_Proj2 h; by repeat move/[apply].
|
|
Qed.
|
|
|
|
Lemma E_FunExt Γ (a b : PTm) A B :
|
|
Γ ⊢ a ∈ PBind PPi A B ->
|
|
Γ ⊢ b ∈ PBind PPi A B ->
|
|
A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
|
|
Γ ⊢ a ≡ b ∈ PBind PPi A B.
|
|
Proof.
|
|
hauto l:on use:regularity, E_FunExt.
|
|
Qed.
|
|
|
|
Lemma E_PairExt Γ (a b : PTm) A B :
|
|
Γ ⊢ a ∈ PBind PSig A B ->
|
|
Γ ⊢ b ∈ PBind PSig A B ->
|
|
Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
|
|
Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
|
|
Γ ⊢ a ≡ b ∈ PBind PSig A B. hauto l:on use:regularity, E_PairExt. Qed.
|
|
|
|
Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 :
|
|
renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 ->
|
|
renaming_ok Γ Ξ (funcomp ξ0 ξ1).
|
|
rewrite /renaming_ok => h0 h1 i A.
|
|
move => {}/h1 {}/h0.
|
|
by asimpl.
|
|
Qed.
|
|
|
|
Lemma E_AppEta Γ (b : PTm) A B :
|
|
Γ ⊢ b ∈ PBind PPi A B ->
|
|
Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
|
|
Proof.
|
|
move => h.
|
|
have [i hPi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
|
|
have [j [hA hB]] : exists i, Γ ⊢ A ∈ PUniv i /\ A :: Γ ⊢ B ∈ PUniv i by hauto lq:on use:Bind_Inv.
|
|
have {i} {}hPi : Γ ⊢ PBind PPi A B ∈ PUniv j by sfirstorder use:T_Bind, wff_mutual.
|
|
have hΓ : ⊢ A :: Γ by hauto lq:on use:Bind_Inv, Wff_Cons'.
|
|
have hΓ' : ⊢ ren_PTm shift A :: A :: Γ by sauto lq:on use:renaming, renaming_shift inv:Wff.
|
|
apply E_FunExt; eauto.
|
|
apply T_Abs.
|
|
eapply T_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
|
|
change (PBind _ _ _) with (ren_PTm shift (PBind PPi A B)).
|
|
|
|
eapply renaming; eauto.
|
|
apply renaming_shift.
|
|
constructor => //.
|
|
by constructor.
|
|
|
|
apply : E_Transitive. simpl.
|
|
apply E_AppAbs' with (i := j)(A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B); eauto.
|
|
by asimpl; rewrite subst_scons_id.
|
|
hauto q:on use:renaming, renaming_shift.
|
|
constructor => //.
|
|
by constructor.
|
|
asimpl.
|
|
eapply T_App' with (A := ren_PTm shift (ren_PTm shift A)) (B := ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B)); cycle 2.
|
|
constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift.
|
|
by constructor. asimpl. substify. by asimpl.
|
|
have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))= (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl.
|
|
eapply renaming; eauto. by eauto using renaming_shift, renaming_comp.
|
|
asimpl. renamify.
|
|
eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
|
|
hauto q:on use:renaming, renaming_shift.
|
|
sauto lq:on use:renaming, renaming_shift, E_Refl.
|
|
constructor. constructor=>//. constructor.
|
|
Qed.
|
|
|
|
Lemma Proj1_Inv Γ (a : PTm ) U :
|
|
Γ ⊢ PProj PL a ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
|
|
Proof.
|
|
move E : (PProj PL a) => u hu.
|
|
move :a E. elim : Γ u U / hu => //=.
|
|
- move => Γ a A B ha _ a0 [*]. subst.
|
|
exists A, B. split => //=.
|
|
eapply regularity in ha.
|
|
move : ha => [i].
|
|
move /Bind_Inv => [j][h _].
|
|
by move /E_Refl /Su_Eq in h.
|
|
- hauto lq:on rew:off ctrs:LEq.
|
|
Qed.
|
|
|
|
Lemma Proj2_Inv Γ (a : PTm) U :
|
|
Γ ⊢ PProj PR a ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
|
|
Proof.
|
|
move E : (PProj PR a) => u hu.
|
|
move :a E. elim : Γ u U / hu => //=.
|
|
- move => Γ a A B ha _ a0 [*]. subst.
|
|
exists A, B. split => //=.
|
|
have ha' := ha.
|
|
eapply regularity in ha.
|
|
move : ha => [i ha].
|
|
move /T_Proj1 in ha'.
|
|
apply : bind_inst; eauto.
|
|
apply : E_Refl ha'.
|
|
- hauto lq:on rew:off ctrs:LEq.
|
|
Qed.
|
|
|
|
Lemma Pair_Inv Γ (a b : PTm ) U :
|
|
Γ ⊢ PPair a b ∈ U ->
|
|
exists A B, Γ ⊢ a ∈ A /\
|
|
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
|
|
Γ ⊢ PBind PSig A B ≲ U.
|
|
Proof.
|
|
move E : (PPair a b) => u hu.
|
|
move : a b E. elim : Γ u U / hu => //=.
|
|
- move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
|
|
exists A,B. repeat split => //=.
|
|
move /E_Refl /Su_Eq : hS. apply.
|
|
- hauto lq:on rew:off ctrs:LEq.
|
|
Qed.
|
|
|
|
Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
|
|
Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
|
|
Proof.
|
|
move => a b Γ A.
|
|
move /Proj1_Inv. move => [A0][B0][hab]hA0.
|
|
move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
|
|
have [i ?] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
|
|
move /Su_Sig_Proj1 in hS.
|
|
have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
|
|
apply : E_Conv; eauto.
|
|
apply : E_ProjPair1; eauto.
|
|
Qed.
|
|
|
|
Lemma E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
|
|
Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
|
|
Proof.
|
|
move => a b Γ A. move /Proj2_Inv.
|
|
move => [A0][B0][ha]h.
|
|
have hr := ha.
|
|
move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
|
|
have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
|
|
have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using E_ProjPair1 with wt.
|
|
move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
|
|
apply : E_Conv; eauto.
|
|
apply : E_Conv; eauto.
|
|
apply : E_ProjPair2; eauto.
|
|
Qed.
|
|
|
|
|
|
Lemma E_PairEta Γ a A B :
|
|
Γ ⊢ a ∈ PBind PSig A B ->
|
|
Γ ⊢ PPair (PProj PL a) (PProj PR a) ≡ a ∈ PBind PSig A B.
|
|
Proof.
|
|
move => h.
|
|
have [i hSig] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto use:regularity.
|
|
apply E_PairExt => //.
|
|
eapply T_Pair; eauto with wt.
|
|
apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
|
|
by eauto with wt.
|
|
apply E_ProjPair2.
|
|
apply : T_Proj2; eauto with wt.
|
|
Qed.
|