yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Finish refactoring substitution lemmas

Browse source
This commit is contained in:
Yiyun Liu 2025-03-03 15:22:59 -05:00
parent 896d22ac9b
commit d68adf85f4
4 changed files with 244 additions and 235 deletions
Download patch file Download diff file Expand all files Collapse all files

16
theories/common.v
View file

@ -10,6 +10,12 @@ Inductive lookup : nat -> list PTm -> PTm -> Prop :=
lookup i Γ A -> lookup i Γ A ->
lookup (S i) (cons B Γ) (ren_PTm shift A). lookup (S i) (cons B Γ) (ren_PTm shift A).
Lemma lookup_deter i Γ A B :
lookup i Γ A ->
lookup i Γ B ->
A = B.
Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed.
Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U. Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
Proof. move => ->. apply here. Qed. Proof. move => ->. apply here. Qed.
@ -126,6 +132,14 @@ Definition ishne_ren (a : PTm) (ξ : nat -> nat) :
ishne (ren_PTm ξ a) = ishne a. ishne (ren_PTm ξ a) = ishne a.
Proof. move : ξ. elim : a => //=. Qed. Proof. move : ξ. elim : a => //=. Qed.
Lemma renaming_shift Γ (ρ : nat -> PTm) A : Lemma renaming_shift Γ A :
renaming_ok (cons A Γ) Γ shift. renaming_ok (cons A Γ) Γ shift.
Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed. Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed.
Lemma subst_scons_id (a : PTm) :
subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) a = a.
Proof.
have E : subst_PTm VarPTm a = a by asimpl.
rewrite -{2}E.
apply ext_PTm. case => //=.
Qed.

8
theories/fp_red.v
View file

@ -12,14 +12,6 @@ Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
Require Import Btauto. Require Import Btauto.
Require Import Cdcl.Itauto. Require Import Cdcl.Itauto.
Lemma subst_scons_id (a : PTm) :
subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) a = a.
Proof.
have E : subst_PTm VarPTm a = a by asimpl.
rewrite -{2}E.
apply ext_PTm. case => //=.
Qed.
Ltac2 spec_refl () := Ltac2 spec_refl () :=
List.iter List.iter
(fun a => match a with (fun a => match a with

12
theories/preservation.v
View file

@ -1,15 +1,15 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red.
From Hammer Require Import Tactics. From Hammer Require Import Tactics.
Require Import ssreflect. Require Import ssreflect.
Require Import Psatz. Require Import Psatz.
Require Import Coq.Logic.FunctionalExtensionality. Require Import Coq.Logic.FunctionalExtensionality.
Lemma App_Inv n Γ (b a : PTm n) U : Lemma App_Inv Γ (b a : PTm) U :
Γ ⊢ PApp b a ∈ U -> Γ ⊢ PApp b a ∈ U ->
exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U. exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
Proof. Proof.
move E : (PApp b a) => u hu. move E : (PApp b a) => u hu.
move : b a E. elim : n Γ u U / hu => n //=. move : b a E. elim : Γ u U / hu => //=.
- move => Γ b a A B hb _ ha _ b0 a0 [*]. subst. - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
exists A,B. exists A,B.
repeat split => //=. repeat split => //=.
@ -18,12 +18,12 @@ Proof.
- hauto lq:on rew:off ctrs:LEq. - hauto lq:on rew:off ctrs:LEq.
Qed. Qed.
Lemma Abs_Inv n Γ (a : PTm (S n)) U : Lemma Abs_Inv Γ (a : PTm) U :
Γ ⊢ PAbs a ∈ U -> Γ ⊢ PAbs a ∈ U ->
exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U. exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
Proof. Proof.
move E : (PAbs a) => u hu. move E : (PAbs a) => u hu.
move : a E. elim : n Γ u U / hu => n //=. move : a E. elim : Γ u U / hu => //=.
- move => Γ a A B i hP _ ha _ a0 [*]. subst. - move => Γ a A B i hP _ ha _ a0 [*]. subst.
exists A, B. repeat split => //=. exists A, B. repeat split => //=.
hauto lq:on use:E_Refl, Su_Eq. hauto lq:on use:E_Refl, Su_Eq.

439
theories/structural.v
View file

@ -75,44 +75,44 @@ Qed.
Lemma E_IndCong' Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i U : Lemma E_IndCong' Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i U :
U = subst_PTm (scons a0 VarPTm) P0 -> U = subst_PTm (scons a0 VarPTm) P0 ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i -> (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i -> (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
Γ ⊢ a0 ≡ a1 ∈ PNat -> Γ ⊢ a0 ≡ a1 ∈ PNat ->
Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 -> Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) -> (cons P0 (cons PNat Γ)) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ U. Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ U.
Proof. move => ->. apply E_IndCong. Qed. Proof. move => ->. apply E_IndCong. Qed.
Lemma T_Ind' s Γ P (a : PTm s) b c i U : Lemma T_Ind' Γ P (a : PTm) b c i U :
U = subst_PTm (scons a VarPTm) P -> U = subst_PTm (scons a VarPTm) P ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> cons PNat Γ ⊢ P ∈ PUniv i ->
Γ ⊢ a ∈ PNat -> Γ ⊢ a ∈ PNat ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> cons P (cons PNat Γ) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P a b c ∈ U. Γ ⊢ PInd P a b c ∈ U.
Proof. move =>->. apply T_Ind. Qed. Proof. move =>->. apply T_Ind. Qed.
Lemma T_Proj2' n Γ (a : PTm n) A B U : Lemma T_Proj2' Γ (a : PTm) A B U :
U = subst_PTm (scons (PProj PL a) VarPTm) B -> U = subst_PTm (scons (PProj PL a) VarPTm) B ->
Γ ⊢ a ∈ PBind PSig A B -> Γ ⊢ a ∈ PBind PSig A B ->
Γ ⊢ PProj PR a ∈ U. Γ ⊢ PProj PR a ∈ U.
Proof. move => ->. apply T_Proj2. Qed. Proof. move => ->. apply T_Proj2. Qed.
Lemma E_Proj2' n Γ i (a b : PTm n) A B U : Lemma E_Proj2' Γ i (a b : PTm) A B U :
U = subst_PTm (scons (PProj PL a) VarPTm) B -> U = subst_PTm (scons (PProj PL a) VarPTm) B ->
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ≡ b ∈ PBind PSig A B -> Γ ⊢ a ≡ b ∈ PBind PSig A B ->
Γ ⊢ PProj PR a ≡ PProj PR b ∈ U. Γ ⊢ PProj PR a ≡ PProj PR b ∈ U.
Proof. move => ->. apply E_Proj2. Qed. Proof. move => ->. apply E_Proj2. Qed.
Lemma E_Bind' n Γ i p (A0 A1 : PTm n) B0 B1 : Lemma E_Bind' Γ i p (A0 A1 : PTm) B0 B1 :
Γ ⊢ A0 ∈ PUniv i -> Γ ⊢ A0 ∈ PUniv i ->
Γ ⊢ A0 ≡ A1 ∈ PUniv i -> Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> cons A0 Γ ⊢ B0 ≡ B1 ∈ PUniv i ->
Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i. Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
Proof. hauto lq:on use:E_Bind, wff_mutual. Qed. Proof. hauto lq:on use:E_Bind, wff_mutual. Qed.
Lemma E_App' n Γ i (b0 b1 a0 a1 : PTm n) A B U : Lemma E_App' Γ i (b0 b1 a0 a1 : PTm) A B U :
U = subst_PTm (scons a0 VarPTm) B -> U = subst_PTm (scons a0 VarPTm) B ->
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B -> Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
@ -120,16 +120,16 @@ Lemma E_App' n Γ i (b0 b1 a0 a1 : PTm n) A B U :
Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ U. Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ U.
Proof. move => ->. apply E_App. Qed. Proof. move => ->. apply E_App. Qed.
Lemma E_AppAbs' n Γ (a : PTm (S n)) b A B i u U : Lemma E_AppAbs' Γ (a : PTm) b A B i u U :
u = subst_PTm (scons b VarPTm) a -> u = subst_PTm (scons b VarPTm) a ->
U = subst_PTm (scons b VarPTm ) B -> U = subst_PTm (scons b VarPTm ) B ->
Γ ⊢ PBind PPi A B ∈ PUniv i -> Γ ⊢ PBind PPi A B ∈ PUniv i ->
Γ ⊢ b ∈ A -> Γ ⊢ b ∈ A ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B -> cons A Γ ⊢ a ∈ B ->
Γ ⊢ PApp (PAbs a) b ≡ u ∈ U. Γ ⊢ PApp (PAbs a) b ≡ u ∈ U.
move => -> ->. apply E_AppAbs. Qed. move => -> ->. apply E_AppAbs. Qed.
Lemma E_ProjPair2' n Γ (a b : PTm n) A B i U : Lemma E_ProjPair2' Γ (a b : PTm) A B i U :
U = subst_PTm (scons a VarPTm) B -> U = subst_PTm (scons a VarPTm) B ->
Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
@ -137,14 +137,14 @@ Lemma E_ProjPair2' n Γ (a b : PTm n) A B i U :
Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U. Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U.
Proof. move => ->. apply E_ProjPair2. Qed. Proof. move => ->. apply E_ProjPair2. Qed.
Lemma E_AppEta' n Γ (b : PTm n) A B i u : Lemma E_AppEta' Γ (b : PTm ) A B i u :
u = (PApp (ren_PTm shift b) (VarPTm var_zero)) -> u = (PApp (ren_PTm shift b) (VarPTm var_zero)) ->
Γ ⊢ PBind PPi A B ∈ (PUniv i) -> Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ b ∈ PBind PPi A B ->
Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B. Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B.
Proof. qauto l:on use:wff_mutual, E_AppEta. Qed. Proof. qauto l:on use:wff_mutual, E_AppEta. Qed.
Lemma Su_Pi_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T : Lemma Su_Pi_Proj2' Γ (a0 a1 A0 A1 : PTm ) B0 B1 U T :
U = subst_PTm (scons a0 VarPTm) B0 -> U = subst_PTm (scons a0 VarPTm) B0 ->
T = subst_PTm (scons a1 VarPTm) B1 -> T = subst_PTm (scons a1 VarPTm) B1 ->
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
@ -152,7 +152,7 @@ Lemma Su_Pi_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
Γ ⊢ U ≲ T. Γ ⊢ U ≲ T.
Proof. move => -> ->. apply Su_Pi_Proj2. Qed. Proof. move => -> ->. apply Su_Pi_Proj2. Qed.
Lemma Su_Sig_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T : Lemma Su_Sig_Proj2' Γ (a0 a1 A0 A1 : PTm) B0 B1 U T :
U = subst_PTm (scons a0 VarPTm) B0 -> U = subst_PTm (scons a0 VarPTm) B0 ->
T = subst_PTm (scons a1 VarPTm) B1 -> T = subst_PTm (scons a1 VarPTm) B1 ->
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
@ -160,64 +160,61 @@ Lemma Su_Sig_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
Γ ⊢ U ≲ T. Γ ⊢ U ≲ T.
Proof. move => -> ->. apply Su_Sig_Proj2. Qed. Proof. move => -> ->. apply Su_Sig_Proj2. Qed.
Lemma E_IndZero' n Γ P i (b : PTm n) c U : Lemma E_IndZero' Γ P i (b : PTm) c U :
U = subst_PTm (scons PZero VarPTm) P -> U = subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> cons PNat Γ ⊢ P ∈ PUniv i ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> cons P (cons PNat Γ) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P PZero b c ≡ b ∈ U. Γ ⊢ PInd P PZero b c ≡ b ∈ U.
Proof. move => ->. apply E_IndZero. Qed. Proof. move => ->. apply E_IndZero. Qed.
Lemma Wff_Cons' n Γ (A : PTm n) i : Lemma Wff_Cons' Γ (A : PTm) i :
Γ ⊢ A ∈ PUniv i -> Γ ⊢ A ∈ PUniv i ->
(* -------------------------------- *) (* -------------------------------- *)
⊢ funcomp (ren_PTm shift) (scons A Γ). ⊢ cons A Γ.
Proof. hauto lq:on rew:off use:Wff_Cons, wff_mutual. Qed. Proof. hauto lq:on rew:off use:Wff_Cons, wff_mutual. Qed.
Lemma E_IndSuc' s Γ P (a : PTm s) b c i u U : Lemma E_IndSuc' Γ P (a : PTm) b c i u U :
u = subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c -> u = subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c ->
U = subst_PTm (scons (PSuc a) VarPTm) P -> U = subst_PTm (scons (PSuc a) VarPTm) P ->
funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i -> cons PNat Γ ⊢ P ∈ PUniv i ->
Γ ⊢ a ∈ PNat -> Γ ⊢ a ∈ PNat ->
Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
Γ ⊢ PInd P (PSuc a) b c ≡ u ∈ U. Γ ⊢ PInd P (PSuc a) b c ≡ u ∈ U.
Proof. move => ->->. apply E_IndSuc. Qed. Proof. move => ->->. apply E_IndSuc. Qed.
Lemma renaming : Lemma renaming :
(forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\ (forall Γ, ⊢ Γ -> True) /\
(forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ -> (forall Γ (a A : PTm), Γ ⊢ a ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\ Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\
(forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ -> (forall Γ (a b A : PTm), Γ ⊢ a ≡ b ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A) /\ Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A) /\
(forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ -> (forall Γ (A B : PTm), Γ ⊢ A ≲ B -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ ->
Δ ⊢ ren_PTm ξ A ≲ ren_PTm ξ B). Δ ⊢ ren_PTm ξ A ≲ ren_PTm ξ B).
Proof. Proof.
apply wt_mutual => //=; eauto 3 with wt. apply wt_mutual => //=; eauto 3 with wt.
- move => n Γ i hΓ _ m Δ ξ hΔ hξ.
rewrite hξ.
by apply T_Var.
- hauto lq:on rew:off ctrs:Wt, Wff use:renaming_up. - hauto lq:on rew:off ctrs:Wt, Wff use:renaming_up.
- move => n Γ a A B i hP ihP ha iha m Δ ξ hΔ hξ. - move => Γ a A B i hP ihP ha iha Δ ξ hΔ hξ.
apply : T_Abs; eauto. apply : T_Abs; eauto.
move : ihP(hΔ) (hξ); repeat move/[apply]. move/Bind_Inv. move : ihP(hΔ) (hξ); repeat move/[apply]. move/Bind_Inv.
hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up. hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up.
- move => *. apply : T_App'; eauto. by asimpl. - move => *. apply : T_App'; eauto. by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ξ hξ hΔ. - move => Γ a A b B i hA ihA hB ihB hS ihS Δ ξ hξ hΔ.
eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl. eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
- move => n Γ a A B ha iha m Δ ξ hΔ hξ. apply : T_Proj2'; eauto. by asimpl. - move => Γ a A B ha iha Δ ξ hΔ hξ. apply : T_Proj2'; eauto. by asimpl.
- move => s Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
move => [:hP]. move => [:hP].
apply : T_Ind'; eauto. by asimpl. apply : T_Ind'; eauto. by asimpl.
abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'. abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'.
hauto l:on use:renaming_up. hauto l:on use:renaming_up.
set x := subst_PTm _ _. have -> : x = ren_PTm ξ (subst_PTm (scons PZero VarPTm) P) by subst x; asimpl. set x := subst_PTm _ _. have -> : x = ren_PTm ξ (subst_PTm (scons PZero VarPTm) P) by subst x; asimpl.
by subst x; eauto. by subst x; eauto.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ. subst Ξ. have hΞ : ⊢ Ξ. subst Ξ.
apply : Wff_Cons'; eauto. apply hP. apply : Wff_Cons'; eauto. apply hP.
move /(_ _ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
set Ξ' := (funcomp _ _ : fin (S (S _)) -> _) . set Ξ' := (cons _ _) .
have : renaming_ok Ξ Ξ' (upRen_PTm_PTm (upRen_PTm_PTm ξ)). have : renaming_ok Ξ Ξ' (upRen_PTm_PTm (upRen_PTm_PTm ξ)).
by do 2 apply renaming_up. by do 2 apply renaming_up.
move /[swap] /[apply]. move /[swap] /[apply].
@ -225,31 +222,33 @@ Proof.
- hauto lq:on ctrs:Wt,LEq. - hauto lq:on ctrs:Wt,LEq.
- hauto lq:on ctrs:Eq. - hauto lq:on ctrs:Eq.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up. - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ξ hΔ hξ. - move => Γ a b A B i hPi ihPi ha iha Δ ξ hΔ hξ.
move : ihPi (hΔ) (hξ). repeat move/[apply]. move : ihPi (hΔ) (hξ). repeat move/[apply].
move => /Bind_Inv [j][h0][h1]h2. move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
move {hPi}. move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up. apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up.
- move => *. apply : E_App'; eauto. by asimpl. - move => *. apply : E_App'; eauto. by asimpl.
- move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ξ hΔ hξ. - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ξ hΔ hξ.
apply : E_Pair; eauto. apply : E_Pair; eauto.
move : ihb hΔ hξ. repeat move/[apply]. move : ihb hΔ hξ. repeat move/[apply].
by asimpl. by asimpl.
- move => *. apply : E_Proj2'; eauto. by asimpl. - move => *. apply : E_Proj2'; eauto. by asimpl.
- move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc. - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
move => m Δ ξ hΔ hξ [:hP']. move => Δ ξ hΔ hξ [:hP' hren].
apply E_IndCong' with (i := i). apply E_IndCong' with (i := i); eauto with wt.
by asimpl. by asimpl.
apply ihP0.
abstract : hP'. abstract : hP'.
qauto l:on use:renaming_up, Wff_Cons', T_Nat'. qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
abstract : hren.
qauto l:on use:renaming_up, Wff_Cons', T_Nat'. qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
by eauto with wt. apply ihP; eauto with wt.
move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl. move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ. have hΞ : ⊢ Ξ.
subst Ξ. apply :Wff_Cons'; eauto. apply hP'. subst Ξ. apply :Wff_Cons'; eauto.
move /(_ _ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(qauto l:on use:renaming_up)). move /(_ ltac:(qauto l:on use:renaming_up)).
suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ)) suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
(ren_PTm shift (ren_PTm shift
@ -259,31 +258,33 @@ Proof.
(ren_PTm (upRen_PTm_PTm ξ) P0)) by scongruence. (ren_PTm (upRen_PTm_PTm ξ) P0)) by scongruence.
by asimpl. by asimpl.
- qauto l:on ctrs:Eq, LEq. - qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ξ hΔ hξ. - move => Γ a b A B i hP ihP hb ihb ha iha Δ ξ hΔ hξ.
move : ihP (hξ) (hΔ). repeat move/[apply]. move : ihP (hξ) (hΔ). repeat move/[apply].
move /Bind_Inv. move /Bind_Inv.
move => [j][h0][h1]h2. move => [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl. apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:renaming_up. hauto lq:on ctrs:Wff use:renaming_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ. - move => Γ a b A B i hP ihP ha iha hb ihb Δ ξ hΔ hξ.
move : {hP} ihP (hξ) (hΔ). repeat move/[apply]. move : {hP} ihP (hξ) (hΔ). repeat move/[apply].
move /Bind_Inv => [i0][h0][h1]h2. move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ ⊢ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto. apply : E_ProjPair1; eauto.
move : ihb hξ hΔ. repeat move/[apply]. by asimpl. move : ihb hξ hΔ. repeat move/[apply]. by asimpl.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ. - move => Γ a b A B i hP ihP ha iha hb ihb Δ ξ hΔ hξ.
apply : E_ProjPair2'; eauto. by asimpl. apply : E_ProjPair2'; eauto. by asimpl.
move : ihb hξ hΔ; repeat move/[apply]. by asimpl. move : ihb hξ hΔ; repeat move/[apply]. by asimpl.
- move => n Γ P i b c hP ihP hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P i b c hP ihP hb ihb hc ihc Δ ξ hΔ hξ.
apply E_IndZero' with (i := i); eauto. by asimpl. apply E_IndZero' with (i := i); eauto. by asimpl.
qauto l:on use:Wff_Cons', T_Nat', renaming_up. sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ m Δ ξ hΔ) : ihb. move /(_ Δ ξ hΔ) : ihb.
asimpl. by apply. asimpl. by apply.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up. have hΞ : ⊢ Ξ by sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ _ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(qauto l:on use:renaming_up)). set p := renaming_ok _ _ _.
have : p. by do 2 apply renaming_up.
move => /[swap]/[apply].
suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ)) suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
(ren_PTm shift (ren_PTm shift
(subst_PTm (subst_PTm
@ -291,15 +292,15 @@ Proof.
(subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift)) (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift))
(ren_PTm (upRen_PTm_PTm ξ) P)) by scongruence. (ren_PTm (upRen_PTm_PTm ξ) P)) by scongruence.
by asimpl. by asimpl.
- move => n Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
apply E_IndSuc' with (i := i). by asimpl. by asimpl. apply E_IndSuc' with (i := i). by asimpl. by asimpl.
qauto l:on use:Wff_Cons', T_Nat', renaming_up. sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
by eauto with wt. by eauto with wt.
move /(_ m Δ ξ hΔ) : ihb. asimpl. by apply. move /(_ Δ ξ hΔ) : ihb. asimpl. by apply.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up. have hΞ : ⊢ Ξ by sauto lq:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ _ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(qauto l:on use:renaming_up)). move /(_ ltac:(by eauto using renaming_up)).
by asimpl. by asimpl.
- move => *. - move => *.
apply : E_AppEta'; eauto. by asimpl. apply : E_AppEta'; eauto. by asimpl.
@ -315,94 +316,94 @@ Proof.
- move => *. apply : Su_Sig_Proj2'; eauto; by asimpl. - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
Qed. Qed.
Definition morphing_ok {n m} Δ Γ (ρ : fin n -> PTm m) := Definition morphing_ok Δ Γ (ρ : nat -> PTm) :=
forall i, Δ ⊢ ρ i ∈ subst_PTm ρ (Γ i). forall i A, lookup i Γ A -> Δ ⊢ ρ i ∈ subst_PTm ρ A.
Lemma morphing_ren n m p Ξ Δ Γ Lemma morphing_ren Ξ Δ Γ
(ρ : fin n -> PTm m) (ξ : fin m -> fin p) : (ρ : nat -> PTm) (ξ : nat -> nat) :
⊢ Ξ -> ⊢ Ξ ->
renaming_ok Ξ Δ ξ -> morphing_ok Δ Γ ρ -> renaming_ok Ξ Δ ξ -> morphing_ok Δ Γ ρ ->
morphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ). morphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
Proof. Proof.
move => hΞ hξ hρ. move => hΞ hξ hρ i A.
move => i.
rewrite {1}/funcomp. rewrite {1}/funcomp.
have -> : have -> :
subst_PTm (funcomp (ren_PTm ξ) ρ) (Γ i) = subst_PTm (funcomp (ren_PTm ξ) ρ) A =
ren_PTm ξ (subst_PTm ρ (Γ i)) by asimpl. ren_PTm ξ (subst_PTm ρ A) by asimpl.
eapply renaming; eauto. move => ?. eapply renaming; eauto.
Qed. Qed.
Lemma morphing_ext n m Δ Γ (ρ : fin n -> PTm m) (a : PTm m) (A : PTm n) : Lemma morphing_ext Δ Γ (ρ : nat -> PTm) (a : PTm) (A : PTm) :
morphing_ok Δ Γ ρ -> morphing_ok Δ Γ ρ ->
Δ ⊢ a ∈ subst_PTm ρ A -> Δ ⊢ a ∈ subst_PTm ρ A ->
morphing_ok morphing_ok
Δ (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ). Δ (cons A Γ) (scons a ρ).
Proof. Proof.
move => h ha i. destruct i as [i|]; by asimpl. move => h ha i B.
elim /lookup_inv => //=_.
- move => A0 Γ0 ? [*]. subst.
by asimpl.
- move => i0 Γ0 A0 B0 h0 ? [*]. subst.
asimpl. by apply h.
Qed. Qed.
Lemma T_Var' n Γ (i : fin n) U : Lemma renaming_wt : forall Γ (a A : PTm), Γ ⊢ a ∈ A -> forall Δ (ξ : nat -> nat), ⊢ Δ -> renaming_ok Δ Γ ξ -> Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A.
U = Γ i ->
⊢ Γ ->
Γ ⊢ VarPTm i ∈ U.
Proof. move => ->. apply T_Var. Qed.
Lemma renaming_wt : forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ -> Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A.
Proof. sfirstorder use:renaming. Qed. Proof. sfirstorder use:renaming. Qed.
Lemma renaming_wt' : forall n m Δ Γ a A (ξ : fin n -> fin m) u U, Lemma renaming_wt' : forall Δ Γ a A (ξ : nat -> nat) u U,
u = ren_PTm ξ a -> U = ren_PTm ξ A -> u = ren_PTm ξ a -> U = ren_PTm ξ A ->
Γ ⊢ a ∈ A -> ⊢ Δ -> Γ ⊢ a ∈ A -> ⊢ Δ ->
renaming_ok Δ Γ ξ -> Δ ⊢ u ∈ U. renaming_ok Δ Γ ξ -> Δ ⊢ u ∈ U.
Proof. hauto use:renaming_wt. Qed. Proof. hauto use:renaming_wt. Qed.
Lemma morphing_up n m Γ Δ (ρ : fin n -> PTm m) (A : PTm n) k : Lemma morphing_up Γ Δ (ρ : nat -> PTm) (A : PTm) k :
morphing_ok Γ Δ ρ -> morphing_ok Γ Δ ρ ->
Γ ⊢ subst_PTm ρ A ∈ PUniv k -> Γ ⊢ subst_PTm ρ A ∈ PUniv k ->
morphing_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) (funcomp (ren_PTm shift) (scons A Δ)) (up_PTm_PTm ρ). morphing_ok (cons (subst_PTm ρ A) Γ) (cons A Δ) (up_PTm_PTm ρ).
Proof. Proof.
move => h h1 [:hp]. apply morphing_ext. move => h h1 [:hp]. apply morphing_ext.
rewrite /morphing_ok. rewrite /morphing_ok.
move => i. move => i A0 hA0.
rewrite {2}/funcomp. apply : renaming_wt'; last by apply renaming_shift.
apply : renaming_wt'; eauto. by asimpl. rewrite /funcomp. reflexivity.
2 : { eauto. }
by asimpl.
abstract : hp. qauto l:on ctrs:Wff use:wff_mutual. abstract : hp. qauto l:on ctrs:Wff use:wff_mutual.
eauto using renaming_shift. apply : T_Var;eauto. apply here'. by asimpl.
apply : T_Var';eauto. rewrite /funcomp. by asimpl.
Qed. Qed.
Lemma weakening_wt : forall n Γ (a A B : PTm n) i, Lemma weakening_wt : forall Γ (a A B : PTm) i,
Γ ⊢ B ∈ PUniv i -> Γ ⊢ B ∈ PUniv i ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
funcomp (ren_PTm shift) (scons B Γ) ⊢ ren_PTm shift a ∈ ren_PTm shift A. cons B Γ ⊢ ren_PTm shift a ∈ ren_PTm shift A.
Proof. Proof.
move => n Γ a A B i hB ha. move => Γ a A B i hB ha.
apply : renaming_wt'; eauto. apply : renaming_wt'; eauto.
apply : Wff_Cons'; eauto. apply : Wff_Cons'; eauto.
apply : renaming_shift; eauto. apply : renaming_shift; eauto.
Qed. Qed.
Lemma weakening_wt' : forall n Γ (a A B : PTm n) i U u, Lemma weakening_wt' : forall Γ (a A B : PTm) i U u,
u = ren_PTm shift a -> u = ren_PTm shift a ->
U = ren_PTm shift A -> U = ren_PTm shift A ->
Γ ⊢ B ∈ PUniv i -> Γ ⊢ B ∈ PUniv i ->
Γ ⊢ a ∈ A -> Γ ⊢ a ∈ A ->
funcomp (ren_PTm shift) (scons B Γ) ⊢ u ∈ U. cons B Γ ⊢ u ∈ U.
Proof. move => > -> ->. apply weakening_wt. Qed. Proof. move => > -> ->. apply weakening_wt. Qed.
Lemma morphing : Lemma morphing :
(forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\ (forall Γ, ⊢ Γ -> True) /\
(forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ -> (forall Γ a A, Γ ⊢ a ∈ A -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A) /\ Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A) /\
(forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ -> (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
Δ ⊢ subst_PTm ρ a ≡ subst_PTm ρ b ∈ subst_PTm ρ A) /\ Δ ⊢ subst_PTm ρ a ≡ subst_PTm ρ b ∈ subst_PTm ρ A) /\
(forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ -> (forall Γ A B, Γ ⊢ A ≲ B -> forall Δ ρ, ⊢ Δ -> morphing_ok Δ Γ ρ ->
Δ ⊢ subst_PTm ρ A ≲ subst_PTm ρ B). Δ ⊢ subst_PTm ρ A ≲ subst_PTm ρ B).
Proof. Proof.
apply wt_mutual => //=. apply wt_mutual => //=.
- hauto l:on unfold:morphing_ok.
- hauto lq:on use:morphing_up, Wff_Cons', T_Bind. - hauto lq:on use:morphing_up, Wff_Cons', T_Bind.
- move => n Γ a A B i hP ihP ha iha m Δ ρ hΔ hρ. - move => Γ a A B i hP ihP ha iha Δ ρ hΔ hρ.
move : ihP (hΔ) (hρ); repeat move/[apply]. move : ihP (hΔ) (hρ); repeat move/[apply].
move /Bind_Inv => [j][h0][h1]h2. move {hP}. move /Bind_Inv => [j][h0][h1]h2. move {hP}.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i by hauto lq:on ctrs:Wt. have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i by hauto lq:on ctrs:Wt.
@ -411,7 +412,7 @@ Proof.
hauto lq:on use:Wff_Cons', Bind_Inv. hauto lq:on use:Wff_Cons', Bind_Inv.
apply : morphing_up; eauto. apply : morphing_up; eauto.
- move => *; apply : T_App'; eauto; by asimpl. - move => *; apply : T_App'; eauto; by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ρ hρ hΔ. - move => Γ a A b B i hA ihA hB ihB hS ihS Δ ρ hρ hΔ.
eapply T_Pair' with (U := subst_PTm ρ (subst_PTm (scons a VarPTm) B));eauto. by asimpl. eapply T_Pair' with (U := subst_PTm ρ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
- hauto lq:on use:T_Proj1. - hauto lq:on use:T_Proj1.
- move => *. apply : T_Proj2'; eauto. by asimpl. - move => *. apply : T_Proj2'; eauto. by asimpl.
@ -419,9 +420,8 @@ Proof.
- qauto l:on ctrs:Wt. - qauto l:on ctrs:Wt.
- qauto l:on ctrs:Wt. - qauto l:on ctrs:Wt.
- qauto l:on ctrs:Wt. - qauto l:on ctrs:Wt.
- move => s Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
have hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ)) have hξ' : morphing_ok (cons PNat Δ) (cons PNat Γ) (up_PTm_PTm ξ).
(funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
move /morphing_up : hξ. move /(_ PNat 0). move /morphing_up : hξ. move /(_ PNat 0).
apply. by apply T_Nat. apply. by apply T_Nat.
move => [:hP]. move => [:hP].
@ -430,11 +430,11 @@ Proof.
move /morphing_up : hξ. move /(_ PNat 0). move /morphing_up : hξ. move /(_ PNat 0).
apply. by apply T_Nat. apply. by apply T_Nat.
move : ihb hξ hΔ; do!move/[apply]. by asimpl. move : ihb hξ hΔ; do!move/[apply]. by asimpl.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ. subst Ξ. have hΞ : ⊢ Ξ. subst Ξ.
apply : Wff_Cons'; eauto. apply hP. apply : Wff_Cons'; eauto. apply hP.
move /(_ _ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
set Ξ' := (funcomp _ _ : fin (S (S _)) -> _) . set Ξ' := (cons _ _) .
have : morphing_ok Ξ Ξ' (up_PTm_PTm (up_PTm_PTm ξ)). have : morphing_ok Ξ Ξ' (up_PTm_PTm (up_PTm_PTm ξ)).
eapply morphing_up; eauto. apply hP. eapply morphing_up; eauto. apply hP.
move /[swap]/[apply]. move /[swap]/[apply].
@ -447,23 +447,23 @@ Proof.
- hauto lq:on ctrs:Eq. - hauto lq:on ctrs:Eq.
- hauto lq:on ctrs:Eq. - hauto lq:on ctrs:Eq.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up. - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ρ hΔ hρ. - move => Γ a b A B i hPi ihPi ha iha Δ ρ hΔ hρ.
move : ihPi (hΔ) (hρ). repeat move/[apply]. move : ihPi (hΔ) (hρ). repeat move/[apply].
move => /Bind_Inv [j][h0][h1]h2. move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
move {hPi}. move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up. apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up.
- move => *. apply : E_App'; eauto. by asimpl. - move => *. apply : E_App'; eauto. by asimpl.
- move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ρ hΔ hρ. - move => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ρ hΔ hρ.
apply : E_Pair; eauto. apply : E_Pair; eauto.
move : ihb hΔ hρ. repeat move/[apply]. move : ihb hΔ hρ. repeat move/[apply].
by asimpl. by asimpl.
- hauto q:on ctrs:Eq. - hauto q:on ctrs:Eq.
- move => *. apply : E_Proj2'; eauto. by asimpl. - move => *. apply : E_Proj2'; eauto. by asimpl.
- move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc. - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
move => m Δ ξ hΔ hξ. move => Δ ξ hΔ hξ.
have hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ)) have hξ' : morphing_ok (cons PNat Δ)
(funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ). (cons PNat Γ) (up_PTm_PTm ξ).
move /morphing_up : hξ. move /(_ PNat 0). move /morphing_up : hξ. move /(_ PNat 0).
apply. by apply T_Nat. apply. by apply T_Nat.
move => [:hP']. move => [:hP'].
@ -474,56 +474,54 @@ Proof.
qauto l:on use:renaming_up, Wff_Cons', T_Nat'. qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
by eauto with wt. by eauto with wt.
move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl. move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ. have hΞ : ⊢ Ξ.
subst Ξ. apply :Wff_Cons'; eauto. apply hP'. subst Ξ. apply :Wff_Cons'; eauto. apply hP'.
move /(_ _ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(qauto l:on use:morphing_up)). move /(_ ltac:(qauto l:on use:morphing_up)).
asimpl. substify. by asimpl. asimpl. substify. by asimpl.
- eauto with wt. - eauto with wt.
- qauto l:on ctrs:Eq, LEq. - qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ρ hΔ hρ. - move => Γ a b A B i hP ihP hb ihb ha iha Δ ρ hΔ hρ.
move : ihP (hρ) (hΔ). repeat move/[apply]. move : ihP (hρ) (hΔ). repeat move/[apply].
move /Bind_Inv. move /Bind_Inv.
move => [j][h0][h1]h2. move => [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl. apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:morphing_up. hauto lq:on ctrs:Wff use:morphing_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ. - move => Γ a b A B i hP ihP ha iha hb ihb Δ ρ hΔ hρ.
move : {hP} ihP (hρ) (hΔ). repeat move/[apply]. move : {hP} ihP (hρ) (hΔ). repeat move/[apply].
move /Bind_Inv => [i0][h0][h1]h2. move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ ⊢ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt. have ? : Δ ⊢ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto. apply : E_ProjPair1; eauto.
move : ihb hρ hΔ. repeat move/[apply]. by asimpl. move : ihb hρ hΔ. repeat move/[apply]. by asimpl.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ. - move => Γ a b A B i hP ihP ha iha hb ihb Δ ρ hΔ hρ.
apply : E_ProjPair2'; eauto. by asimpl. apply : E_ProjPair2'; eauto. by asimpl.
move : ihb hρ hΔ; repeat move/[apply]. by asimpl. move : ihb hρ hΔ; repeat move/[apply]. by asimpl.
- move => n Γ P i b c hP ihP hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P i b c hP ihP hb ihb hc ihc Δ ξ hΔ hξ.
have hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ)) have hξ' : morphing_ok (cons PNat Δ)(cons PNat Γ) (up_PTm_PTm ξ).
(funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
move /morphing_up : hξ. move /(_ PNat 0). move /morphing_up : hξ. move /(_ PNat 0).
apply. by apply T_Nat. apply. by apply T_Nat.
apply E_IndZero' with (i := i); eauto. by asimpl. apply E_IndZero' with (i := i); eauto. by asimpl.
qauto l:on use:Wff_Cons', T_Nat', renaming_up. qauto l:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ m Δ ξ hΔ) : ihb. move /(_ Δ ξ hΔ) : ihb.
asimpl. by apply. asimpl. by apply.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up. have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ _ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(sauto lq:on use:morphing_up)). move /(_ ltac:(sauto lq:on use:morphing_up)).
asimpl. substify. by asimpl. asimpl. substify. by asimpl.
- move => n Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ. - move => Γ P a b c i hP ihP ha iha hb ihb hc ihc Δ ξ hΔ hξ.
have hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ)) have hξ' : morphing_ok (cons PNat Δ) (cons PNat Γ) (up_PTm_PTm ξ).
(funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
move /morphing_up : hξ. move /(_ PNat 0). move /morphing_up : hξ. move /(_ PNat 0).
apply. by apply T_Nat'. apply. by apply T_Nat'.
apply E_IndSuc' with (i := i). by asimpl. by asimpl. apply E_IndSuc' with (i := i). by asimpl. by asimpl.
qauto l:on use:Wff_Cons', T_Nat', renaming_up. qauto l:on use:Wff_Cons', T_Nat', renaming_up.
by eauto with wt. by eauto with wt.
move /(_ m Δ ξ hΔ) : ihb. asimpl. by apply. move /(_ Δ ξ hΔ) : ihb. asimpl. by apply.
set Ξ := funcomp _ _. set Ξ := cons _ _.
have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up. have hΞ : ⊢ Ξ by qauto l:on use:Wff_Cons', T_Nat', renaming_up.
move /(_ _ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc. move /(_ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
move /(_ ltac:(sauto l:on use:morphing_up)). move /(_ ltac:(sauto l:on use:morphing_up)).
asimpl. substify. by asimpl. asimpl. substify. by asimpl.
- move => *. - move => *.
@ -540,40 +538,39 @@ Proof.
- move => *. apply : Su_Sig_Proj2'; eauto; by asimpl. - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
Qed. Qed.
Lemma morphing_wt : forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ -> Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A. Lemma morphing_wt : forall Γ (a A : PTm ), Γ ⊢ a ∈ A -> forall Δ (ρ : nat -> PTm), ⊢ Δ -> morphing_ok Δ Γ ρ -> Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A.
Proof. sfirstorder use:morphing. Qed. Proof. sfirstorder use:morphing. Qed.
Lemma morphing_wt' : forall n m Δ Γ a A (ρ : fin n -> PTm m) u U, Lemma morphing_wt' : forall Δ Γ a A (ρ : nat -> PTm) u U,
u = subst_PTm ρ a -> U = subst_PTm ρ A -> u = subst_PTm ρ a -> U = subst_PTm ρ A ->
Γ ⊢ a ∈ A -> ⊢ Δ -> Γ ⊢ a ∈ A -> ⊢ Δ ->
morphing_ok Δ Γ ρ -> Δ ⊢ u ∈ U. morphing_ok Δ Γ ρ -> Δ ⊢ u ∈ U.
Proof. hauto use:morphing_wt. Qed. Proof. hauto use:morphing_wt. Qed.
Lemma morphing_id : forall n (Γ : fin n -> PTm n), ⊢ Γ -> morphing_ok Γ Γ VarPTm. Lemma morphing_id : forall Γ, ⊢ Γ -> morphing_ok Γ Γ VarPTm.
Proof. Proof.
move => n Γ hΓ. rewrite /morphing_ok => Γ hΓ i. asimpl.
rewrite /morphing_ok. eauto using T_Var.
move => i. asimpl. by apply T_Var.
Qed. Qed.
Lemma substing_wt : forall n Γ (a : PTm (S n)) (b A : PTm n) B, Lemma substing_wt : forall Γ (a : PTm) (b A : PTm) B,
funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B -> (cons A Γ) ⊢ a ∈ B ->
Γ ⊢ b ∈ A -> Γ ⊢ b ∈ A ->
Γ ⊢ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm) B. Γ ⊢ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm) B.
Proof. Proof.
move => n Γ a b A B ha hb [:hΓ]. apply : morphing_wt; eauto. move => Γ a b A B ha hb [:hΓ]. apply : morphing_wt; eauto.
abstract : hΓ. sfirstorder use:wff_mutual. abstract : hΓ. sfirstorder use:wff_mutual.
apply morphing_ext; last by asimpl. apply morphing_ext; last by asimpl.
by apply morphing_id. by apply morphing_id.
Qed. Qed.
(* Could generalize to all equal contexts *) (* Could generalize to all equal contexts *)
Lemma ctx_eq_subst_one n (A0 A1 : PTm n) i j Γ a A : Lemma ctx_eq_subst_one (A0 A1 : PTm) i j Γ a A :
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ a ∈ A -> (cons A0 Γ) ⊢ a ∈ A ->
Γ ⊢ A0 ∈ PUniv i -> Γ ⊢ A0 ∈ PUniv i ->
Γ ⊢ A1 ∈ PUniv j -> Γ ⊢ A1 ∈ PUniv j ->
Γ ⊢ A1 ≲ A0 -> Γ ⊢ A1 ≲ A0 ->
funcomp (ren_PTm shift) (scons A1 Γ) ⊢ a ∈ A. (cons A1 Γ) ⊢ a ∈ A.
Proof. Proof.
move => h0 h1 h2 h3. move => h0 h1 h2 h3.
replace a with (subst_PTm VarPTm a); last by asimpl. replace a with (subst_PTm VarPTm a); last by asimpl.
@ -581,22 +578,23 @@ Proof.
have ? : ⊢ Γ by sfirstorder use:wff_mutual. have ? : ⊢ Γ by sfirstorder use:wff_mutual.
apply : morphing_wt; eauto. apply : morphing_wt; eauto.
apply : Wff_Cons'; eauto. apply : Wff_Cons'; eauto.
move => k. destruct k as [k|]. move => k A2. elim/lookup_inv => //=_; cycle 1.
- asimpl. - move => i0 Γ0 A3 B hi ? [*]. subst.
eapply weakening_wt' with (a := VarPTm k);eauto using T_Var. asimpl.
eapply weakening_wt' with (a := VarPTm i0);eauto using T_Var.
by substify. by substify.
- move => [:hΓ']. - move => A3 Γ0 ? [*]. subst.
move => [:hΓ'].
apply : T_Conv. apply : T_Conv.
apply T_Var. apply T_Var.
abstract : hΓ'. abstract : hΓ'.
eauto using Wff_Cons'. eauto using Wff_Cons'. apply here.
rewrite /funcomp. asimpl. substify. asimpl. asimpl. renamify.
renamify.
eapply renaming; eauto. eapply renaming; eauto.
apply : renaming_shift; eauto. apply : renaming_shift; eauto.
Qed. Qed.
Lemma bind_inst n Γ p (A : PTm n) B i a0 a1 : Lemma bind_inst Γ p (A : PTm) B i a0 a1 :
Γ ⊢ PBind p A B ∈ PUniv i -> Γ ⊢ PBind p A B ∈ PUniv i ->
Γ ⊢ a0 ≡ a1 ∈ A -> Γ ⊢ a0 ≡ a1 ∈ A ->
Γ ⊢ subst_PTm (scons a0 VarPTm) B ≲ subst_PTm (scons a1 VarPTm) B. Γ ⊢ subst_PTm (scons a0 VarPTm) B ≲ subst_PTm (scons a1 VarPTm) B.
@ -606,7 +604,7 @@ Proof.
case : p h => //=; hauto l:on use:Su_Pi_Proj2, Su_Sig_Proj2. case : p h => //=; hauto l:on use:Su_Pi_Proj2, Su_Sig_Proj2.
Qed. Qed.
Lemma Cumulativity n Γ (a : PTm n) i j : Lemma Cumulativity Γ (a : PTm ) i j :
i <= j -> i <= j ->
Γ ⊢ a ∈ PUniv i -> Γ ⊢ a ∈ PUniv i ->
Γ ⊢ a ∈ PUniv j. Γ ⊢ a ∈ PUniv j.
@ -616,9 +614,9 @@ Proof.
sfirstorder use:wff_mutual. sfirstorder use:wff_mutual.
Qed. Qed.
Lemma T_Bind' n Γ i j p (A : PTm n) (B : PTm (S n)) : Lemma T_Bind' Γ i j p (A : PTm ) (B : PTm) :
Γ ⊢ A ∈ PUniv i -> Γ ⊢ A ∈ PUniv i ->
funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv j -> (cons A Γ) ⊢ B ∈ PUniv j ->
Γ ⊢ PBind p A B ∈ PUniv (max i j). Γ ⊢ PBind p A B ∈ PUniv (max i j).
Proof. Proof.
move => h0 h1. move => h0 h1.
@ -629,47 +627,48 @@ Qed.
Hint Resolve T_Bind' : wt. Hint Resolve T_Bind' : wt.
Lemma regularity : Lemma regularity :
(forall n (Γ : fin n -> PTm n), ⊢ Γ -> forall i, exists j, Γ ⊢ Γ i ∈ PUniv j) /\ (forall Γ, ⊢ Γ -> forall i A, lookup i Γ A -> exists j, Γ ⊢ A ∈ PUniv j) /\
(forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> exists i, Γ ⊢ A ∈ PUniv i) /\ (forall Γ a A, Γ ⊢ a ∈ A -> exists i, Γ ⊢ A ∈ PUniv i) /\
(forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ A /\ exists i, Γ ⊢ A ∈ PUniv i) /\ (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ A /\ exists i, Γ ⊢ A ∈ PUniv i) /\
(forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i /\ Γ ⊢ B ∈ PUniv i). (forall Γ A B, Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i /\ Γ ⊢ B ∈ PUniv i).
Proof. Proof.
apply wt_mutual => //=; eauto with wt. apply wt_mutual => //=; eauto with wt.
- move => n Γ A i hΓ ihΓ hA _ j. - move => i A. elim/lookup_inv => //=_.
destruct j as [j|]. - move => Γ A i hΓ ihΓ hA _ j A0.
have := ihΓ j. elim /lookup_inv => //=_; cycle 1.
move => [j0 hj]. + move => i0 Γ0 A1 B + ? [*]. subst.
exists j0. apply : renaming_wt' => //=; eauto using renaming_shift. move : ihΓ => /[apply]. move => [j hA1].
reflexivity. econstructor; eauto. exists j. apply : renaming_wt' => //=; eauto using renaming_shift. done.
exists i. rewrite {2}/funcomp. simpl. apply : Wff_Cons'; eauto.
apply : renaming_wt'; eauto. reflexivity. + move => A1 Γ0 ? [*]. subst.
exists i. apply : renaming_wt'; eauto. reflexivity.
econstructor; eauto. econstructor; eauto.
apply : renaming_shift; eauto. apply : renaming_shift; eauto.
- move => n Γ b a A B hb [i ihb] ha [j iha]. - move => Γ b a A B hb [i ihb] ha [j iha].
move /Bind_Inv : ihb => [k][h0][h1]h2. move /Bind_Inv : ihb => [k][h0][h1]h2.
move : substing_wt ha h1; repeat move/[apply]. move : substing_wt ha h1; repeat move/[apply].
move => h. exists k. move => h. exists k.
move : h. by asimpl. move : h. by asimpl.
- hauto lq:on use:Bind_Inv. - hauto lq:on use:Bind_Inv.
- move => n Γ a A B ha [i /Bind_Inv[j][h0][h1]h2]. - move => Γ a A B ha [i /Bind_Inv[j][h0][h1]h2].
exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1. exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1.
move : substing_wt h1; repeat move/[apply]. move : substing_wt h1; repeat move/[apply].
by asimpl. by asimpl.
- move => s Γ P a b c i + ? + *. clear. move => h ha. exists i. - move => Γ P a b c i + ? + *. clear. move => h ha. exists i.
hauto lq:on use:substing_wt. hauto lq:on use:substing_wt.
- sfirstorder. - sfirstorder.
- sfirstorder. - sfirstorder.
- sfirstorder. - sfirstorder.
- move => n Γ i p A0 A1 B0 B1 hΓ ihΓ hA0 - move => Γ i p A0 A1 B0 B1 hΓ ihΓ hA0
[i0 ihA0] hA [ihA [ihA' [i1 ihA'']]]. [i0 ihA0] hA [ihA [ihA' [i1 ihA'']]].
move => hB [ihB0 [ihB1 [i2 ihB2]]].
repeat split => //=. repeat split => //=.
qauto use:T_Bind. qauto use:T_Bind.
apply T_Bind; eauto. apply T_Bind; eauto.
sfirstorder.
apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric. apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
eauto using T_Univ. hauto lq:on.
- hauto lq:on ctrs:Wt,Eq. - hauto lq:on ctrs:Wt,Eq.
- move => n Γ i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]] - move => n i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]]
ha [iha0 [iha1 [i1 iha2]]]. ha [iha0 [iha1 [i1 iha2]]].
repeat split. repeat split.
qauto use:T_App. qauto use:T_App.
@ -680,15 +679,16 @@ Proof.
hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt. hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt.
- hauto lq:on use:bind_inst db:wt. - hauto lq:on use:bind_inst db:wt.
- hauto lq:on use:Bind_Inv db:wt. - hauto lq:on use:Bind_Inv db:wt.
- move => n Γ i a b A B hS _ hab [iha][ihb][j]ihs. - move => Γ i a b A B hS _ hab [iha][ihb][j]ihs.
repeat split => //=; eauto with wt. repeat split => //=; eauto with wt.
apply : T_Conv; eauto with wt. apply : T_Conv; eauto with wt.
move /E_Symmetric /E_Proj1 in hab. move /E_Symmetric /E_Proj1 in hab.
eauto using bind_inst. eauto using bind_inst.
move /T_Proj1 in iha. move /T_Proj1 in iha.
hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt. hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
- move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i _ _ hPE [hP0 [hP1 _]] hae [ha0 [ha1 _]] _ [hb0 [hb1 hb2]] _ [hc0 [hc1 hc2]]. - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i _ _ hPE [hP0 [hP1 _]] hae [ha0 [ha1 _]] _ [hb0 [hb1 hb2]] _ [hc0 [hc1 [j hc2]]].
have wfΓ : ⊢ Γ by hauto use:wff_mutual. have wfΓ : ⊢ Γ by hauto use:wff_mutual.
have wfΓ' : ⊢ (PNat :: Γ) by qauto use:Wff_Cons', T_Nat'.
repeat split. by eauto using T_Ind. repeat split. by eauto using T_Ind.
apply : T_Conv. apply : T_Ind; eauto. apply : T_Conv. apply : T_Ind; eauto.
apply : T_Conv; eauto. apply : T_Conv; eauto.
@ -696,13 +696,12 @@ Proof.
apply : T_Conv. apply : ctx_eq_subst_one; eauto. apply : T_Conv. apply : ctx_eq_subst_one; eauto.
by eauto using Su_Eq, E_Symmetric. by eauto using Su_Eq, E_Symmetric.
eapply renaming; eauto. eapply renaming; eauto.
eapply morphing; eauto 20 using Su_Eq, morphing_ext, morphing_id with wt. eapply morphing. apply : Su_Eq. apply hPE. apply wfΓ'.
apply morphing_ext; eauto. apply morphing_ext.
replace (funcomp VarPTm shift) with (funcomp (@ren_PTm n _ shift) VarPTm); last by asimpl. replace (funcomp VarPTm shift) with (funcomp (@ren_PTm shift) VarPTm); last by asimpl.
apply : morphing_ren; eauto using Wff_Cons' with wt. apply : morphing_ren; eauto using morphing_id, renaming_shift.
apply : renaming_shift; eauto. by apply morphing_id. apply T_Suc. apply T_Var=>//. apply here. apply : Wff_Cons'; eauto using T_Nat'.
apply T_Suc. apply T_Var'. by asimpl. apply : Wff_Cons'; eauto using T_Nat'. apply renaming_shift.
apply : Wff_Cons'; eauto. apply : renaming_shift; eauto.
have /E_Symmetric /Su_Eq : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv i by eauto with wt. have /E_Symmetric /Su_Eq : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv i by eauto with wt.
move /E_Symmetric in hae. move /E_Symmetric in hae.
by eauto using Su_Sig_Proj2. by eauto using Su_Sig_Proj2.
@ -711,62 +710,62 @@ Proof.
- hauto lq:on ctrs:Wt. - hauto lq:on ctrs:Wt.
- hauto q:on use:substing_wt db:wt. - hauto q:on use:substing_wt db:wt.
- hauto l:on use:bind_inst db:wt. - hauto l:on use:bind_inst db:wt.
- move => n Γ P i b c hP _ hb _ hc _. - move => Γ P i b c hP _ hb _ hc _.
have ? : ⊢ Γ by hauto use:wff_mutual. have ? : ⊢ Γ by hauto use:wff_mutual.
repeat split=>//. repeat split=>//.
by eauto with wt. by eauto with wt.
sauto lq:on use:substing_wt. sauto lq:on use:substing_wt.
- move => s Γ P a b c i hP _ ha _ hb _ hc _. - move => Γ P a b c i hP _ ha _ hb _ hc _.
have ? : ⊢ Γ by hauto use:wff_mutual. have ? : ⊢ Γ by hauto use:wff_mutual.
repeat split=>//. repeat split=>//.
apply : T_Ind; eauto with wt. apply : T_Ind; eauto with wt.
set Ξ : fin (S (S _)) -> _ := (X in X ⊢ _ ∈ _) in hc. set Ξ := (X in X ⊢ _ ∈ _) in hc.
have : morphing_ok Γ Ξ (scons (PInd P a b c) (scons a VarPTm)). have : morphing_ok Γ Ξ (scons (PInd P a b c) (scons a VarPTm)).
apply morphing_ext. apply morphing_ext. by apply morphing_id. apply morphing_ext. apply morphing_ext. by apply morphing_id.
by eauto. by eauto with wt. by eauto. by eauto with wt.
subst Ξ. subst Ξ.
move : morphing_wt hc; repeat move/[apply]. asimpl. by apply. move : morphing_wt hc; repeat move/[apply]. asimpl. by apply.
sauto lq:on use:substing_wt. sauto lq:on use:substing_wt.
- move => n Γ b A B i hΓ ihΓ hP _ hb [i0 ihb]. - move => Γ b A B i hP _ hb [i0 ihb].
repeat split => //=; eauto with wt. repeat split => //=; eauto with wt.
have {}hb : funcomp (ren_PTm shift) (scons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B) have {}hb : (cons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B)
by hauto lq:on use:weakening_wt, Bind_Inv. by hauto lq:on use:weakening_wt, Bind_Inv.
apply : T_Abs; eauto. apply : T_Abs; eauto.
apply : T_App'; eauto; rewrite-/ren_PTm. apply : T_App'; eauto; rewrite-/ren_PTm. asimpl. by rewrite subst_scons_id.
by asimpl.
apply T_Var. sfirstorder use:wff_mutual. apply T_Var. sfirstorder use:wff_mutual.
apply here.
- hauto lq:on ctrs:Wt. - hauto lq:on ctrs:Wt.
- move => n Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]]. - move => Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
have ? : ⊢ Γ by sfirstorder use:wff_mutual. have ? : ⊢ Γ by sfirstorder use:wff_mutual.
exists (max i j). exists (max i j).
have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia. have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia.
qauto l:on use:T_Conv, Su_Univ. qauto l:on use:T_Conv, Su_Univ.
- move => n Γ i j hΓ *. exists (S (max i j)). - move => Γ i j hΓ *. exists (S (max i j)).
have [? ?] : S i <= S (Nat.max i j) /\ S j <= S (Nat.max i j) by lia. have [? ?] : S i <= S (Nat.max i j) /\ S j <= S (Nat.max i j) by lia.
hauto lq:on ctrs:Wt,LEq. hauto lq:on ctrs:Wt,LEq.
- move => n Γ A0 A1 B0 B1 i hΓ ihΓ hA0 _ hA1 [i0][ih0]ih1 hB[j0][ihB0]ihB1. - move => Γ A0 A1 B0 B1 i hA0 _ hA1 [i0][ih0]ih1 hB[j0][ihB0]ihB1.
exists (max i0 j0). exists (max i0 j0).
split; eauto with wt. split; eauto with wt.
apply T_Bind'; eauto. apply T_Bind'; eauto.
sfirstorder use:ctx_eq_subst_one. sfirstorder use:ctx_eq_subst_one.
- move => n Γ A0 A1 B0 B1 i hΓ ihΓ hA1 _ hA0 [i0][ihA0]ihA1 hB[i1][ihB0]ihB1. - move => n A0 A1 B0 B1 i hA1 _ hA0 [i0][ihA0]ihA1 hB[i1][ihB0]ihB1.
exists (max i0 i1). repeat split; eauto with wt. exists (max i0 i1). repeat split; eauto with wt.
apply T_Bind'; eauto. apply T_Bind'; eauto.
sfirstorder use:ctx_eq_subst_one. sfirstorder use:ctx_eq_subst_one.
- sfirstorder. - sfirstorder.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1]. - move => Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Bind_Inv : ih0 => [i0][h _]. move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _]. move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1). exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia. have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity. eauto using Cumulativity.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1]. - move => Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Bind_Inv : ih0 => [i0][h _]. move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _]. move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1). exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia. have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity. eauto using Cumulativity.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1. - move => Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1.
move => [i][ihP0]ihP1. move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1. move => ha [iha0][iha1][j]ihA1.
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _]. move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
@ -779,7 +778,7 @@ Proof.
move : substing_wt ih0';repeat move/[apply]. by asimpl. move : substing_wt ih0';repeat move/[apply]. by asimpl.
+ apply Cumulativity with (i := i1); eauto. + apply Cumulativity with (i := i1); eauto.
move : substing_wt ih1' iha1;repeat move/[apply]. by asimpl. move : substing_wt ih1' iha1;repeat move/[apply]. by asimpl.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1. - move => Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1.
move => [i][ihP0]ihP1. move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1. move => ha [iha0][iha1][j]ihA1.
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _]. move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
@ -795,23 +794,25 @@ Proof.
Unshelve. all: exact 0. Unshelve. all: exact 0.
Qed. Qed.
Lemma Var_Inv n Γ (i : fin n) A : Lemma Var_Inv Γ (i : nat) B A :
Γ ⊢ VarPTm i ∈ A -> Γ ⊢ VarPTm i ∈ A ->
⊢ Γ /\ Γ ⊢ Γ i ≲ A. lookup i Γ B ->
⊢ Γ /\ Γ ⊢ B ≲ A.
Proof. Proof.
move E : (VarPTm i) => u hu. move E : (VarPTm i) => u hu.
move : i E. move : i E.
elim : n Γ u A / hu=>//=. elim : Γ u A / hu=>//=.
- move => n Γ i hΓ i0 [?]. subst. - move => i Γ A hΓ hi i0 [?]. subst.
repeat split => //=. repeat split => //=.
have h : Γ ⊢ VarPTm i ∈ Γ i by eauto using T_Var. have ? : A = B by eauto using lookup_deter. subst.
have h : Γ ⊢ VarPTm i ∈ B by eauto using T_Var.
eapply regularity in h. eapply regularity in h.
move : h => [i0]?. move : h => [i0]?.
apply : Su_Eq. apply E_Refl; eassumption. apply : Su_Eq. apply E_Refl; eassumption.
- sfirstorder use:Su_Transitive. - sfirstorder use:Su_Transitive.
Qed. Qed.
Lemma renaming_su' : forall n m Δ Γ (ξ : fin n -> fin m) (A B : PTm n) u U , Lemma renaming_su' : forall Δ Γ ξ (A B : PTm) u U ,
u = ren_PTm ξ A -> u = ren_PTm ξ A ->
U = ren_PTm ξ B -> U = ren_PTm ξ B ->
Γ ⊢ A ≲ B -> Γ ⊢ A ≲ B ->
@ -819,23 +820,23 @@ Lemma renaming_su' : forall n m Δ Γ (ξ : fin n -> fin m) (A B : PTm n) u U ,
Δ ⊢ u ≲ U. Δ ⊢ u ≲ U.
Proof. move => > -> ->. hauto l:on use:renaming. Qed. Proof. move => > -> ->. hauto l:on use:renaming. Qed.
Lemma weakening_su : forall n Γ (A0 A1 B : PTm n) i, Lemma weakening_su : forall Γ (A0 A1 B : PTm) i,
Γ ⊢ B ∈ PUniv i -> Γ ⊢ B ∈ PUniv i ->
Γ ⊢ A0 ≲ A1 -> Γ ⊢ A0 ≲ A1 ->
funcomp (ren_PTm shift) (scons B Γ) ⊢ ren_PTm shift A0 ≲ ren_PTm shift A1. (cons B Γ) ⊢ ren_PTm shift A0 ≲ ren_PTm shift A1.
Proof. Proof.
move => n Γ A0 A1 B i hB hlt. move => Γ A0 A1 B i hB hlt.
apply : renaming_su'; eauto. apply : renaming_su'; eauto.
apply : Wff_Cons'; eauto. apply : Wff_Cons'; eauto.
apply : renaming_shift; eauto. apply : renaming_shift; eauto.
Qed. Qed.
Lemma regularity_sub0 : forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i. Lemma regularity_sub0 : forall Γ (A B : PTm), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i.
Proof. hauto lq:on use:regularity. Qed. Proof. hauto lq:on use:regularity. Qed.
Lemma Su_Pi_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 : Lemma Su_Pi_Proj2_Var Γ (A0 A1 : PTm) B0 B1 :
Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1. cons A1 Γ ⊢ B0 ≲ B1.
Proof. Proof.
move => h. move => h.
have /Su_Pi_Proj1 h1 := h. have /Su_Pi_Proj1 h1 := h.
@ -843,15 +844,16 @@ Proof.
move /weakening_su : (h) h2. move => /[apply]. move /weakening_su : (h) h2. move => /[apply].
move => h2. move => h2.
apply : Su_Pi_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2. apply : Su_Pi_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
apply E_Refl. apply T_Var' with (i := var_zero); eauto. apply E_Refl. apply T_Var with (i := var_zero); eauto.
sfirstorder use:wff_mutual. sfirstorder use:wff_mutual.
by asimpl. apply here.
by asimpl. by asimpl; rewrite subst_scons_id.
by asimpl; rewrite subst_scons_id.
Qed. Qed.
Lemma Su_Sig_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 : Lemma Su_Sig_Proj2_Var Γ (A0 A1 : PTm) B0 B1 :
Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1. (cons A0 Γ) ⊢ B0 ≲ B1.
Proof. Proof.
move => h. move => h.
have /Su_Sig_Proj1 h1 := h. have /Su_Sig_Proj1 h1 := h.
@ -859,8 +861,9 @@ Proof.
move /weakening_su : (h) h2. move => /[apply]. move /weakening_su : (h) h2. move => /[apply].
move => h2. move => h2.
apply : Su_Sig_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2. apply : Su_Sig_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
apply E_Refl. apply T_Var' with (i := var_zero); eauto. apply E_Refl. apply T_Var with (i := var_zero); eauto.
sfirstorder use:wff_mutual. sfirstorder use:wff_mutual.
by asimpl. apply here.
by asimpl. by asimpl; rewrite subst_scons_id.
by asimpl; rewrite subst_scons_id.
Qed. Qed.