From 9d8924cd6c6fd14573a702db79722c6780d22b11 Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Tue, 7 Nov 2023 16:36:03 +0100 Subject: [PATCH] More unified All_local_env, cleaned up {PCUIC,}Typing --- common/theories/BasicAst.v | 4 + common/theories/EnvironmentTyping.v | 420 ++++++++++++------ erasure/theories/ESubstitution.v | 2 +- erasure/theories/ErasureFunction.v | 4 +- erasure/theories/ErasureProperties.v | 6 +- .../theories/Bidirectional/BDStrengthening.v | 4 +- pcuic/theories/Bidirectional/BDToPCUIC.v | 16 +- pcuic/theories/Conversion/PCUICClosedConv.v | 2 +- pcuic/theories/Conversion/PCUICInstConv.v | 17 +- pcuic/theories/PCUICAlpha.v | 10 +- pcuic/theories/PCUICArities.v | 8 +- pcuic/theories/PCUICClassification.v | 2 +- pcuic/theories/PCUICContextConversion.v | 27 +- pcuic/theories/PCUICContexts.v | 8 +- pcuic/theories/PCUICExpandLetsCorrectness.v | 12 +- pcuic/theories/PCUICGlobalEnv.v | 5 +- pcuic/theories/PCUICInductiveInversion.v | 46 +- pcuic/theories/PCUICInductives.v | 39 +- pcuic/theories/PCUICSR.v | 36 +- pcuic/theories/PCUICSafeLemmata.v | 10 +- pcuic/theories/PCUICSpine.v | 46 +- pcuic/theories/PCUICSubstitution.v | 4 +- pcuic/theories/PCUICTyping.v | 227 ---------- pcuic/theories/PCUICValidity.v | 15 +- pcuic/theories/Typing/PCUICClosedTyp.v | 8 +- .../Typing/PCUICContextConversionTyp.v | 3 +- pcuic/theories/Typing/PCUICNamelessTyp.v | 4 +- pcuic/theories/Typing/PCUICRenameTyp.v | 34 +- .../Typing/PCUICUnivSubstitutionTyp.v | 4 +- pcuic/theories/Typing/PCUICWeakeningEnvTyp.v | 10 +- pcuic/theories/Typing/PCUICWeakeningTyp.v | 10 +- safechecker/theories/PCUICSafeChecker.v | 2 +- safechecker/theories/PCUICTypeChecker.v | 8 +- template-coq/theories/Typing.v | 155 ------- .../theories/PCUICToTemplateCorrectness.v | 4 +- 35 files changed, 479 insertions(+), 733 deletions(-) diff --git a/common/theories/BasicAst.v b/common/theories/BasicAst.v index e9e96d203..f84a3a460 100644 --- a/common/theories/BasicAst.v +++ b/common/theories/BasicAst.v @@ -244,6 +244,10 @@ End Contexts. Arguments context_decl : clear implicits. +Definition judgment_of_decl {term universe} d : judgment_ term universe := + TermoptTyp (decl_body d) (decl_type d). + + Definition map_decl {term term'} (f : term -> term') (d : context_decl term) : context_decl term' := {| decl_name := d.(decl_name); decl_body := option_map f d.(decl_body); diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v index e6374979f..9e027cec1 100644 --- a/common/theories/EnvironmentTyping.v +++ b/common/theories/EnvironmentTyping.v @@ -316,136 +316,6 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). Import T E TU. - Section TypeLocal. - Context (typing : forall (Γ : context), judgment -> Type). - - Inductive All_local_env : context -> Type := - | localenv_nil : - All_local_env [] - - | localenv_cons_abs Γ na t : - All_local_env Γ -> - typing Γ (Typ t) -> - All_local_env (Γ ,, vass na t) - - | localenv_cons_def Γ na b t : - All_local_env Γ -> - typing Γ (TermTyp b t) -> - All_local_env (Γ ,, vdef na b t). - Derive Signature NoConfusion for All_local_env. - End TypeLocal. - - Arguments localenv_nil {_}. - Arguments localenv_cons_def {_ _ _ _ _} _ _. - Arguments localenv_cons_abs {_ _ _ _} _ _. - - Lemma All_local_env_fold P f Γ : - All_local_env (fun Γ j => P (fold_context_k f Γ) (judgment_map (f #|Γ|) j)) Γ <~> - All_local_env P (fold_context_k f Γ). - Proof. - split. - - induction 1; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; try constructor; auto. - - induction Γ; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; intros H. - * constructor. - * destruct a as [na [b|] ty]; depelim H; specialize (IHΓ H); constructor; simpl; auto. - Qed. - - Lemma All_local_env_impl_gen (P Q : context -> judgment -> Type) l : - All_local_env P l -> - (forall Γ bo ty, P Γ (TermoptTyp bo ty) -> Q Γ (TermoptTyp bo ty)) -> - All_local_env Q l. - Proof. - induction 1; intros; simpl; econstructor; eauto. - Qed. - - Lemma All_local_env_impl (P Q : context -> judgment -> Type) l : - All_local_env P l -> - (forall Γ j, P Γ j -> Q Γ j) -> - All_local_env Q l. - Proof. - induction 1; intros; simpl; econstructor; eauto. - Qed. - - Lemma All_local_env_impl_ind {P Q : context -> judgment -> Type} {l} : - All_local_env P l -> - (forall Γ j, All_local_env Q Γ -> P Γ j -> Q Γ j) -> - All_local_env Q l. - Proof. - induction 1; intros; simpl; econstructor; eauto. - Qed. - - Lemma All_local_env_skipn P Γ : All_local_env P Γ -> forall n, All_local_env P (skipn n Γ). - Proof. - induction 1; simpl; intros; destruct n; simpl; try econstructor; eauto. - Qed. - #[global] - Hint Resolve All_local_env_skipn : wf. - - Section All_local_env_rel. - - Definition All_local_rel P Γ Γ' - := (All_local_env (fun Γ0 j => P (Γ ,,, Γ0) j) Γ'). - - Definition All_local_rel_nil {P Γ} : All_local_rel P Γ [] - := localenv_nil. - - Definition All_local_rel_abs {P Γ Γ' A na} : - All_local_rel P Γ Γ' -> P (Γ ,,, Γ') (Typ A) - -> All_local_rel P Γ (Γ',, vass na A) - := localenv_cons_abs. - - Definition All_local_rel_def {P Γ Γ' t A na} : - All_local_rel P Γ Γ' -> - P (Γ ,,, Γ') (TermTyp t A) -> - All_local_rel P Γ (Γ',, vdef na t A) - := localenv_cons_def. - - Lemma All_local_rel_local : - forall P Γ, - All_local_env P Γ -> - All_local_rel P [] Γ. - Proof. - intros P Γ h. eapply All_local_env_impl. - - exact h. - - intros. - rewrite app_context_nil_l. assumption. - Defined. - - Lemma All_local_local_rel P Γ : - All_local_rel P [] Γ -> All_local_env P Γ. - Proof. - intro X. eapply All_local_env_impl. exact X. - intros Γ0 j XX; cbn in XX; rewrite app_context_nil_l in XX; assumption. - Defined. - - Lemma All_local_app_rel {P Γ Γ'} : - All_local_env P (Γ ,,, Γ') -> All_local_env P Γ × All_local_rel P Γ Γ'. - Proof. - induction Γ'. - - intros hΓ. - split. - 1: exact hΓ. - constructor. - - inversion 1 ; subst. - all: edestruct IHΓ' ; auto. - all: split ; auto. - all: constructor ; auto. - Defined. - - Lemma All_local_rel_app {P Γ Γ'} : - All_local_env P Γ -> All_local_rel P Γ Γ' -> All_local_env P (Γ ,,, Γ'). - Proof. - intros ? hΓ'. - induction hΓ'. - - assumption. - - cbn. - constructor ; auto. - - cbn. - constructor ; auto. - Defined. - - End All_local_env_rel. - (** Well-formedness of local environments embeds a sorting for each variable *) Definition on_local_decl (P : context -> judgment -> Type) Γ d := @@ -640,6 +510,15 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). intros; rewrite -Hf; now apply HPQ. Qed. + Lemma lift_typing_map {P} f j : + lift_typing0 (fun t T => P (f t) (f T)) j -> + (forall u, f (tSort u) = tSort u) -> + lift_typing0 P (judgment_map f j). + Proof. + intros HT Hf. + apply lift_typing_f_impl with (1 := HT) => //. + Qed. + Lemma lift_sorting_impl {Pc Qc Ps Qs j} : lift_sorting Pc Ps j -> (forall t T, Pc t T -> Qc t T) -> @@ -661,6 +540,230 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). intros; now apply HPQ. Qed. + Section TypeLocal. + Context (typing : forall (Γ : context), judgment -> Type). + + Inductive All_local_env : context -> Type := + | localenv_nil : + All_local_env [] + + | localenv_cons_abs Γ na t : + All_local_env Γ -> + typing Γ (Typ t) -> + All_local_env (Γ ,, vass na t) + + | localenv_cons_def Γ na b t : + All_local_env Γ -> + typing Γ (TermTyp b t) -> + All_local_env (Γ ,, vdef na b t). + + Derive Signature NoConfusion for All_local_env. + End TypeLocal. + + Arguments localenv_nil {_}. + Arguments localenv_cons_def {_ _ _ _ _} _ _. + Arguments localenv_cons_abs {_ _ _ _} _ _. + + Definition localenv_cons {typing Γ na bo t} : + All_local_env typing Γ -> typing Γ (TermoptTyp bo t) -> All_local_env typing (Γ ,, mkdecl na bo t) + := match bo with None => localenv_cons_abs | Some b => localenv_cons_def end. + + Definition All_local_env_snoc {P Γ decl} : All_local_env P Γ -> on_local_decl P Γ decl -> All_local_env P (Γ ,, decl) := + match decl with mkdecl na bo t => localenv_cons end. + + Lemma All_local_env_tip {typing Γ decl} : All_local_env typing (Γ ,, decl) -> All_local_env typing Γ × on_local_decl typing Γ decl. + Proof. + intros wfΓ; depelim wfΓ. + all: split; assumption. + Defined. + + Lemma All_local_env_ind1 typing P : + P [] -> + (forall Γ decl, P Γ -> on_local_decl typing Γ decl -> P (Γ ,, decl)) -> + forall Γ, All_local_env typing Γ -> P Γ. + Proof. + induction Γ => //. + move/All_local_env_tip => [] ??. + now apply X0. + Defined. + + Lemma All_local_env_fold P f Γ : + All_local_env (fun Γ j => P (fold_context_k f Γ) (judgment_map (f #|Γ|) j)) Γ <~> + All_local_env P (fold_context_k f Γ). + Proof. + split. + - induction 1; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; try constructor; auto. + - induction Γ; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; intros H. + * constructor. + * destruct a as [na [b|] ty]; depelim H; specialize (IHΓ H); constructor; simpl; auto. + Qed. + + Lemma All_local_env_impl_gen (P Q : context -> judgment -> Type) l : + All_local_env P l -> + (forall Γ bo ty, P Γ (TermoptTyp bo ty) -> Q Γ (TermoptTyp bo ty)) -> + All_local_env Q l. + Proof. + induction 1; intros; simpl; econstructor; eauto. + Qed. + + Lemma All_local_env_impl (P Q : context -> judgment -> Type) l : + All_local_env P l -> + (forall Γ j, P Γ j -> Q Γ j) -> + All_local_env Q l. + Proof. + induction 1; intros; simpl; econstructor; eauto. + Qed. + + Lemma All_local_env_impl_ind {P Q : context -> judgment -> Type} {l} : + All_local_env P l -> + (forall Γ j, All_local_env Q Γ -> P Γ j -> Q Γ j) -> + All_local_env Q l. + Proof. + induction 1; intros; simpl; econstructor; eauto. + Qed. + + Lemma All_local_env_skipn {P Γ} n : All_local_env P Γ -> All_local_env P (skipn n Γ). + Proof. + intros hΓ. + induction n in Γ, hΓ |- * => //. + destruct Γ; cbn; eauto. + apply All_local_env_tip in hΓ as []. + eauto. + Defined. + #[global] + Hint Resolve All_local_env_skipn : wf. + + Lemma All_local_env_app_skipn {P Γ Δ} n : All_local_env P (Γ ,,, Δ) -> + All_local_env P (Γ ,,, skipn n Δ). + Proof. + intros hΓ. + induction n in Δ, hΓ |- * => //. + destruct Δ; cbn; eauto. + apply All_local_env_tip in hΓ as []. + eauto. + Qed. + + Lemma All_local_env_nth_error {P Γ n decl} : All_local_env P Γ -> nth_error Γ n = Some decl -> on_local_decl P (skipn (S n) Γ) decl. + Proof. + induction Γ in n |- *; destruct n => //= /All_local_env_tip [] wfΓ ondecl Hnth //=. + - injection Hnth as [= ->]. assumption. + - now eapply IHΓ. + Defined. + + Section All_local_env_rel. + + Definition All_local_rel P Γ Γ' + := (All_local_env (fun Δ j => P (Γ ,,, Δ) j) Γ'). + + Definition All_local_rel_nil {P Γ} : All_local_rel P Γ [] + := localenv_nil. + + Definition All_local_rel_snoc {P Γ Γ' decl} : + All_local_rel P Γ Γ' -> on_local_decl P (Γ ,,, Γ') decl -> + All_local_rel P Γ (Γ' ,, decl) + := All_local_env_snoc. + + Definition All_local_rel_abs {P Γ Γ' A na} : + All_local_rel P Γ Γ' -> P (Γ ,,, Γ') (Typ A) + -> All_local_rel P Γ (Γ',, vass na A) + := localenv_cons. + + Definition All_local_rel_def {P Γ Γ' t A na} : + All_local_rel P Γ Γ' -> + P (Γ ,,, Γ') (TermTyp t A) -> + All_local_rel P Γ (Γ',, vdef na t A) + := localenv_cons. + + Definition All_local_rel_tip {P Γ Γ' decl} : + All_local_rel P Γ (Γ' ,, decl) -> All_local_rel P Γ Γ' × on_local_decl P (Γ ,,, Γ') decl + := All_local_env_tip. + + Definition All_local_rel_ind1 typing Γ P : + P [] -> + (forall Δ decl, P Δ -> on_local_decl typing (Γ ,,, Δ) decl -> P (Δ ,, decl)) -> + forall Δ, All_local_rel typing Γ Δ -> P Δ + := All_local_env_ind1 _ P. + + Lemma All_local_rel_local : + forall P Γ, + All_local_env P Γ -> + All_local_rel P [] Γ. + Proof. + intros P Γ h. eapply All_local_env_impl. + - exact h. + - intros. + rewrite app_context_nil_l. assumption. + Defined. + + Lemma All_local_local_rel P Γ : + All_local_rel P [] Γ -> All_local_env P Γ. + Proof. + intro X. eapply All_local_env_impl. exact X. + intros Γ0 j XX; cbn in XX; rewrite app_context_nil_l in XX; assumption. + Defined. + + Lemma All_local_app_rel {P Γ Γ'} : + All_local_env P (Γ ,,, Γ') -> All_local_env P Γ × All_local_rel P Γ Γ'. + Proof. + induction Γ'. + - intros hΓ. + split. + 1: exact hΓ. + constructor. + - move => /= /All_local_env_tip [] hΓ ona. + edestruct IHΓ' ; auto. + split ; auto. + apply All_local_rel_snoc; auto. + Defined. + + Definition All_local_env_app_inv {P Γ Γ'} := @All_local_app_rel P Γ Γ'. + + Lemma All_local_rel_app_inv {P Γ Γ' Γ''} : + All_local_rel P Γ (Γ' ,,, Γ'') -> All_local_rel P Γ Γ' × All_local_rel P (Γ ,,, Γ') Γ''. + Proof. + intro H. + eapply All_local_env_app_inv in H as [H H']. + split; tas. + apply All_local_env_impl with (1 := H'). + intros; now rewrite -app_context_assoc. + Defined. + + Lemma All_local_env_app {P Γ Γ'} : + All_local_env P Γ -> All_local_rel P Γ Γ' -> All_local_env P (Γ ,,, Γ'). + Proof. + induction 2 using All_local_rel_ind1 => //=. + apply All_local_env_snoc; tas. + Defined. + + Lemma All_local_rel_app {P Γ Γ' Γ''} : + All_local_rel P Γ Γ' -> All_local_rel P (Γ ,,, Γ') Γ'' -> All_local_rel P Γ (Γ' ,,, Γ''). + Proof. + induction 2 using All_local_rel_ind1 => //=. + apply All_local_rel_snoc; tas. now rewrite app_context_assoc. + Defined. + + Lemma All_local_env_prod_inv : + forall P Q Γ, + All_local_env (fun Δ j => P Δ j × Q Δ j) Γ -> + All_local_env P Γ × All_local_env Q Γ. + Proof using Type. + intros P Q Γ h. + split; apply All_local_env_impl with (1 := h). + all: now intros ??[]. + Qed. + + Lemma All_local_env_lift_prod_inv : + forall P Q Δ, + All_local_env (lift_typing1 (Prop_local_conj P Q)) Δ -> + All_local_env (lift_typing1 P) Δ × All_local_env (lift_typing1 Q) Δ. + Proof using Type. + intros P Q Δ h. + split; apply All_local_env_impl with (1 := h); intros ?? H; apply lift_typing_impl with (1 := H). + all: move => ??[] //. + Qed. + + End All_local_env_rel. + Section TypeLocalOver. Context (checking : context -> term -> term -> Type). Context (sorting : context -> term -> Universe.t -> Type). @@ -710,6 +813,39 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). repeat (eexists; tea). Defined. + Definition on_wf_local_decl {typing Γ} + (P : forall Γ (wfΓ : All_local_env (lift_typing1 typing) Γ) t T, typing Γ t T -> Type) + (wfΓ : All_local_env (lift_typing1 typing) Γ) {d} + (H : on_local_decl (lift_typing1 typing) Γ d) := + match d return (on_local_decl (lift_typing1 typing) Γ d) -> Type with + | {| decl_name := na; decl_body := Some b; decl_type := ty |} + => fun H => P Γ wfΓ b ty H.1 × P Γ wfΓ ty _ H.2.π2.1 + | {| decl_name := na; decl_body := None; decl_type := ty |} + => fun H => P Γ wfΓ ty _ H.2.π2.1 + end H. + + + Lemma nth_error_All_local_env_over {typing} {P Γ n decl} (eq : nth_error Γ n = Some decl) {wfΓ : All_local_env (lift_typing1 typing) Γ} : + All_local_env_over typing P Γ wfΓ -> + let Γ' := skipn (S n) Γ in + let wfΓ' := All_local_env_skipn _ wfΓ in + let p := All_local_env_nth_error wfΓ eq in + (All_local_env_over typing P Γ' wfΓ' * on_wf_local_decl P wfΓ' p)%type. + Proof. + induction 1 in n, decl, eq |- *. + - exfalso. destruct n => //. + - destruct n; simpl. + + simpl in *. split; tas. clear -Hs. + destruct f_equal; cbn. + assumption. + + apply IHX. + - destruct n; simpl. + + simpl in *. split; tas. clear -Hc Hs. + destruct f_equal; cbn. + split; assumption. + + apply IHX. + Defined. + Lemma All_local_env_over_2 typing P Γ (H : All_local_env (lift_typing1 typing) Γ) : All_local_env_over _ (fun Γ _ t T _ => P Γ t T) _ H -> All_local_env (lift_typing_conj typing P) Γ. @@ -838,7 +974,7 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). All_local_env_size_gen (fun Δ => csize (Γ ,,, Δ)) (fun Δ => ssize (Γ ,,, Δ)) base Δ w). Lemma All_local_env_size_app c s csize ssize base Γ Γ' (wfΓ : All_local_env (lift_sorting1 c s) Γ) (wfΓ' : All_local_rel (lift_sorting1 c s) Γ Γ') : - All_local_env_size_gen csize ssize base _ (All_local_rel_app wfΓ wfΓ') + base = All_local_env_size_gen csize ssize base _ wfΓ + All_local_rel_size_gen c s csize ssize base _ _ wfΓ'. + All_local_env_size_gen csize ssize base _ (All_local_env_app wfΓ wfΓ') + base = All_local_env_size_gen csize ssize base _ wfΓ + All_local_rel_size_gen c s csize ssize base _ _ wfΓ'. Proof. induction Γ'. - dependent inversion wfΓ'. @@ -1874,6 +2010,28 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT forall Σ, on_global_env Pcmp P Σ -> on_global_env Pcmp Q Σ. Proof. intros; eapply on_global_env_impl_config; eauto; reflexivity. Qed. + Lemma lookup_on_global_env `{checker_flags} {Pcmp P} {Σ : global_env} {c decl} : + on_global_env Pcmp P Σ -> + lookup_env Σ c = Some decl -> + ∑ Σ' : global_env_ext, on_global_env Pcmp P Σ' × strictly_extends_decls Σ' Σ × on_global_decl Pcmp P Σ' c decl. + Proof. + unfold on_global_env. + destruct Σ as [univs Σ retro]; cbn. intros [cu ond]. + induction ond; cbn in * => //. + destruct o. rename udecl0 into udecl. + case: eqb_specT => [-> [= <-]| ne]. + - exists ({| universes := univs; declarations := Σ; retroknowledge := retro |}, udecl); cbn. + split; try constructor; tas. + split => //=. now exists [(kn, d)]. + - intros hl. + specialize (IHond hl) as [[Σ' udecl'] [ong [[equ ext extretro] ond']]]. + exists (Σ', udecl'). cbn in equ |- *. subst univs. split; cbn; auto; try apply ong. + split; cbn; auto. split; cbn; auto. + cbn in ext. destruct ext as [Σ'' ->]. cbn in *. + now exists ((kn, d) :: Σ''). + Qed. + + End GlobalMaps. Module Type GlobalMapsSig (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvTypingSig T E TU) (C: ConversionSig T E TU ET) (L: LookupSig T E). diff --git a/erasure/theories/ESubstitution.v b/erasure/theories/ESubstitution.v index d1dcccbf0..151bd532c 100644 --- a/erasure/theories/ESubstitution.v +++ b/erasure/theories/ESubstitution.v @@ -242,7 +242,7 @@ Proof. eapply e. eapply weakening_wf_local => //. rewrite app_context_assoc //. - now eapply wf_local_app_inv in X7 as []. + now eapply All_local_env_app_inv in X7 as []. rewrite app_context_assoc. reflexivity. now rewrite [_.1](PCUICCasesContexts.inst_case_branch_context_eq a). - assert (HT : Σ;;; Γ ,,, Γ' |- PCUICAst.tFix mfix n : (decl.(dtype))). diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v index 4303991ee..d388ce56d 100644 --- a/erasure/theories/ErasureFunction.v +++ b/erasure/theories/ErasureFunction.v @@ -36,8 +36,8 @@ Lemma wf_local_rel_alpha_eq_end {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Δ wf_local_rel Σ Γ Δ -> wf_local_rel Σ Γ Δ'. Proof. intros wfΓ eqctx wf. - apply wf_local_app_inv. - eapply wf_local_app in wf => //. + apply All_local_env_app_inv. + eapply All_local_env_app in wf => //. eapply PCUICSpine.wf_local_alpha; tea. eapply All2_app => //. reflexivity. Qed. diff --git a/erasure/theories/ErasureProperties.v b/erasure/theories/ErasureProperties.v index e67357ff6..8e2f5631a 100644 --- a/erasure/theories/ErasureProperties.v +++ b/erasure/theories/ErasureProperties.v @@ -44,7 +44,7 @@ Proof. apply All_local_env_impl_ind with (1 := w0) => Δ j wfΓ' Hj. apply lift_typing_impl with (1 := Hj) => t T HT. eapply context_conversion with (Γ ,,, Δ); eauto. - - eapply wf_local_app; eauto. + - eapply All_local_env_app; eauto. - eapply conv_context_app_same; eauto. Qed. @@ -52,9 +52,9 @@ Lemma conv_context_wf_local_app {A B A'} {Σ : global_env_ext} {wfΣ : wf Σ} : wf_local Σ (A ,,, B) -> wf_local Σ A' -> conv_context cumulAlgo_gen Σ A A' -> wf_local Σ (A' ,,, B). Proof. intros wfab wfa' cv. - eapply wf_local_app => //. + eapply All_local_env_app => //. eapply wf_local_rel_conv; tea. - now eapply wf_local_app_inv. + now eapply All_local_env_app_inv. Qed. diff --git a/pcuic/theories/Bidirectional/BDStrengthening.v b/pcuic/theories/Bidirectional/BDStrengthening.v index 2728f3df5..34598a8f7 100644 --- a/pcuic/theories/Bidirectional/BDStrengthening.v +++ b/pcuic/theories/Bidirectional/BDStrengthening.v @@ -1004,10 +1004,10 @@ Lemma strengthening `{cf: checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ Proof. intros Hty. assert (wf_local Σ Γ) by - move: Hty => /typing_wf_local /wf_local_app_inv [] /wf_local_app_inv [] //. + move: Hty => /typing_wf_local /All_local_env_app_inv [] /All_local_env_app_inv [] //. assert (wfΓ'' : wf_local Σ (Γ ,,, Γ'')). - { apply wf_local_app => //. + { apply All_local_env_app => //. erewrite <- (lift_unlift_context Γ''). eapply bidirectional_to_pcuic ; tea. rewrite rename_context_lift_context. diff --git a/pcuic/theories/Bidirectional/BDToPCUIC.v b/pcuic/theories/Bidirectional/BDToPCUIC.v index a641496b0..30ab48109 100644 --- a/pcuic/theories/Bidirectional/BDToPCUIC.v +++ b/pcuic/theories/Bidirectional/BDToPCUIC.v @@ -146,7 +146,7 @@ Section BDToPCUICTyping. Proof using Type. intros allo ; induction allo. all: constructor; tas. - all: apply wf_local_app in IHallo; tas. + all: apply All_local_env_app in IHallo; tas. all: apply lift_sorting_it_impl with tu => //= Ht; eauto. apply Hc; cbn; auto. now eapply has_sort_isType, Hs. @@ -163,7 +163,7 @@ Section BDToPCUICTyping. subst. assert (isType Σ Γ t). { - eapply wf_local_rel_app_inv in wfΔ as [wfd _]. + eapply All_local_rel_app_inv in wfΔ as [wfd _]. inversion_clear wfd. eassumption. } @@ -172,19 +172,19 @@ Section BDToPCUICTyping. 1: by rewrite subst_telescope_length ; reflexivity. rewrite -(rev_involutive Γ0) -subst_context_telescope. cbn in wfΔ. - apply wf_local_rel_app_inv in wfΔ as []. + apply All_local_rel_app_inv in wfΔ as []. apply wf_local_local_rel. eapply substitution_wf_local ; eauto. 1: repeat constructor. 1: rewrite subst_empty ; eauto. - apply wf_local_app. + apply All_local_env_app. 1: constructor ; eauto. eassumption. - subst d. subst. assert (isType Σ Γ t). { - eapply wf_local_rel_app_inv in wfΔ as [wfd _]. + eapply All_local_rel_app_inv in wfΔ as [wfd _]. inversion_clear wfd. apply lift_sorting_it_impl_gen with X2 => //. } @@ -256,7 +256,7 @@ Section BDToPCUICTyping. move: (H) => [decl ?]. unshelve epose proof (decl' := declared_minductive_to_gen decl); eauto. eapply wf_local_subst_instance_decl ; eauto. - eapply wf_local_app_inv. + eapply All_local_env_app_inv. now eapply on_minductive_wf_params_indices. } @@ -491,7 +491,7 @@ Proof. - assert (Σ ;;; Γ |- i : t). { rewrite /= app_context_assoc in wfΓ. - eapply wf_local_app_inv in wfΓ as [wfΓ _]. + eapply All_local_env_app_inv in wfΓ as [wfΓ _]. inversion wfΓ ; subst. now apply checking_typing. } @@ -512,7 +512,7 @@ Proof. constructor. 1: constructor. rewrite !subst_empty. - eapply wf_local_app_inv in wfΓ as [wfΓ _]. + eapply All_local_env_app_inv in wfΓ as [wfΓ _]. inversion wfΓ ; subst. now eapply unlift_TermTyp. Qed. diff --git a/pcuic/theories/Conversion/PCUICClosedConv.v b/pcuic/theories/Conversion/PCUICClosedConv.v index 335ddfcde..9d95179a8 100644 --- a/pcuic/theories/Conversion/PCUICClosedConv.v +++ b/pcuic/theories/Conversion/PCUICClosedConv.v @@ -117,7 +117,7 @@ Proof. unshelve eapply declared_minductive_to_gen in h; tea. red in h. eapply lookup_on_global_env in h. 2: eauto. - destruct h as [Σ' [ext wfΣ' decl']]. + destruct h as (Σ' & ext & wfΣ' & decl'). red in decl'. destruct decl' as [h ? ? ?]. rewrite inds_spec. rewrite forallb_rev. unfold mapi. diff --git a/pcuic/theories/Conversion/PCUICInstConv.v b/pcuic/theories/Conversion/PCUICInstConv.v index eaaecb333..27c5783c7 100644 --- a/pcuic/theories/Conversion/PCUICInstConv.v +++ b/pcuic/theories/Conversion/PCUICInstConv.v @@ -1604,24 +1604,23 @@ Proof using Type. Qed. Lemma wf_local_app_inst (Σ : global_env_ext) {wfΣ : wf Σ} Γ Δ : - All_local_env (fun Γ' j => + All_local_rel (fun Γ j => forall Δ σ, wf_local Σ Δ -> - Σ ;;; Δ ⊢ σ : (Γ ,,, Γ') -> - lift_typing0 (fun (t T : term) => Σ ;;; Δ |- t.[σ] : T.[σ]) j) Δ -> + Σ ;;; Δ ⊢ σ : Γ -> + lift_typing0 (fun t T => Σ ;;; Δ |- t.[σ] : T.[σ]) j) Γ Δ -> forall Δ' σ, Σ ;;; Δ' ⊢ σ : Γ -> wf_local Σ Δ' -> wf_local Σ (Δ' ,,, inst_context σ Δ). Proof using Type. intros. - induction X. + induction X using All_local_rel_ind1. - now simpl. - - rewrite inst_context_snoc /=. constructor; auto. - eapply t0; tas. - eapply well_subst_app; auto. - - rewrite inst_context_snoc /=. constructor; auto. - eapply t0; tas. + - rewrite inst_context_snoc /=. + apply All_local_env_snoc; auto. + apply lift_typing_map with (j := judgment_of_decl _) => //. + eapply X; tas. eapply well_subst_app; auto. Qed. diff --git a/pcuic/theories/PCUICAlpha.v b/pcuic/theories/PCUICAlpha.v index dfcf5055e..31d66ab58 100644 --- a/pcuic/theories/PCUICAlpha.v +++ b/pcuic/theories/PCUICAlpha.v @@ -46,7 +46,7 @@ Section Alpha. lift_typing typing Σ Γ (Typ (lift0 (S i) ty)). Proof using Type. intros Σ Γ i na ty hΣ hΓ e. simpl. - eapply nth_error_All_local_env in e as hj; tea. + eapply All_local_env_nth_error in e as hj; tea. apply nth_error_Some_length in e. rewrite -(firstn_skipn (S i) Γ) in hΓ |- *. apply lift_typing_f_impl with (1 := hj) => // ?? HT. @@ -731,7 +731,7 @@ Section Alpha. destruct eqp. eapply PCUICSpine.ctx_inst_eq_context; tea. rewrite List.rev_involutive. - * eapply weaken_wf_local; tea. now eapply wf_local_app_inv in X4 as []. + * eapply weaken_wf_local; tea. now eapply All_local_env_app_inv in X4 as []. eapply (on_minductive_wf_params_indices_inst isdecl _ cup). * eapply ctx_inst_eq_context; tea. cbn; eauto. * eapply ctx_inst_eq_context; tea. cbn; intros; eauto. @@ -751,7 +751,7 @@ Section Alpha. eapply All2_trans'; tea. 2:{ eapply All2_symP; tea. tc. } intros ??? [[] ?]; try constructor; simpl; auto; now transitivity na'. } - destruct (wf_local_app_inv X4) as [wfΔ _]. + destruct (All_local_env_app_inv X4) as [wfΔ _]. assert (clΔ := (wf_local_closed_context wfΔ)). econstructor; tea; eauto. 2,3: constructor; tea ; eauto. * eapply (type_ws_cumul_pb (pb:=Cumul)). @@ -872,7 +872,7 @@ Section Alpha. { apply eq_context_upto_cat; auto. reflexivity. } specialize (hwf (Γ ,,, types)). forward hwf. { apply eq_context_upto_cat; auto; reflexivity. } - eapply wf_local_app_inv in hwfΔ as []. + eapply All_local_env_app_inv in hwfΔ as []. eapply eq_context_conversion; tea. eapply type_Cumul'. + econstructor. @@ -956,7 +956,7 @@ Section Alpha. { apply eq_context_upto_cat; auto. reflexivity. } specialize (hwf (Γ ,,, types)). forward hwf. { apply eq_context_upto_cat; auto; reflexivity. } - eapply wf_local_app_inv in hwfΔ as []. + eapply All_local_env_app_inv in hwfΔ as []. eapply eq_context_conversion; tea. eapply type_Cumul'. + econstructor. diff --git a/pcuic/theories/PCUICArities.v b/pcuic/theories/PCUICArities.v index 698147649..e9c2fec96 100644 --- a/pcuic/theories/PCUICArities.v +++ b/pcuic/theories/PCUICArities.v @@ -676,15 +676,15 @@ Section WfEnv. + rewrite it_mkProd_or_LetIn_app. destruct x as [na [b|] ty]; cbn; move=> H. * apply inversion_LetIn in H as (s1 & A & H0 & H1 & H2 & H3); auto. - eapply All_local_env_app; split; pcuic. - eapply All_local_env_app. split. repeat constructor; eauto. repeat (eexists; eauto). + eapply All_local_env_app; pcuic. + eapply All_local_env_app. repeat constructor; eauto. repeat (eexists; eauto). auto. apply IHΔ in H2. eapply All_local_env_app_inv in H2. intuition auto. eapply All_local_env_impl; eauto. simpl. intros. now rewrite app_context_assoc. * apply inversion_Prod in H as (s1 & A & H0 & H1 & H2); auto. - eapply All_local_env_app; split; pcuic. - eapply All_local_env_app. split. repeat constructor; eauto. repeat (eexists; eauto). + eapply All_local_env_app; pcuic. + eapply All_local_env_app. repeat constructor; eauto. repeat (eexists; eauto). apply IHΔ in H1. eapply All_local_env_app_inv in H1. intuition auto. eapply All_local_env_impl; eauto. simpl. intros. diff --git a/pcuic/theories/PCUICClassification.v b/pcuic/theories/PCUICClassification.v index c9405a08b..168d7b10a 100644 --- a/pcuic/theories/PCUICClassification.v +++ b/pcuic/theories/PCUICClassification.v @@ -372,7 +372,7 @@ Qed. * elimtype False; depelim ass. * simpl. rewrite !it_mkProd_or_LetIn_app /= /mkProd_or_LetIn /= //. intros wf sp. - pose proof (wf_local_app_inv wf) as [_ wfty]. + pose proof (All_local_env_app_inv wf) as [_ wfty]. eapply All_local_env_app_inv in wfty as [wfty _]. depelim wfty. intros Hargs. eapply nth_error_None in Hargs. len in Hargs. len; simpl. diff --git a/pcuic/theories/PCUICContextConversion.v b/pcuic/theories/PCUICContextConversion.v index 2a61f7c83..ef86698ec 100644 --- a/pcuic/theories/PCUICContextConversion.v +++ b/pcuic/theories/PCUICContextConversion.v @@ -1154,37 +1154,24 @@ Qed. #[global] Hint Extern 4 (eq_term_upto_univ _ _ _ _ _) => reflexivity : pcuic. -Lemma nth_error_All_local_env {P Γ n} (isdecl : n < #|Γ|) : - All_local_env P Γ -> - on_some (on_local_decl P (skipn (S n) Γ)) (nth_error Γ n). -Proof. - induction 1 in n, isdecl |- *. red; simpl. - - destruct n; simpl; inv isdecl. - - destruct n. red; simpl. red. simpl. apply t0. - simpl. apply IHX. simpl in isdecl. lia. - - destruct n; simpl in *. - * rewrite skipn_S skipn_0. apply t0. - * rewrite !skipn_S. apply IHX. lia. -Qed. - Lemma context_cumulativity_wf_app {cf:checker_flags} Σ Γ Γ' Δ : cumul_context cumulAlgo_gen Σ Γ' Γ -> wf_local Σ Γ' -> - All_local_env (fun Γ j => - forall Γ' : context, - cumul_context cumulAlgo_gen Σ Γ' Γ -> wf_local Σ Γ' -> - (lift_typing0 (fun t T => Σ;;; Γ' |- t : T)) j) - (Γ,,, Δ) -> + All_local_env (fun Γ j => + forall Γ' : context, + cumul_context cumulAlgo_gen Σ Γ' Γ -> wf_local Σ Γ' -> + (lift_typing0 (fun t T => Σ;;; Γ' |- t : T)) j) + (Γ,,, Δ) -> wf_local Σ (Γ' ,,, Δ). Proof. intros. - eapply wf_local_app => //. + eapply All_local_env_app => //. eapply All_local_env_app_inv in X1 as []. eapply All_local_env_impl_ind; tea => /=. intros Γ'' j H HT. eapply HT. eapply All2_fold_app => //. eapply All2_fold_refl. intros. eapply cumul_decls_refl. - eapply All_local_env_app; split; auto. + eapply All_local_env_app; auto. Qed. Lemma is_closed_context_cumul_app Γ Δ Γ' : diff --git a/pcuic/theories/PCUICContexts.v b/pcuic/theories/PCUICContexts.v index 6af6db0f7..fe5ace964 100644 --- a/pcuic/theories/PCUICContexts.v +++ b/pcuic/theories/PCUICContexts.v @@ -347,7 +347,7 @@ Section WfEnv. Proof using wfΣ. induction Γ in Δ |- *; simpl; auto. intros wfΓ wfΔ. depelim wfΓ; simpl. - - apply IHΓ; auto. eapply All_local_env_app. split; auto. + - apply IHΓ; auto. eapply All_local_env_app; auto. + constructor; auto. + eapply All_local_env_impl; eauto. simpl; intros. now rewrite app_context_assoc. @@ -372,7 +372,7 @@ Section WfEnv. wf_local Σ (Γ ,,, Δ) -> wf_local Σ (Γ ,,, smash_context [] Δ). Proof using wfΣ. intros wf. - apply All_local_env_app. split. + apply All_local_env_app. now apply All_local_env_app_inv in wf. eapply wf_local_rel_smash_context; auto. Qed. @@ -641,7 +641,7 @@ Lemma subslet_extended_subst {cf} {Σ} {wfΣ : wf Σ} Γ Δ : (lift_context (context_assumptions Δ) 0 Δ). Proof. move=> wfΔ. - eapply wf_local_app_inv in wfΔ as [wfΓ wfΔ]. + eapply All_local_env_app_inv in wfΔ as [wfΓ wfΔ]. induction Δ as [|[na [d|] ?] ?] in wfΔ |- *; simpl; try constructor. * depelim wfΔ. repeat red in l, l0. specialize (IHΔ wfΔ). @@ -659,7 +659,7 @@ Proof. specialize (IHΔ wfΔ). rewrite lift_context_snoc /lift_decl /= /map_decl /=. assert (wf_local Σ (Γ ,,, smash_context [] Δ)). - { eapply wf_local_smash_end. eapply All_local_env_app. now split. } + { eapply wf_local_smash_end. now eapply All_local_env_app. } assert (wf_local Σ (Γ ,,, smash_context [] Δ ,, mkdecl na None (subst0 (extended_subst Δ 0) (lift (context_assumptions Δ) #|Δ| decl_type)))). { simpl. constructor; tas. diff --git a/pcuic/theories/PCUICExpandLetsCorrectness.v b/pcuic/theories/PCUICExpandLetsCorrectness.v index 39bd1b658..714499023 100644 --- a/pcuic/theories/PCUICExpandLetsCorrectness.v +++ b/pcuic/theories/PCUICExpandLetsCorrectness.v @@ -961,7 +961,7 @@ Section wtsub. split. eapply spine_subst_wt in s. now eapply All_rev_inv in s. exists mdecl, idecl. split; auto. now symmetry. - * eapply wf_local_app_inv. eapply wf_local_alpha. + * eapply All_local_env_app_inv. eapply wf_local_alpha. eapply All2_app; [|reflexivity]. eapply alpha_eq_subst_instance. symmetry; tea. eapply wf_ind_predicate; tea. pcuic. @@ -971,7 +971,7 @@ Section wtsub. eapply All2i_All2_mix_left in brs_ty; tea. eapply All2i_nth_hyp in brs_ty. solve_all. split; auto. - { eapply wf_local_app_inv. eapply wf_local_alpha. + { eapply All_local_env_app_inv. eapply wf_local_alpha. eapply All2_app; [|reflexivity]. eapply alpha_eq_subst_instance in a2. symmetry; tea. @@ -1896,7 +1896,7 @@ Proof. - destruct nth_error eqn:Heq => //. simpl in H. noconf H. simpl. destruct c; noconf H => //. rewrite (trans_lift _ (shiftnP #|skipn (S i) Γ| xpred0)); eauto. - eapply nth_error_All_local_env in wt0; tea. apply unlift_TermTyp in wt0. + eapply All_local_env_nth_error in wt0; tea. apply unlift_TermTyp in wt0. now eapply subject_is_open_term. do 2 constructor. now rewrite nth_error_map Heq. @@ -3696,7 +3696,7 @@ Proof. exact X. } { intros c; depelim c. constructor. - destruct (wf_local_app_inv wfctx) as [w _]. depelim w. + destruct (All_local_env_app_inv wfctx) as [w _]. depelim w. apply unlift_TermTyp in l0 as Hb. unshelve epose proof (substitution_wf_local (Γ':=[vdef na b t]) _ wfctx). shelve. { now eapply subslet_def_tip. } @@ -4033,13 +4033,13 @@ Proof. - cbn. constructor. cbn in wfctx. rewrite -app_assoc in wfctx. unshelve epose proof (substitution_wf_local (Σ := Σ) (Γ' := [vdef na b t]) _ wfctx). shelve. - { eapply subslet_def_tip. eapply wf_local_app_inv in wfctx as [wf' _]. eapply unlift_TermTyp. + { eapply subslet_def_tip. eapply All_local_env_app_inv in wfctx as [wf' _]. eapply unlift_TermTyp. now depelim wf'. } rewrite subst_context_subst_telescope in X. specialize (IHi X). rewrite (trans_local_subst_telescope (shiftnP (S #|Γ|) xpred0) (shiftnP #|Γ| xpred0)) in IHi. { apply wf_local_closed_context in wfctx. now move/onfvs_app: wfctx => /=. } - { eapply wf_local_app_inv in wfctx as [wf' _]. + { eapply All_local_env_app_inv in wfctx as [wf' _]. depelim wf'. apply unlift_TermTyp in l. cbn. now rewrite (subject_is_open_term l). } apply IHi. Qed. diff --git a/pcuic/theories/PCUICGlobalEnv.v b/pcuic/theories/PCUICGlobalEnv.v index 207ddc8a2..3abe5276e 100644 --- a/pcuic/theories/PCUICGlobalEnv.v +++ b/pcuic/theories/PCUICGlobalEnv.v @@ -94,13 +94,12 @@ Section DeclaredInv. ind_npars mdecl = context_assumptions mdecl.(ind_params). Proof using wfΣ. intros h. - eapply declared_minductive_to_gen in h. + unshelve eapply declared_minductive_to_gen in h; tea. unfold declared_minductive in h. eapply lookup_on_global_env in h; tea. - destruct h as [Σ' [ext wfΣ' decl']]. + destruct h as (Σ' & ext & wfΣ' & decl'). red in decl'. destruct decl' as [h ? ? ?]. now rewrite onNpars. - Unshelve. all: eauto. Qed. End DeclaredInv. diff --git a/pcuic/theories/PCUICInductiveInversion.v b/pcuic/theories/PCUICInductiveInversion.v index 9d258bb60..6ee342f73 100644 --- a/pcuic/theories/PCUICInductiveInversion.v +++ b/pcuic/theories/PCUICInductiveInversion.v @@ -1229,7 +1229,7 @@ Proof. specialize (X Δ ltac:(len; lia) _ _ H). simpl; len. destruct X; split; auto. simpl. - eapply All_local_env_app; split. + eapply All_local_env_app. constructor; auto. eapply (All_local_env_impl _ _ _ a). intros; auto. now rewrite app_context_assoc. simpl. @@ -2527,15 +2527,16 @@ Lemma ws_cumul_ctx_pb_wf_local {cf:checker_flags} {Σ} {wfΣ : wf Σ.1} Γ Γ' wf_local Σ (Γ' ,,, Δ). Proof. intros wf wf' e. - eapply All_local_env_app; split => //. - eapply wf_local_app_inv in wf as []. + eapply All_local_env_app => //. + eapply All_local_env_app_inv in wf as []. eapply All_local_env_impl_ind; eauto. intros. + rewrite -/(All_local_rel (lift_typing1 (typing Σ)) Γ' Γ0) /= in X, X0. apply lift_typing_impl with (1 := X0); intros ?? Hs. eapply closed_context_cumulativity; tea. - eapply All_local_env_app; split=> //. + eapply All_local_env_app=> //. eapply ws_cumul_ctx_pb_app_same; tea. 2:now symmetry. - eapply wf_local_app in X; tea. + eapply All_local_env_app in X; tea. eauto with fvs. Qed. @@ -2811,7 +2812,7 @@ Proof. rewrite !subst_instance_app_ctx in wfargs. apply is_closed_context_weaken => //. rewrite -app_context_assoc in wfargs. - apply wf_local_app_inv in wfargs as []; eauto with fvs. + apply All_local_env_app_inv in wfargs as []; eauto with fvs. apply wf_local_closed_context in a; move: a. now rewrite !is_closed_subst_inst. } 2:now eapply conv_inds. @@ -3239,12 +3240,12 @@ Proof. eapply typing_spine_ctx_inst in ty_indices as [argsi sp]; tea. - eapply ctx_inst_cumul; tea. apply (ctx_inst_smash.1 argsi). - { apply wf_local_app_inv. apply wf_local_smash_end; tea. + { apply All_local_env_app_inv. apply wf_local_smash_end; tea. eapply substitution_wf_local; tea. eapply X1. rewrite -app_context_assoc -subst_instance_app_ctx. eapply weaken_wf_local; tea. eapply (on_minductive_wf_params_indices_inst isdecl _ c). } - { apply wf_local_app_inv. apply wf_local_smash_end; tea. + { apply All_local_env_app_inv. apply wf_local_smash_end; tea. eapply substitution_wf_local; tea. eapply X0. rewrite -app_context_assoc -subst_instance_app_ctx. eapply weaken_wf_local; tea. @@ -3299,18 +3300,19 @@ Lemma wf_set_binder_name {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ} {nas Δ} wf_local Σ (Γ ,,, map2 set_binder_name nas Δ). Proof. intros ha wf. - apply wf_local_app_inv in wf as []. - eapply wf_local_app => //. - induction w in nas, ha |- *; depelim ha; cbn. constructor. - all: constructor; eauto; try apply IHw; auto. - all: apply lift_typing_impl with (1 := t0) => // ?? Hs. - all: eapply context_conversion; tea. - 1,3: eapply wf_local_app, IHw; eauto. - all: eapply eq_binder_annots_eq_ctx in ha. - all: eapply eq_context_upto_univ_conv_context. - all: eapply eq_context_upto_cat. - 1,3: reflexivity. - all: symmetry; apply ha. + apply All_local_env_app_inv in wf as [wfΓ wfΔ]. + eapply All_local_env_app => //. + induction wfΔ using All_local_rel_ind1 in nas, ha |- *; depelim ha; cbn. constructor. + specialize (IHwfΔ _ ha). + apply All_local_rel_snoc; tas. + apply lift_typing_impl with (1 := X) => // ?? Hs. + eapply context_conversion; tea. + 1: now eapply All_local_env_app. + eapply eq_binder_annots_eq_ctx in ha. + eapply eq_context_upto_univ_conv_context. + eapply eq_context_upto_cat. + 1: reflexivity. + symmetry; apply ha. Qed. Lemma WfArity_build_case_predicate_type {cf:checker_flags} {Σ Γ ci args mdecl idecl p ps} : @@ -3526,8 +3528,8 @@ Proof. rewrite -Nat.add_comm lift_context_add. eapply spine_subst_weakening;tea. eapply spine_subst_to_extended_list_k; tea. - now apply wf_local_app_inv in wf. - destruct (wf_local_app_inv wf) as []. + now apply All_local_env_app_inv in wf. + destruct (All_local_env_app_inv wf) as []. epose proof (@all_rels_subst_lift _ _ _ _ _ Δ' T a). eapply typing_spine_strengthen; tea; revgoals. eapply ws_cumul_pb_eq_le; symmetry. diff --git a/pcuic/theories/PCUICInductives.v b/pcuic/theories/PCUICInductives.v index d7feeb9c4..a124402e5 100644 --- a/pcuic/theories/PCUICInductives.v +++ b/pcuic/theories/PCUICInductives.v @@ -540,7 +540,7 @@ Record wf_subslet {cf} Σ Γ s Δ := Lemma wf_subslet_dom {cf} {Σ Γ s Δ} : wf_subslet Σ Γ s Δ -> wf_local Σ Γ. Proof. - intros [wf _]. now eapply wf_local_app_inv in wf. + intros [wf _]. now eapply All_local_env_app_inv in wf. Qed. Lemma subst_id s Γ t : @@ -953,7 +953,7 @@ Proof. eapply (weakening_wf_local (Γ'' := [_])). 2:eapply wf_projection_context_gen; tea. 2:apply decli. rewrite - !skipn_subst_context. - eapply wf_local_app_skipn. + eapply All_local_env_app_skipn. rewrite -(smash_context_subst []) /=. rewrite -(smash_context_subst []) /=. rewrite subst_context_nil. @@ -1191,7 +1191,7 @@ Proof. destruct isdecl as [[[] ?] ?]; eauto. } destruct (ind_cunivs oib) as [|? []] eqn:hequ => //. eapply PCUICClosedConv.sorts_local_ctx_All_local_env in wfargs. - 2:{ eapply All_local_env_app. split; auto. + 2:{ eapply All_local_env_app; auto. red in onpars. eapply (All_local_env_impl _ _ _ onpars). intros. apply lift_typing_impl with (1 := X); intros ? Hs. eapply weaken_ctx; auto. } @@ -1299,16 +1299,15 @@ Proof. rewrite nth_error_app_lt in Heq'. autorewrite with len. lia. set (idx := context_assumptions (cstr_args c) - S i) in *. - unshelve epose proof (nth_error_All_local_env (n:=idx) _ wfsargs). - autorewrite with len. simpl. lia. - rename X1 into onnth. - destruct (nth_error (subst_context _ 1 _) idx) as [c2|] eqn:hidx. + unshelve epose proof ((nth_error_Some' _ idx).2 _) as (c2 & hidx); cycle -1. + eapply @All_local_env_nth_error with (n := idx) (2 := hidx) in wfsargs as onnth. + 2: autorewrite with len; simpl. 2: lia. simpl in onnth. red in onnth. cbn in onnth. assert(decl_body c2 = None). { apply nth_error_assumption_context in hidx; auto. rewrite /subst_context /lift_context. apply assumption_context_fold, smash_context_assumption_context. constructor. } - rewrite H in onnth. 2:{ simpl in onnth; contradiction. } + rewrite H in onnth. destruct onnth as (_ & s & Hs & _). Ltac havefst H := match goal with @@ -1349,7 +1348,7 @@ Proof. { assert(wfargs' : wf_local (Σ.1, ind_universes mdecl) (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, smash_context [] (cstr_args c))). - { apply All_local_env_app; split; auto. + { apply All_local_env_app; auto. now apply All_local_env_app_inv in wfargs as [wfindpars wfargs]. apply wf_local_rel_smash_context; auto. } eapply closed_wf_local in wfargs'; auto. @@ -1411,7 +1410,7 @@ Proof. exists arg. split; auto. 2:{ apply wf_local_smash_end; auto. } eapply wf_local_smash_end in wfargs. - eapply (wf_local_app_skipn (n:=context_assumptions (cstr_args c) - S i)) in wfargs. + eapply All_local_env_app_skipn with (n:=context_assumptions (cstr_args c) - S i) in wfargs. epose proof (wf_local_nth_isType (d:=arg) (n:=0) wfargs). rewrite skipn_app in X1. rewrite skipn_length in X1. len. @@ -2099,7 +2098,7 @@ Lemma wf_local_expand_lets {cf} {Σ} {wfΣ : wf Σ} {Γ Δ Γ'} : Proof. intros hwf. rewrite /expand_lets_ctx /expand_lets_k_ctx. - destruct (wf_local_app_inv hwf) as [wfΓΔ _]. + destruct (All_local_env_app_inv hwf) as [wfΓΔ _]. rewrite -app_context_assoc in hwf. eapply (weakening_wf_local (Γ'' := smash_context [] Δ)) in hwf. len in hwf. simpl in hwf. simpl. @@ -2121,10 +2120,10 @@ Proof. rewrite -app_context_assoc in Ht. eapply (weakening_typing (Γ'' := smash_context [] Δ)) in Ht. len in Ht. simpl in Ht. simpl. - 2:{ eapply wf_local_smash_end; pcuic. now apply wf_local_app_inv in X. } + 2:{ eapply wf_local_smash_end; pcuic. now apply All_local_env_app_inv in X. } rewrite lift_context_app app_context_assoc Nat.add_0_r in Ht. eapply substitution in Ht; tea. - 2:{ eapply PCUICContexts.subslet_extended_subst. now apply wf_local_app_inv in X. } + 2:{ eapply PCUICContexts.subslet_extended_subst. now apply All_local_env_app_inv in X. } now len in Ht. Qed. @@ -2302,17 +2301,17 @@ Proof. split. * rewrite -app_context_assoc. rewrite smash_context_app_expand_acc. - eapply wf_local_app_inv in spine_dom_wf as [wfΔ wfΓ']. - eapply wf_local_app. now apply wf_local_app_inv in wfΔ. + eapply All_local_env_app_inv in spine_dom_wf as [wfΔ wfΓ']. + eapply All_local_env_app. now apply All_local_env_app_inv in wfΔ. eapply wf_local_rel_smash_context_gen; tea. - * eapply wf_local_app_inv in spine_codom_wf as [wfΔ wfΓ']. + * eapply All_local_env_app_inv in spine_codom_wf as [wfΔ wfΓ']. rewrite - !app_context_assoc -expand_lets_ctx_app. - apply wf_local_app_inv in wfΔ as []. - eapply wf_local_app. - now apply wf_local_app_inv in a as []. + apply All_local_env_app_inv in wfΔ as []. + eapply All_local_env_app. + now apply All_local_env_app_inv in a as []. rewrite smash_context_app_expand_acc. apply wf_local_rel_smash_context_gen; tea. - eapply wf_local_rel_app; tea. + eapply All_local_rel_app; tea. * rewrite /expand_lets_k_ctx /expand_lets_k -map_map_compose -[map (fun t => _) s]map_map_compose. eapply subst_context_subst. now eapply lift_context_subst. diff --git a/pcuic/theories/PCUICSR.v b/pcuic/theories/PCUICSR.v index 55ba863a3..722a3e350 100644 --- a/pcuic/theories/PCUICSR.v +++ b/pcuic/theories/PCUICSR.v @@ -810,9 +810,9 @@ Proof. now eapply closed_red1_red. repeat constructor. specialize (t0 _ c0). - eapply wf_local_app_inv, substitution_wf_local; tea. + eapply All_local_env_app_inv, substitution_wf_local; tea. now eapply subslet_ass_tip. - eapply wf_local_app_inv, substitution_wf_local; tea. + eapply All_local_env_app_inv, substitution_wf_local; tea. now eapply subslet_ass_tip. constructor; auto. eapply IHc. rewrite -subst_context_subst_telescope. @@ -826,7 +826,7 @@ Proof. eapply substitution_wf_local; tea. repeat (constructor; tea). eapply subslet_def. constructor. all:rewrite !subst_empty //. - eapply wf_local_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. + eapply All_local_env_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. Qed. Lemma ctx_inst_merge' {cf} {Σ} {wfΣ : wf Σ} Γ inst inst' Δ : @@ -1434,7 +1434,7 @@ Lemma wf_subslet_skipn {cf Σ Γ s Δ n} : wf_subslet Σ Γ s Δ → wf_subslet Σ Γ (skipn n s) (skipn n Δ). Proof. intros []; split; auto using subslet_skipn. - now eapply wf_local_app_skipn. + now eapply All_local_env_app_skipn. Qed. Lemma isType_subst_arities {cf} {Σ} {wfΣ : wf Σ} {ind mdecl idecl u} {Γ T} : @@ -1554,11 +1554,13 @@ Proof. split; auto. intros Γ' Δ' Δ ->. induction 1. * depelim p. subst. depelim X. constructor. - now eapply wf_local_app_inv. + rewrite -/(All_local_rel (lift_typing1 (typing Σ)) Γ' Γ). + now eapply All_local_env_app_inv. eapply lift_sorting_it_impl_gen with (tu := tu) => // _. now eapply Hs. - * depelim X. - constructor. now eapply wf_local_app_inv. + * depelim X. constructor. + rewrite -/(All_local_rel (lift_typing1 (typing Σ)) Γ' Γ). + now eapply All_local_env_app_inv. depelim p. destruct s as [[red <-]|[red <-]]; subst. all: apply lift_sorting_it_impl_gen with tu => // Ht; eauto. specialize (Hs _ red). eapply type_ws_cumul_pb; tea. @@ -1569,16 +1571,16 @@ Proof. * depelim X; specialize (IHX0 _ X); pose proof (wf_local_closed_context all). + constructor; auto. clear X. pose proof (wf_local_closed_context all). - eapply wf_local_app_inv in all as []. - eapply wf_local_app in IHX0; tea. + eapply All_local_env_app_inv in all as []. + eapply All_local_env_app in IHX0; tea. apply lift_sorting_it_impl with tu => // Hty. eapply closed_context_conversion; tea. eapply red_one_decl_ws_cumul_ctx_pb => //. eapply OnOne2_local_env_impl; tea. intros ???. eapply on_one_decl_impl => ???; firstorder. + constructor; auto. clear X. - eapply wf_local_app_inv in all as []. - eapply wf_local_app in IHX0; tea. + eapply All_local_env_app_inv in all as []. + eapply All_local_env_app in IHX0; tea. apply lift_sorting_it_impl with tu => // Hty. { eapply closed_context_conversion; tea. eapply red_one_decl_ws_cumul_ctx_pb => //. @@ -1592,7 +1594,7 @@ Proof. - (* Rel delta reduction *) rewrite heq_nth_error in H. destruct decl as [na b ty]; noconf H. simpl. - pose proof (PCUICValidity.nth_error_All_local_env heq_nth_error wfΓ); eauto. + eapply All_local_env_nth_error in wfΓ as X0; tea. apply unlift_TermTyp in X0. cbn in *. rewrite <- (firstn_skipn (S n) Γ). @@ -2494,7 +2496,7 @@ Proof. (subst_context (inds (inductive_mind p.(proj_ind)) u (ind_bodies mdecl)) #|ind_params mdecl| (subst_instance u (cstr_args cdecl)))))))); auto. ** eapply wf_local_closed_context. - eapply wf_local_app_skipn. + eapply All_local_env_app_skipn. apply wf_subslet_ctx in projsubs. apply projsubs. ** elim: p.(proj_arg). simpl. constructor. @@ -2704,7 +2706,7 @@ Proof. rewrite H5 in cum. set (idx := S (context_assumptions (cstr_args cdecl) - S parg)) in *. assert (wfpargctxu1 : wf_local Σ (Γ ,,, skipn idx (smash_context [] pargctxu1))). - { simpl. apply wf_local_app_skipn. apply wf_local_smash_end; auto. + { simpl. apply All_local_env_app_skipn. apply wf_local_smash_end; auto. apply idxsubst0. } destruct cum as [[cr mapd] cumdecls]. destruct decl'' as [na [b|] ty]; simpl in mapd; try discriminate. @@ -2794,7 +2796,7 @@ Proof. simpl. eapply ws_cumul_pb_refl. rewrite -skipn_lift_context. eapply wf_local_closed_context. - eapply wf_local_app_skipn. + eapply All_local_env_app_skipn. eapply weakening_wf_local => //. eapply wf_local_smash_end, idxsubst0. move: Hty. @@ -3199,9 +3201,7 @@ Section SRContext. ∑ s, Σ ;;; Γ |- lift0 (S n) (decl_type decl) : tSort s. Proof using Type. intros wfΓ Hnth. - eapply nth_error_All_local_env in wfΓ as H. - 2: now apply nth_error_Some_length in Hnth. - rewrite Hnth /= in H. + eapply All_local_env_nth_error in wfΓ as H; tea. apply nth_error_Some_length in Hnth. destruct H as (_ & s & Hs & _). eapply weakening with (Γ' := firstn (S n) Γ) in Hs; cbn in Hs; eauto. diff --git a/pcuic/theories/PCUICSafeLemmata.v b/pcuic/theories/PCUICSafeLemmata.v index 0946eca02..ff8a8795f 100644 --- a/pcuic/theories/PCUICSafeLemmata.v +++ b/pcuic/theories/PCUICSafeLemmata.v @@ -38,8 +38,8 @@ Proof. * eapply sp. * unshelve epose proof (on_minductive_wf_params_indices_inst isdecl _ cu). rewrite PCUICUnivSubstitutionConv.subst_instance_app_ctx in X. - eapply wf_local_app_inv in X as []. - eapply wf_local_app => //. + eapply All_local_env_app_inv in X as []. + eapply All_local_env_app => //. eapply wf_local_smash_end. now eapply weaken_wf_local; tea. Qed. @@ -342,8 +342,8 @@ Section Lemmata. Proof using Type. intros wfl. destruct pcontext as ((?&h)&?); simpl in *. - apply wf_local_app_inv in wfl as (_&wf). - apply wf_local_rel_app_inv in wf as (wf&_). + apply All_local_env_app_inv in wfl as (_&wf). + apply All_local_rel_app_inv in wf as (wf&_). destruct h; depelim wf; simpl in *. all: destruct l as (Hb & s & Hs & _); cbn in *; econstructor; eauto. Qed. @@ -446,7 +446,7 @@ Section Lemmata. eapply (declared_minductive_ind_npars x1). } now eapply spine_subst_smash in sp. ** cbn in conv_pctx. - eapply wf_local_app_inv. eapply wf_local_alpha. + eapply All_local_env_app_inv. eapply wf_local_alpha. ++ instantiate (1 := (Γ,,, stack_context π,,, smash_context [] (ind_params x)@[puinst],,, (ind_predicate_context ci x x0)@[puinst])). eapply All2_app => //. { eapply alpha_eq_subst_instance. now symmetry. } diff --git a/pcuic/theories/PCUICSpine.v b/pcuic/theories/PCUICSpine.v index b2d8261a0..27b5664d4 100644 --- a/pcuic/theories/PCUICSpine.v +++ b/pcuic/theories/PCUICSpine.v @@ -1185,7 +1185,7 @@ Qed.*) pose proof (ctx_inst_sub_spec ci) as msub. eapply make_context_subst_spec in msub. rewrite List.rev_involutive in msub. - split; pcuic. now eapply wf_local_app_inv in wfΔ as []. + split; pcuic. now eapply All_local_env_app_inv in wfΔ as []. move: ci msub. induction Δ in wfΔ, args |- *. simpl. intros ci. depelim ci. constructor. @@ -1484,9 +1484,8 @@ Proof. rewrite !on_free_vars_ctx_app => /andP[] onΓ. erewrite onΓ => /=. rewrite -{1}(firstn_skipn (S i) Δ) on_free_vars_ctx_app => /andP[] //. } - { clear X; eapply (nth_error_All_local_env (n:=i)) in wf. 2:len; lia. - rewrite nth_error_app_lt // in wf. - rewrite Hnth /= in wf. + { clear X; eapply (All_local_env_nth_error (n:=i)) in wf. + 2: rewrite nth_error_app_lt; eassumption. rewrite skipn_app in wf. replace (S i - #|Δ|) with 0 in wf. 2:lia. rewrite skipn_0 in wf. @@ -1495,8 +1494,8 @@ Proof. rewrite is_open_term_closed //. } rewrite skipn_length; simpl. apply All_local_env_over_2 in X. - unshelve eapply (nth_error_All_local_env (n:=i)) in X. 2: len. - rewrite nth_error_app_lt //= Hnth /on_local_decl /= in X. + eapply (All_local_env_nth_error (n:=i)) in X. + 2: rewrite nth_error_app_lt; eassumption. destruct X as ((Hb & Xb) & s & (Ht & Xt) & _). specialize (Xb Γ (skipn (S i) Δ)). forward Xb. rewrite skipn_app. unfold app_context. f_equal. @@ -1646,7 +1645,7 @@ Section WfEnv. rewrite -eql in l0. autorewrite with len in l0. simpl in l0. lia. eapply (substitution (Δ := []) IHc); auto. rewrite lift_context0_app !app_context_assoc in X. cbn in X. - eapply wf_local_app_inv in X as []. + eapply All_local_env_app_inv in X as []. rewrite lift_context_snoc0 Nat.add_0_r /= in a. cbn in a. depelim a. now apply unlift_TermTyp in l0. * rewrite app_length /= Nat.add_1_r in IHc. @@ -1686,7 +1685,7 @@ Section WfEnv. forward X by auto. apply X; auto. all:eauto with fvs. rewrite -app_tip_assoc app_assoc -[(l ++ _) ++ _]app_assoc eql. - eapply wf_local_app_inv in Hwf as []. eauto with fvs. + eapply All_local_env_app_inv in Hwf as []. eauto with fvs. Qed. Lemma red_expand_let {Γ na b ty t} : @@ -2151,7 +2150,7 @@ Section WfEnv. simpl. rewrite smash_context_acc. simpl. auto. auto. } split; auto. - - eapply All_local_env_app; split; auto. + - eapply All_local_env_app; auto. eapply wf_local_rel_smash_context; auto. - induction inst_subslet0 in inst, inst_ctx_subst0, spine_codom_wf0 |- *. depelim inst_ctx_subst0. @@ -2688,7 +2687,7 @@ Section WfEnv. rewrite app_context_assoc in cum. eapply substitution_ws_cumul_pb in cum; tea. len in cum; tea. - destruct (wf_local_app_inv wf). + destruct (All_local_env_app_inv wf). simpl. len. now eapply PCUICContexts.subslet_extended_subst. @@ -2704,7 +2703,7 @@ Section WfEnv. eapply (weakening_ws_cumul_pb (Γ'' := smash_context [] Δ)) in cum; tea. rewrite /expand_lets /expand_lets_k. eapply (PCUICConversion.substitution_ws_cumul_pb (Γ'' := [])) in cum; tea. len in cum; tea. - destruct (wf_local_app_inv wf). + destruct (All_local_env_app_inv wf). simpl. len. now eapply PCUICContexts.subslet_extended_subst. @@ -2969,7 +2968,7 @@ Section WfEnv. simpl in Hs. eapply has_sort_isType. now rewrite subst_context_nil /= in Hs. exact X. + unshelve epose proof (ctx_inst_spine_subst _ dom); tea. - eapply wf_local_app; tea. now eapply typing_wf_local. + eapply All_local_env_app; tea. now eapply typing_wf_local. pose proof (spine_codom_wf _ _ _ _ _ X0). eapply spine_subst_smash in X0; tea. eapply (PCUICConversion.substitution_ws_cumul_pb (Γ := Γ) (Γ'' := []) X0). @@ -2989,8 +2988,8 @@ Section WfEnv. destruct l as (Hb & s & Hs & _). simpl in *. destruct l0 as (Hb' & s' & Hs' & _). simpl in *. specialize (IHa _ dom). - forward IHa. apply wf_local_app_inv; pcuic. - forward IHa. apply wf_local_app_inv; pcuic. + forward IHa. apply All_local_env_app_inv; pcuic. + forward IHa. apply All_local_env_app_inv; pcuic. rewrite -(app_nil_r i). eapply (ctx_inst_app IHa). rewrite (ctx_inst_sub_subst IHa) /=. @@ -3094,9 +3093,9 @@ Section WfEnv. eapply (HP _ _ _ [i] [hd']); tea. repeat constructor. now rewrite subst_empty. repeat constructor. now rewrite subst_empty. constructor. auto. - eapply wf_local_app_inv. eapply substitution_wf_local; tea. + eapply All_local_env_app_inv. eapply substitution_wf_local; tea. repeat (constructor; tea). rewrite subst_empty; tea. - eapply wf_local_app_inv. eapply substitution_wf_local; tea. + eapply All_local_env_app_inv. eapply substitution_wf_local; tea. repeat (constructor; tea). rewrite subst_empty; tea. now eapply t0. constructor; auto. eapply IHc. rewrite -subst_context_subst_telescope. @@ -3109,7 +3108,7 @@ Section WfEnv. rewrite -subst_context_subst_telescope. eapply substitution_wf_local; tea. repeat (constructor; tea). eapply subslet_def_tip. - eapply wf_local_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. + eapply All_local_env_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. Qed. Lemma All2_ctx_inst {pb} {P} {Γ inst inst' Δ} : @@ -3145,16 +3144,16 @@ Section WfEnv. repeat constructor. now rewrite subst_empty. now apply subslet_ass_tip. now repeat constructor. - * eapply wf_local_app_inv. eapply substitution_wf_local; tea. + * eapply All_local_env_app_inv. eapply substitution_wf_local; tea. now apply subslet_ass_tip. - * eapply wf_local_app_inv. eapply substitution_wf_local; tea. + * eapply All_local_env_app_inv. eapply substitution_wf_local; tea. now apply subslet_ass_tip. - constructor. eapply IHc; eauto. simpl in wf. rewrite - !/(app_context _ _) app_context_assoc in wf. rewrite -subst_context_subst_telescope. eapply substitution_wf_local; tea. repeat (constructor; tea). eapply subslet_def_tip. - eapply wf_local_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. + eapply All_local_env_app_inv in wf as [wf _]. depelim wf. now eapply unlift_TermTyp. Qed. Lemma ctx_inst_open_terms Γ args Δ : @@ -3188,7 +3187,7 @@ Section WfEnv. now eapply subslet_untyped_subslet. now eapply subslet_untyped_subslet. eapply All2_rev. - move/wf_local_app_inv: X => [] /wf_local_app_inv[] /wf_local_closed_context clΓ0 _ _. + move/All_local_env_app_inv: X => [] /All_local_env_app_inv[] /wf_local_closed_context clΓ0 _ _. eapply subslet_open_terms, All_rev_inv in X0. eapply subslet_open_terms, All_rev_inv in X1. solve_all. eapply into_ws_cumul_pb; tea. @@ -3225,9 +3224,8 @@ Lemma wf_local_nth_isType {cf} {Σ} {Γ n d} : isType Σ (skipn (S n) Γ) d.(decl_type). Proof. intros Hwf hnth. - epose proof (nth_error_All_local_env (nth_error_Some_length hnth) Hwf). - rewrite hnth /= in X. unfold on_local_decl in X. - destruct decl_body => //. destruct X => //. + eapply All_local_env_nth_error in Hwf; tea. + eapply lift_sorting_it_impl_gen with Hwf => //. Qed. diff --git a/pcuic/theories/PCUICSubstitution.v b/pcuic/theories/PCUICSubstitution.v index 29ca027ae..816ba61e2 100644 --- a/pcuic/theories/PCUICSubstitution.v +++ b/pcuic/theories/PCUICSubstitution.v @@ -1786,8 +1786,8 @@ Proof. eapply subslet_well_subst; eauto. } 2:{ subst Γ. eapply typing_wf_local in HT. - eapply wf_local_app_inv in HT as [HΓ0 _]. - eapply wf_local_app_inv in HΓ0 as [HΓ0 _]. + eapply All_local_env_app_inv in HT as [HΓ0 _]. + eapply All_local_env_app_inv in HΓ0 as [HΓ0 _]. eapply All_local_env_inst; eauto. } unshelve eapply on_wf_global_env_impl ; tea. clear. intros * HΣ HP HQ Hty. diff --git a/pcuic/theories/PCUICTyping.v b/pcuic/theories/PCUICTyping.v index a5167eecb..aeb915483 100644 --- a/pcuic/theories/PCUICTyping.v +++ b/pcuic/theories/PCUICTyping.v @@ -1204,230 +1204,3 @@ Ltac my_rename_hyp h th := end. Ltac rename_hyp h ht ::= my_rename_hyp h ht. - -Section All_local_env. - (** * Lemmas about All_local_env *) - (* TODO: Move where All_local_env is defined, in EnvironmentTyping *) - - Context {cf: checker_flags}. - - Lemma nth_error_All_local_env {P Γ n} (isdecl : n < #|Γ|) : - All_local_env P Γ -> - on_some (on_local_decl P (skipn (S n) Γ)) (nth_error Γ n). - Proof using Type. - induction 1 in n, isdecl |- *. red; simpl. - - destruct n; simpl; inv isdecl. - - destruct n. red; simpl. red. simpl. apply t0. - simpl. apply IHX. simpl in isdecl. lia. - - destruct n. auto. - apply IHX. simpl in *. lia. - Qed. - - Lemma lookup_on_global_env P (Σ : global_env) c decl : - on_global_env cumulSpec0 P Σ -> - lookup_env Σ c = Some decl -> - { Σ' : global_env & [× extends_strictly_on_decls Σ' Σ, on_global_env cumulSpec0 P Σ' & - on_global_decl cumulSpec0 P (Σ', universes_decl_of_decl decl) c decl] }. - Proof using Type. - destruct Σ as [univs Σ retro]; rewrite /on_global_env /lookup_env; cbn. - intros [cu Σp]. - induction Σp; simpl. congruence. - destruct (eqb_specT c kn); subst. - - intros [= ->]. - exists ({| universes := univs; declarations := Σ; retroknowledge := retro |}). - split. - * red; cbn. split; [split;[lsets|csets]| |]. - exists [(kn, decl)] => //. - apply Retroknowledge.extends_refl. - * split => //. - * destruct o; assumption. - - intros hl. destruct (IHΣp hl) as [Σ' []]. - exists Σ'. - split=> //. - destruct e as [eu ed]. red; cbn in *. - split; [auto| |auto]. - destruct ed as [Σ'' ->]. - exists (Σ'' ,, (kn, d)) => //. - Qed. - - Lemma All_local_env_app (P : context -> judgment -> Type) l l' : - All_local_env P l * All_local_env (fun Γ j => P (l ,,, Γ) j) l' -> - All_local_env P (l ,,, l'). - Proof using Type. - induction l'; simpl; auto. intuition. - intuition. destruct a. destruct decl_body. - inv b. econstructor; eauto. inv b; econstructor; eauto. - Qed. - - Lemma All_local_env_app_inv (P : context -> judgment -> Type) l l' : - All_local_env P (l ,,, l') -> - All_local_env P l * All_local_env (fun Γ j => P (l ,,, Γ) j) l'. - Proof using Type. - apply All_local_app_rel. - Qed. - - Definition wf_local_rel_app_inv {Σ Γ1 Γ2 Γ3} : - wf_local_rel Σ Γ1 (Γ2 ,,, Γ3) -> - wf_local_rel Σ Γ1 Γ2 * wf_local_rel Σ (Γ1 ,,, Γ2) Γ3. - Proof. - intros h. apply All_local_env_app_inv in h as [h1 h2]. - split. - - exact h1. - - eapply All_local_env_impl. 1: exact h2. - intros. - rewrite <- app_context_assoc. - auto. - Defined. - - Lemma All_local_env_lookup {P Γ n} {decl} : - All_local_env P Γ -> - nth_error Γ n = Some decl -> - on_local_decl P (skipn (S n) Γ) decl. - Proof using Type. - induction 1 in n, decl |- *. simpl. destruct n; simpl; congruence. - destruct n. red. simpl. intros [= <-]. simpl. apply t0. - simpl in *. eapply IHX. - destruct n. simpl. intros [= <-]. auto. - eapply IHX. - Qed. - - Definition wf_local_rel_app {Σ Γ1 Γ2 Γ3} : - wf_local_rel Σ Γ1 Γ2 -> wf_local_rel Σ (Γ1 ,,, Γ2) Γ3 - -> wf_local_rel Σ Γ1 (Γ2 ,,, Γ3). - Proof. - intros h1 h2. eapply All_local_env_app. - split. - - assumption. - - eapply All_local_env_impl. - + eassumption. - + change PCUICEnvironment.app_context with app_context. - intros Γ t []; cbn; - now rewrite app_context_assoc. - Defined. - - Definition wf_local_app {Σ Γ1 Γ2} : - wf_local Σ Γ1 -> - wf_local_rel Σ Γ1 Γ2 -> - wf_local Σ (Γ1 ,,, Γ2). - Proof using Type. - intros H1 H2. apply All_local_env_app. - now split. - Qed. - - Definition wf_local_app_inv {Σ Γ1 Γ2} : - wf_local Σ (Γ1 ,,, Γ2) -> - wf_local Σ Γ1 * wf_local_rel Σ Γ1 Γ2. - Proof using Type. - apply All_local_env_app_inv. - Qed. - - Lemma wf_local_app_ind {Σ Γ1 Γ2} : - wf_local Σ Γ1 -> - (wf_local Σ Γ1 -> wf_local_rel Σ Γ1 Γ2) -> - wf_local Σ (Γ1 ,,, Γ2). - Proof using Type. - intros wf IH. - apply wf_local_app; auto. - Qed. - - Lemma All_local_env_map (P : context -> judgment -> Type) f l : - All_local_env (fun Γ j => P (map (map_decl f) Γ) (judgment_map f j)) l - -> All_local_env P (map (map_decl f) l). - Proof using Type. - induction 1; econstructor; eauto. - Qed. - - Definition property := - forall (Σ : global_env_ext) (Γ : context), - wf_local Σ Γ -> forall t T : term, typing Σ Γ t T -> Type. - - Definition lookup_wf_local {Γ P} (wfΓ : All_local_env P Γ) (n : nat) - (isdecl : n < #|Γ|) : - All_local_env P (skipn (S n) Γ). - Proof. - induction wfΓ in n, isdecl |- *; simpl. constructor. - cbn -[skipn] in *. destruct n. - simpl. exact wfΓ. - apply IHwfΓ. auto with arith. - destruct n. exact wfΓ. - apply IHwfΓ. auto with arith. - Defined. - - Lemma wf_local_app_skipn {Σ Γ Γ' n} : - wf_local Σ (Γ ,,, Γ') -> - wf_local Σ (Γ ,,, skipn n Γ'). - Proof using Type. - intros wf. - destruct (le_dec n #|Γ'|). - unfold app_context. - replace Γ with (skipn (n - #|Γ'|) Γ). - rewrite -skipn_app. now apply All_local_env_skipn. - replace (n - #|Γ'|) with 0 by lia. now rewrite skipn_0. - rewrite List.skipn_all2. lia. - now eapply wf_local_app_l in wf. - Qed. - - Definition lookup_wf_local_decl {Γ P} (wfΓ : All_local_env P Γ) (n : nat) - {decl} (eq : nth_error Γ n = Some decl) : - ∑ Pskip : All_local_env P (skipn (S n) Γ), - on_local_decl P (skipn (S n) Γ) decl. - Proof. - induction wfΓ in n, decl, eq |- *; simpl. - - elimtype False. destruct n; depelim eq. - - destruct n. - + simpl. exists wfΓ. injection eq; intros <-. apply t0. - + apply IHwfΓ. auto with arith. - - destruct n. - + exists wfΓ. injection eq; intros <-. apply t0. - + apply IHwfΓ. apply eq. - Defined. - - Definition on_wf_local_decl {Σ Γ} - (P : forall Σ Γ (wfΓ : wf_local Σ Γ) t T, Σ ;;; Γ |- t : T -> Type) - (wfΓ : wf_local Σ Γ) {d} (H : on_local_decl (lift_typing1 (typing Σ)) Γ d) := - match d as d' return (on_local_decl (lift_typing1 (typing Σ)) Γ d') -> Type with - | {| decl_name := na; decl_body := Some b; decl_type := ty |} - => fun H => P Σ Γ wfΓ b ty H.1 × P Σ Γ wfΓ ty _ H.2.π2.1 - | {| decl_name := na; decl_body := None; decl_type := ty |} - => fun H => P Σ Γ wfΓ ty _ H.2.π2.1 - end H. - - Lemma nth_error_All_local_env_over {P Σ Γ n decl} (eq : nth_error Γ n = Some decl) {wfΓ : wf_local Σ Γ} : - All_local_env_over (typing Σ) (P Σ) Γ wfΓ -> - let Γ' := skipn (S n) Γ in - let p := lookup_wf_local_decl wfΓ n eq in - (All_local_env_over (typing Σ) (P Σ) Γ' (projT1 p) * on_wf_local_decl P (projT1 p) (projT2 p))%type. - Proof. - induction 1 in n, decl, eq |- *. simpl. - - destruct n; simpl; elimtype False; discriminate eq. - - destruct n. cbn [skipn]. noconf eq. split. apply X. simpl. apply Hs. - simpl. apply IHX. - - destruct n. noconf eq. simpl. split; auto. - apply IHX. - Defined. - - Lemma All_local_env_prod_inv : - forall P Q Γ, - All_local_env (fun Δ j => P Δ j × Q Δ j) Γ -> - All_local_env P Γ × All_local_env Q Γ. - Proof using Type. - intros P Q Γ h. - induction h. - - split ; constructor. - - destruct IHh, t0. - split ; constructor ; auto. - - destruct IHh, t0. - split ; constructor ; auto. - Qed. - - Lemma All_local_env_lift_prod_inv : - forall Σ P Q Δ, - All_local_env (lift_typing (fun Σ Γ => Trel_conj (P Σ Γ) (Q Σ Γ)) Σ) Δ -> - All_local_env (lift_typing P Σ) Δ × All_local_env (lift_typing Q Σ) Δ. - Proof using Type. - intros Σ P Q Δ h. - split; apply All_local_env_impl with (1 := h); intros ?? H; apply lift_typing_impl with (1 := H). - all: move => ??[] //. - Qed. - -End All_local_env. diff --git a/pcuic/theories/PCUICValidity.v b/pcuic/theories/PCUICValidity.v index 88e3f0d06..289c52c74 100644 --- a/pcuic/theories/PCUICValidity.v +++ b/pcuic/theories/PCUICValidity.v @@ -86,17 +86,6 @@ Section Validity. now apply isType_weaken. Qed. - Lemma nth_error_All_local_env {P} {Γ n d} : - nth_error Γ n = Some d -> - All_local_env P Γ -> - on_local_decl P (skipn (S n) Γ) d. - Proof using Type. - intros heq hΓ. - epose proof (nth_error_Some_length heq). - eapply (nth_error_All_local_env) in H; tea. - now rewrite heq in H. - Qed. - Notation type_ctx := (type_local_ctx (lift_typing typing)). Lemma type_ctx_wf_univ Σ Γ Δ s : type_ctx Σ Γ Δ s -> wf_universe Σ s. Proof using Type. @@ -206,7 +195,7 @@ Section Validity. - assumption. - (* Rel *) - destruct (nth_error_All_local_env heq_nth_error X) as (_ & s & Hs & _). + destruct (All_local_env_nth_error X heq_nth_error) as (_ & s & Hs & _). eapply isType_lift; eauto. 1: now apply nth_error_Some_length in heq_nth_error. now eapply has_sort_isType. @@ -386,7 +375,7 @@ Lemma wf_local_validity `{cf : checker_flags} {Σ} {wfΣ : wf Σ} Γ Δ : Proof. move=> wfΓΔ. apply: validity_wf_local. - now apply: (wf_local_app_inv _).2. + now apply: (All_local_env_app_inv _).2. Qed. diff --git a/pcuic/theories/Typing/PCUICClosedTyp.v b/pcuic/theories/Typing/PCUICClosedTyp.v index 7792c4781..65b511871 100644 --- a/pcuic/theories/Typing/PCUICClosedTyp.v +++ b/pcuic/theories/Typing/PCUICClosedTyp.v @@ -189,7 +189,7 @@ Proof. - unshelve eapply declared_constant_to_gen in H0; tea. rewrite closedn_subst_instance. eapply lookup_on_global_env in X0; eauto. - destruct X0 as [Σ' [hext [onu HΣ'] [IHtm IHty]]]. + destruct X0 as (Σ' & hext & [onu HΣ'] & [IHtm IHty]). simpl in *. eauto using closed_upwards with arith. @@ -479,7 +479,7 @@ Proof. apply (env_prop_sigma typecheck_closed) in wfΣ. intros h. unshelve eapply declared_constant_to_gen in h; tea. eapply lookup_on_global_env in h. 2: eauto. - destruct h as [Σ' [ext wfΣ' [Htm Hty]]]. + destruct h as (Σ' & ext & wfΣ' & [Htm Hty]). easy. Qed. @@ -495,7 +495,7 @@ Proof. apply (env_prop_sigma typecheck_closed) in hΣ. unshelve eapply declared_constant_to_gen in h; tea. eapply lookup_on_global_env in h. 2: eauto. - destruct h as [Σ' [ext wfΣ' [Htm Hty]]]. + destruct h as (Σ' & ext & wfΣ' & [Htm Hty]). simpl in Htm. rewrite e in Htm. easy. @@ -514,7 +514,7 @@ Proof. destruct h as [h1 h2]. unshelve eapply declared_minductive_to_gen in h1; tea. eapply lookup_on_global_env in h1. 2: eauto. - destruct h1 as [Σ' [ext wfΣ' decl']]. + destruct h1 as (Σ' & ext & wfΣ' & decl'). red in decl'. destruct decl' as [h ? ? ?]. eapply Alli_nth_error in h. 2: eassumption. simpl in h. now destruct h as [? [? h] ? ? ?]. diff --git a/pcuic/theories/Typing/PCUICContextConversionTyp.v b/pcuic/theories/Typing/PCUICContextConversionTyp.v index ffecdef50..479d0d214 100644 --- a/pcuic/theories/Typing/PCUICContextConversionTyp.v +++ b/pcuic/theories/Typing/PCUICContextConversionTyp.v @@ -180,8 +180,7 @@ Proof. - pose proof heq_nth_error. eapply (All2_fold_nth_r X0) in H as [d' [Hnth [Hrel Hconv]]]. - unshelve eapply nth_error_All_local_env in X; tea. 2:eapply nth_error_Some_length in heq_nth_error; lia. - rewrite heq_nth_error /= in X. + eapply All_local_env_nth_error in X; tea. red in X. specialize (X _ Hrel). forward X by now eapply All_local_env_skipn. destruct X as (_ & s & Hty & _). diff --git a/pcuic/theories/Typing/PCUICNamelessTyp.v b/pcuic/theories/Typing/PCUICNamelessTyp.v index e4974c121..9e5d3fcd7 100644 --- a/pcuic/theories/Typing/PCUICNamelessTyp.v +++ b/pcuic/theories/Typing/PCUICNamelessTyp.v @@ -258,7 +258,7 @@ Proof. constructor. + now eapply fix_guard_nl. + now rewrite nth_error_map H0. - + rewrite nlctx_app_context in X. now eapply wf_local_app_inv in X. + + rewrite nlctx_app_context in X. now eapply All_local_env_app_inv in X. + clear -X0. apply All_map. eapply All_impl; tea. simpl. intros x [s Hs]. now exists s. @@ -277,7 +277,7 @@ Proof. constructor; auto. + now apply cofix_guard_nl. + now rewrite nth_error_map H0. - + now rewrite nlctx_app_context in X; apply wf_local_app_inv in X. + + now rewrite nlctx_app_context in X; apply All_local_env_app_inv in X. + clear -X0. apply All_map. eapply All_impl; tea. simpl. intros x [s Hs]. now exists s. diff --git a/pcuic/theories/Typing/PCUICRenameTyp.v b/pcuic/theories/Typing/PCUICRenameTyp.v index 22d1da050..76361cd6b 100644 --- a/pcuic/theories/Typing/PCUICRenameTyp.v +++ b/pcuic/theories/Typing/PCUICRenameTyp.v @@ -609,31 +609,25 @@ Lemma rename_predicate_preturn f p : Proof. reflexivity. Qed. Lemma wf_local_app_renaming P Σ Γ Δ : - All_local_env (lift_typing (fun (Σ : global_env_ext) (Γ' : context) (t T : term) => - forall P (Δ : PCUICEnvironment.context) (f : nat -> nat), - renaming (shiftnP #|Γ ,,, Γ'| P) Σ (Γ ,,, Γ') Δ f -> Σ ;;; Δ |- rename f t : rename f T) Σ) - Δ -> + All_local_rel (lift_typing (fun Σ (Γ : context) (t T : term) => + forall P Δ (f : nat -> nat), + renaming (shiftnP #|Γ| P) Σ Γ Δ f -> + Σ ;;; Δ |- rename f t : rename f T) Σ) + Γ Δ -> forall Δ' f, renaming (shiftnP #|Γ| P) Σ Γ Δ' f -> wf_local Σ (Δ' ,,, rename_context f Δ). Proof. intros. destruct X0. - induction X. - - apply a. - - rewrite rename_context_snoc /=. constructor; auto. - eapply lift_typing_f_impl with (1 := t0) => // ?? Hs. - eapply (Hs P (Δ' ,,, rename_context f Γ0) (shiftn #|Γ0| f)). - split => //. - eapply urenaming_ext. - { now rewrite app_length -shiftnP_add. } - { reflexivity. } now eapply urenaming_context. - - rewrite rename_context_snoc /=. constructor; auto. - eapply lift_typing_f_impl with (1 := t0) => // ?? Hs. - apply (Hs P (Δ' ,,, rename_context f Γ0) (shiftn #|Γ0| f)). - split => //. - eapply urenaming_ext. - { now rewrite app_length -shiftnP_add. } - { reflexivity. } now eapply urenaming_context. + induction X using All_local_rel_ind1. + 1: now apply a. + rewrite rename_context_snoc /=. apply All_local_env_snoc; auto. + eapply lift_typing_f_impl with (1 := X) => // ?? Hs. + eapply (Hs P (Δ' ,,, rename_context f Δ) (shiftn #|Δ| f)). + split; auto. + eapply urenaming_ext. + { now rewrite app_length -shiftnP_add. } + { reflexivity. } now eapply urenaming_context. Qed. Lemma rename_decompose_prod_assum f Γ t : diff --git a/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v b/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v index 66ff4540b..d4c8a9317 100644 --- a/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v +++ b/pcuic/theories/Typing/PCUICUnivSubstitutionTyp.v @@ -330,7 +330,7 @@ Proof using Type. rewrite (map_dtype _ (subst_instance u)). econstructor. + specialize (H1 u univs wfΣ' H2). rewrite subst_instance_app in H1. - now eapply wf_local_app_inv in H1 as []. + now eapply All_local_env_app_inv in H1 as []. + now eapply fix_guard_subst_instance. + rewrite nth_error_map H0. reflexivity. + apply All_map, (All_impl X); simpl. intros d X1. @@ -353,7 +353,7 @@ Proof using Type. rewrite (map_dtype _ (subst_instance u)). econstructor. + specialize (H1 u univs wfΣ' H2). rewrite subst_instance_app in H1. - now eapply wf_local_app_inv in H1 as []. + now eapply All_local_env_app_inv in H1 as []. + now eapply cofix_guard_subst_instance. + rewrite nth_error_map H0. reflexivity. + apply All_map, (All_impl X); simpl. intros d X1. diff --git a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v index 398ee88a8..ac54955cb 100644 --- a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v +++ b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v @@ -109,9 +109,9 @@ Proof. now apply IH. - apply All_local_env_over_2 in X. clear wfΓ. - induction X; constructor; eauto 2 with extends. - all: eapply lift_typing_impl; tea. - all: move => t' T' [] _ IH; now apply IH. + apply All_local_env_impl with (1 := X) => Γ' j Hj. + apply lift_typing_impl with (1 := Hj) => t' T' [] _ IH //. + now apply IH. - econstructor; eauto 2 with extends. now apply extends_wf_universe. - econstructor; eauto 2 with extends. all: econstructor; eauto 2 with extends. @@ -120,7 +120,7 @@ Proof. * close_Forall. intros; intuition eauto with extends. - econstructor; eauto with extends. + specialize (forall_Σ' _ wf0 wfΣ' extΣ). - now apply wf_local_app_inv in forall_Σ'. + now apply All_local_env_app_inv in forall_Σ'. + eapply fix_guard_extends; eauto. + eapply (All_impl X0); intros d X. apply (lift_typing_impl X); now intros ? []. @@ -128,7 +128,7 @@ Proof. apply (lift_typing_impl X); now intros ? []. - econstructor; eauto with extends. + specialize (forall_Σ' _ wf0 wfΣ' extΣ). - now apply wf_local_app_inv in forall_Σ'. + now apply All_local_env_app_inv in forall_Σ'. + eapply cofix_guard_extends; eauto. + eapply (All_impl X0); intros d X. apply (lift_typing_impl X); now intros ? []. diff --git a/pcuic/theories/Typing/PCUICWeakeningTyp.v b/pcuic/theories/Typing/PCUICWeakeningTyp.v index 7f6c8a5ff..9acacf9af 100644 --- a/pcuic/theories/Typing/PCUICWeakeningTyp.v +++ b/pcuic/theories/Typing/PCUICWeakeningTyp.v @@ -29,7 +29,7 @@ Proof. intros wfΓ' wfΓ''. pose proof (env_prop_wf_local typing_rename_prop _ wfΣ _ wfΓ') as [_ X]. simpl in X. eapply All_local_env_app_inv in X as [XΓ XΓ']. - apply wf_local_app => //. + apply All_local_env_app => //. rewrite /lift_context. apply All_local_env_fold. eapply (All_local_env_impl_ind XΓ'). @@ -39,8 +39,8 @@ Proof. rewrite Nat.add_0_r; rewrite !lift_rename. eapply (Hf xpredT). split. - + apply wf_local_app; auto. - apply (All_local_env_fold (fun Δ => lift_typing1 (typing Σ) (Γ ,,, Γ'' ,,, Δ))) in IH. apply IH. + + apply All_local_env_app; auto. + apply All_local_env_fold, IH. + apply weakening_renaming. Qed. @@ -177,11 +177,11 @@ Proof. generalize (@nil context_decl) as Δ. rewrite /fix_context_gen. intros Δ wfΔ. - eapply All_local_env_app. split; auto. + eapply All_local_env_app; auto. induction a in Δ, wfΔ |- *; simpl; auto. + constructor. + simpl. - eapply All_local_env_app. split; auto. + eapply All_local_env_app; auto. * constructor. 1: constructor. apply lift_typing_f_impl with (1 := p) => // ?? Hs. eapply (weakening Σ Γ Δ); auto. diff --git a/safechecker/theories/PCUICSafeChecker.v b/safechecker/theories/PCUICSafeChecker.v index 8645f99d1..7bfa151df 100644 --- a/safechecker/theories/PCUICSafeChecker.v +++ b/safechecker/theories/PCUICSafeChecker.v @@ -798,7 +798,7 @@ Section CheckEnv. unfold arities_context. induction 1; simpl; auto. rewrite rev_map_cons /=. - eapply All_local_env_app; split. constructor; pcuic. + eapply All_local_env_app. constructor; pcuic. eapply All_local_env_impl; eauto. intros Γ j Hj. apply lift_typing_impl with (1 := Hj) => t T HT. diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v index f8daea604..f38b48c7a 100644 --- a/safechecker/theories/PCUICTypeChecker.v +++ b/safechecker/theories/PCUICTypeChecker.v @@ -531,7 +531,7 @@ Section Typecheck. Lemma sq_wf_local_app {Γ Δ} : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ Γ ∥ -> ∥ wf_local_rel Σ Γ Δ ∥ -> ∥ wf_local Σ (Γ ,,, Δ) ∥. Proof using Type. - intros. sq. now apply wf_local_app. + intros. sq. now apply All_local_env_app. Qed. Equations check_context_rel Γ (wfΓ : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ Γ ∥) (Δ : context) : @@ -870,7 +870,7 @@ Section Typecheck. 1: constructor. rewrite subst_empty. apply checking_typing ; auto. - apply wf_local_rel_app_inv in wfΔ as [wt _]. + apply All_local_rel_app_inv in wfΔ as [wt _]. now depelim wt. Qed. Next Obligation. @@ -1967,7 +1967,7 @@ Section Typecheck. - econstructor ; tea. now apply closed_red_red. - now eapply All2_fold_All2 in check_wfpctx_conv. - - now eapply wf_local_rel_wf_local_bd, wf_local_app_inv, wf_case_predicate_context. + - now eapply wf_local_rel_wf_local_bd, All_local_env_app_inv, wf_case_predicate_context. - eapply ctx_inst_typing_bd ; eauto. eapply ctx_inst_smash. now rewrite subst_instance_smash /= in wt_params. @@ -2002,7 +2002,7 @@ Section Typecheck. - now eapply All2_fold_All2. } cbn ; intros ? ? ? [? []] ; intuition auto. - now eapply wf_local_rel_wf_local_bd, wf_local_app_inv. + now eapply wf_local_rel_wf_local_bd, All_local_env_app_inv. Qed. Next Obligation. diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v index 741644b26..913e1a43a 100644 --- a/template-coq/theories/Typing.v +++ b/template-coq/theories/Typing.v @@ -1526,163 +1526,8 @@ Proof. eapply (X _ X0 _ _ Hty). simpl; lia. Qed. -(** * Lemmas about All_local_env *) -(* TODO: Move where All_local_env is defined, in EnvironmentTyping *) - -Lemma nth_error_All_local_env {P Γ n} (isdecl : n < #|Γ|) : - All_local_env P Γ -> - on_some (on_local_decl P (skipn (S n) Γ)) (nth_error Γ n). -Proof. - induction 1 in n, isdecl |- *. red; simpl. - - destruct n; simpl; inv isdecl. - - destruct n. red; simpl. red. simpl. apply t0. - simpl. apply IHX. simpl in isdecl. lia. - - destruct n. auto. - apply IHX. simpl in *. lia. -Qed. - Arguments on_global_env {cf} Pcmp P !g. -Lemma lookup_on_global_env `{checker_flags} {Pcmp P} {Σ : global_env} {c decl} : - on_global_env Pcmp P Σ -> - lookup_env Σ c = Some decl -> - { Σ' : global_env_ext & on_global_env Pcmp P Σ' × strictly_extends_decls Σ' Σ × on_global_decl Pcmp P Σ' c decl }. -Proof. - unfold on_global_env. - destruct Σ as [univs Σ retro]; cbn. intros [cu ond]. - induction ond; cbn in * => //. - destruct o. rename udecl0 into udecl. - case: eqb_specT => [-> [= <-]| ne]. - - exists ({| universes := univs; declarations := Σ; retroknowledge := retro |}, udecl). - split; try constructor; tas. - cbn. split => //=. now exists [(kn, d)]. - - intros hl. - destruct (IHond hl) as [[Σ' udecl'] [ong [[equ ext extretro] ond']]]. - exists (Σ', udecl'). cbn in equ |- *. subst univs. split; cbn; auto; try apply ong. - split; cbn; auto. split; cbn; auto. - cbn in ext. destruct ext as [Σ'' ->]. cbn in *. - now exists ((kn, d) :: Σ''). -Qed. - -Lemma All_local_env_app_inv - (P : context -> judgment -> Type) l l' : - All_local_env P (l ,,, l') -> - All_local_env P l * All_local_env (fun Γ j => P (l ,,, Γ) j) l'. -Proof. - induction l'; simpl; split; auto. - - constructor. - - intros. unfold app_context in X. - inv X. - + intuition auto. - + auto. apply IHl'. auto. - - inv X. - + eapply localenv_cons_abs. - * apply IHl'. apply X0. - * apply X1. - + eapply localenv_cons_def. - * apply IHl'. apply X0. - * apply X1. -Qed. - -Lemma All_local_env_lookup {P Γ n} {decl} : - All_local_env P Γ -> - nth_error Γ n = Some decl -> - on_local_decl P (skipn (S n) Γ) decl. -Proof. - induction 1 in n, decl |- *. - - simpl. destruct n; simpl; congruence. - - destruct n. - + red. simpl. intro HH; apply some_inj in HH; rewrite <- HH; tas. - + apply IHX. - - destruct n. - + red. simpl. intro HH; apply some_inj in HH; rewrite <- HH; tas. - + apply IHX. -Qed. - -Lemma All_local_env_app `{checker_flags} (P : context -> judgment -> Type) l l' : - All_local_env P l * All_local_env (fun Γ j => P (l ,,, Γ) j) l' -> - All_local_env P (l ,,, l'). -Proof. - induction l'; simpl; auto. intuition. - intuition. destruct a. destruct decl_body. - inv b. econstructor; eauto. inv b; econstructor; eauto. Qed. - -Lemma All_local_env_map `{checker_flags} (P : context -> judgment -> Type) f l : - All_local_env (fun Γ j => P (map (map_decl f) Γ) (judgment_map f j)) l -> All_local_env P (map (map_decl f) l). -Proof. - induction 1; econstructor; eauto. -Qed. - -Definition property `{checker_flags} := - forall (Σ : global_env_ext) (Γ : context), - wf_local Σ Γ -> forall t T : term, typing Σ Γ t T -> Type. - -Definition lookup_wf_local {Γ P} (wfΓ : All_local_env P Γ) (n : nat) (isdecl : n < #|Γ|) : - All_local_env P (skipn (S n) Γ). -Proof. - induction wfΓ in n, isdecl |- *; simpl. constructor. - cbn -[skipn] in *. destruct n. - simpl. exact wfΓ. - apply IHwfΓ. auto with arith. - destruct n. exact wfΓ. - apply IHwfΓ. auto with arith. -Defined. - -Definition lookup_wf_local_decl {Γ P} (wfΓ : All_local_env P Γ) (n : nat) - {decl} (eq : nth_error Γ n = Some decl) : - ∑ Pskip : All_local_env P (skipn (S n) Γ), - on_local_decl P (skipn (S n) Γ) decl. -Proof. - induction wfΓ in n, decl, eq |- *; simpl. - - elimtype False. destruct n; inversion eq. - - destruct n. - + simpl. exists wfΓ. injection eq; intros <-. apply t0. - + apply IHwfΓ. auto with arith. - - destruct n. - + exists wfΓ. injection eq; intros <-. apply t0. - + apply IHwfΓ. apply eq. -Defined. - -Definition on_wf_local_decl `{checker_flags} {Σ Γ} - (P : forall Σ Γ (wfΓ : wf_local Σ Γ) t T, Σ ;;; Γ |- t : T -> Type) - (wfΓ : wf_local Σ Γ) {d} - (H : on_local_decl (lift_typing1 (typing Σ)) Γ d) := - match d as d' return (on_local_decl (lift_typing1 (typing Σ)) Γ d') -> Type with - | {| decl_name := na; decl_body := Some b; decl_type := ty |} - => fun H => P Σ Γ wfΓ b ty H.1 × P Σ Γ wfΓ ty _ H.2.π2.1 - | {| decl_name := na; decl_body := None; decl_type := ty |} - => fun H => P Σ Γ wfΓ ty _ H.2.π2.1 - end H. - - -Lemma nth_error_All_local_env_over `{checker_flags} {P Σ Γ n decl} (eq : nth_error Γ n = Some decl) {wfΓ : wf_local Σ Γ} : - All_local_env_over (typing Σ) (P Σ) Γ wfΓ -> - let Γ' := skipn (S n) Γ in - let p := lookup_wf_local_decl wfΓ n eq in - (All_local_env_over (typing Σ) (P Σ) Γ' (projT1 p) * on_wf_local_decl P (projT1 p) (projT2 p))%type. -Proof. - induction 1 in n, decl, eq |- *. simpl. - - destruct n; simpl; elimtype False; discriminate eq. - - destruct n; simpl. - + cbn [skipn]. simpl in *. split; tas. - destruct (f_equal (fun e => match e with - | Some c => c - | None => {| decl_name := na; - decl_body := None; decl_type := t |} - end) eq). - assumption. - + apply IHX. - - destruct n. - + cbn [skipn]. simpl in *. split; tas. - destruct (f_equal (fun e => match e with - | Some c => c - | None => {| decl_name := na; - decl_body := Some b; decl_type := t |} - end) eq). - cbn. split; assumption. - + apply IHX. -Defined. - Definition wf_ext_wf `{checker_flags} Σ : wf_ext Σ -> wf Σ := fst. #[global] diff --git a/template-pcuic/theories/PCUICToTemplateCorrectness.v b/template-pcuic/theories/PCUICToTemplateCorrectness.v index 6816d9dcd..ea69d1105 100644 --- a/template-pcuic/theories/PCUICToTemplateCorrectness.v +++ b/template-pcuic/theories/PCUICToTemplateCorrectness.v @@ -714,7 +714,7 @@ Section wtsub. split. eapply spine_subst_wt in s. now eapply All_rev_inv in s. exists mdecl, idecl. split; auto. now symmetry. - * eapply wf_local_app_inv. eapply wf_local_alpha. + * eapply All_local_env_app_inv. eapply wf_local_alpha. eapply All2_app; [|reflexivity]. eapply alpha_eq_subst_instance. symmetry; tea. eapply wf_ind_predicate; tea. pcuic. @@ -724,7 +724,7 @@ Section wtsub. eapply All2i_All2_mix_left in brs_ty; tea. eapply All2i_nth_hyp in brs_ty. solve_all. split; auto. - { eapply wf_local_app_inv. eapply wf_local_alpha. + { eapply All_local_env_app_inv. eapply wf_local_alpha. eapply All2_app; [|reflexivity]. eapply alpha_eq_subst_instance in a2. symmetry; tea.