69 lines
2.5 KiB
Coq
69 lines
2.5 KiB
Coq
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
|
|
From Hammer Require Import Tactics.
|
|
Require Import ssreflect.
|
|
Require Import Psatz.
|
|
Require Import Coq.Logic.FunctionalExtensionality.
|
|
|
|
Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
|
|
|
|
Lemma Wff_Cons_Inv n Γ (A : PTm n) :
|
|
⊢ funcomp (ren_PTm shift) (scons A Γ) ->
|
|
⊢ Γ /\ exists i, Γ ⊢ A ∈ PUniv i.
|
|
Proof.
|
|
elim /wff_inv => //= _.
|
|
move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
|
|
Equality.simplify_dep_elim.
|
|
have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
|
|
move /(_ var_zero) : (h).
|
|
rewrite /funcomp. asimpl.
|
|
move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
|
|
move => ?. subst.
|
|
have : Γ0 = Γ. extensionality i.
|
|
move /(_ (Some i)) : h.
|
|
rewrite /funcomp. asimpl.
|
|
move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
|
|
done.
|
|
move => ?. subst. sfirstorder.
|
|
Qed.
|
|
|
|
Lemma T_Abs n Γ (a : PTm (S n)) A B :
|
|
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
|
|
Γ ⊢ PAbs a ∈ PBind PPi A B.
|
|
Proof.
|
|
move => ha.
|
|
have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
|
|
have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
|
|
move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
|
|
hauto lq:on rew:off use:T_Bind', typing.T_Abs.
|
|
Qed.
|
|
|
|
Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
|
|
Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
|
|
funcomp (ren_PTm shift) (scons 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 n Γ (b0 b1 a0 a1 : PTm n) 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 n Γ (a b : PTm n) 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.
|