Library MetaCoq.Erasure.EDeps
From Coq Require Import Arith List.
From Equations Require Import Equations.
From MetaCoq.PCUIC Require Import
PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
Set Warnings "-notation-overridden".
From MetaCoq.Erasure Require Import EAst EAstUtils ECSubst EInduction
ELiftSubst EGlobalEnv EWcbvEval Extract ESubstitution.
From MetaCoq.Erasure Require EExtends.
Set Warnings "+notation-overridden".
From MetaCoq.Template Require Import config utils monad_utils.
Derive NoConfusion for term.
Derive Signature for erases_deps.
Derive Signature for Forall.
Lemma erases_deps_mkApps Σ Σ' hd args :
erases_deps Σ Σ' hd →
Forall (erases_deps Σ Σ') args →
erases_deps Σ Σ' (mkApps hd args).
Proof.
intros er erall.
induction args using rev_ind; [easy|].
rewrite !mkApps_app.
cbn in ×.
apply Forall_app in erall as (? & ?).
depelim H0.
now constructor.
Qed.
Lemma erases_deps_mkApps_inv Σ Σ' hd args :
erases_deps Σ Σ' (mkApps hd args) →
erases_deps Σ Σ' hd ∧ Forall (erases_deps Σ Σ') args.
Proof.
intros er.
induction args using rev_ind; [easy|].
rewrite mkApps_app in ×.
cbn in ×.
depelim er.
intuition auto.
now apply app_Forall.
Qed.
Lemma erases_deps_lift Σ Σ' n k t :
erases_deps Σ Σ' t →
erases_deps Σ Σ' (lift n k t).
Proof.
intros er.
induction t in k, t, er |- × using EInduction.term_forall_list_ind; cbn in *; auto.
- now destruct (_ <=? _); constructor.
- depelim er.
constructor.
induction H; cbn in *; [easy|].
now depelim X.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
econstructor; eauto.
- depelim er.
econstructor; eauto.
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_subst Σ Σ' s k t :
All (erases_deps Σ Σ') s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (subst s k t).
Proof.
intros aller er.
induction t in k, aller, er |- × using term_forall_list_ind; cbn in *; auto.
- destruct (_ <=? _); [|now constructor].
destruct nth_error eqn:nth; [|now constructor].
eapply All_nth_error in nth; [|now eauto].
now apply erases_deps_lift.
- depelim er.
constructor.
induction H; [simpl; easy|].
depelim X.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
econstructor; eauto.
- depelim er.
econstructor; eauto.
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_subst1 Σ Σ' t k u :
erases_deps Σ Σ' t →
erases_deps Σ Σ' u →
erases_deps Σ Σ' (subst1 t k u).
Proof.
intros.
apply erases_deps_subst; [|easy].
now constructor.
Qed.
Lemma erases_deps_csubst Σ Σ' s k t :
erases_deps Σ Σ' s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (csubst s k t).
Proof.
intros aller er.
induction t in k, aller, er |- × using term_forall_list_ind; cbn in *; auto.
- destruct (_ ?= _); try constructor; easy.
- depelim er.
constructor.
induction H; [simpl; easy|].
depelim X.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
cbn. econstructor; eauto.
- depelim er.
econstructor; [easy|easy|easy|easy|easy|].
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl;easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_substl Σ Σ' s t :
Forall (fun s ⇒ erases_deps Σ Σ' s) s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (substl s t).
Proof.
intros all exp.
unfold substl.
induction s using List.rev_ind; [easy|].
rewrite fold_left_app.
cbn.
apply Forall_app in all as (? & erx).
depelim erx.
now apply erases_deps_csubst.
Qed.
Lemma Forall_erases_deps_fix_subst Σ Σ' defs :
Forall (erases_deps Σ Σ' ∘ dbody) defs →
Forall (erases_deps Σ Σ') (fix_subst defs).
Proof.
intros all.
unfold EGlobalEnv.fix_subst.
induction defs at 2; constructor; cbn in ×.
- now constructor.
- now apply IHl.
Qed.
Lemma Forall_erases_deps_cofix_subst Σ Σ' defs :
Forall (erases_deps Σ Σ' ∘ dbody) defs →
Forall (erases_deps Σ Σ') (EGlobalEnv.cofix_subst defs).
Proof.
intros all.
unfold EGlobalEnv.cofix_subst.
induction defs at 2; constructor; cbn in ×.
- now constructor.
- now apply IHl.
Qed.
Lemma erases_deps_cunfold_fix Σ Σ' defs i narg f :
cunfold_fix defs i = Some (narg, f) →
Forall (fun d ⇒ erases_deps Σ Σ' (dbody d)) defs →
erases_deps Σ Σ' f.
Proof.
intros cuf all.
unfold cunfold_fix in ×.
destruct (nth_error _ _) eqn:nth; [|congruence].
eapply nth_error_forall in nth; [|eassumption].
noconf cuf.
apply erases_deps_substl; [|easy].
now apply Forall_erases_deps_fix_subst.
Qed.
Lemma erases_deps_cunfold_cofix Σ Σ' defs i narg f :
cunfold_cofix defs i = Some (narg, f) →
Forall (fun d ⇒ erases_deps Σ Σ' (dbody d)) defs →
erases_deps Σ Σ' f.
Proof.
intros cuf all.
unfold cunfold_cofix in ×.
destruct (nth_error _ _) eqn:nth; [|congruence].
eapply nth_error_forall in nth; [|eassumption].
noconf cuf.
apply erases_deps_substl; [|easy].
now apply Forall_erases_deps_cofix_subst.
Qed.
Notation "Σ ⊢ s ▷ t" := (eval Σ s t) (at level 50, s, t at next level) : type_scope.
Lemma erases_deps_eval {wfl:WcbvFlags} {hcon : with_constructor_as_block = false} Σ t v Σ' :
Σ' ⊢ t ▷ v →
erases_deps Σ Σ' t →
erases_deps Σ Σ' v.
Proof.
intros ev er.
induction ev in t, v, ev, er |- *; cbn in ×.
- now constructor.
- depelim er.
apply IHev3.
apply erases_deps_csubst; [easy|].
intuition auto.
now depelim H.
- depelim er.
now apply IHev2, erases_deps_csubst.
- depelim er.
apply IHev2.
unfold EGlobalEnv.iota_red.
apply erases_deps_substl.
+ intuition auto.
apply erases_deps_mkApps_inv in H4.
now apply Forall_rev, Forall_skipn.
+ eapply nth_error_forall in e1; [|now eauto].
assumption.
- congruence.
- depelim er.
subst brs; cbn in ×.
depelim H3.
cbn in ×.
apply IHev2.
apply erases_deps_substl; [|easy].
apply All_Forall, All_repeat.
now constructor.
- depelim er.
intuition auto.
eapply erases_deps_mkApps_inv in H as (? & ?).
depelim H.
apply IHev3.
constructor; [|easy].
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_fix.
- depelim er.
intuition auto.
apply erases_deps_mkApps_inv in H as (? & ?).
constructor; [|easy].
now apply erases_deps_mkApps.
- depelim er.
specialize (IHev1 er1).
specialize (IHev2 er2).
eapply IHev3. econstructor; eauto.
eapply erases_deps_cunfold_fix; eauto.
now depelim IHev1.
- depelim er.
specialize (IHev1 er).
apply erases_deps_mkApps_inv in IHev1 as (? & ?).
depelim H4.
apply IHev2.
econstructor; [easy|easy|easy|easy| |easy].
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_cofix; eauto.
- depelim er.
specialize (IHev1 er).
apply erases_deps_mkApps_inv in IHev1 as (? & ?).
depelim H3.
apply IHev2.
econstructor; eauto.
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_cofix.
- depelim er.
now apply IHev, H2.
- depelim er.
intuition auto.
apply erases_deps_mkApps_inv in H3 as (? & ?).
apply IHev2.
now eapply nth_error_forall in e2.
- congruence.
- constructor.
- depelim er.
now constructor.
- congruence.
- depelim er. now constructor.
- easy.
Qed.
#[global]
Hint Resolve erases_deps_eval erases_deps_subst erases_deps_subst1 : core.
Local Existing Instance config.extraction_checker_flags.
Lemma erases_deps_forall_ind Σ Σ'
(P : Extract.E.term → Prop)
(Hbox : P Extract.E.tBox)
(Hrel : ∀ i : nat, P (Extract.E.tRel i))
(Hvar : ∀ n : ident, P (Extract.E.tVar n))
(Hevar :
∀ (m : nat) (l : list Extract.E.term),
Forall P l →
Forall (erases_deps Σ Σ') l → P (Extract.E.tEvar m l))
(Hlam : ∀ (na : name) (body : Extract.E.term),
erases_deps Σ Σ' body → P body → P (Extract.E.tLambda na body))
(Hletin : ∀ (na : name) (val body : Extract.E.term),
erases_deps Σ Σ' val →
P val → erases_deps Σ Σ' body → P body → P (Extract.E.tLetIn na val body))
(Happ : ∀ hd arg : Extract.E.term,
erases_deps Σ Σ' hd → P hd → erases_deps Σ Σ' arg → P arg → P (Extract.E.tApp hd arg))
(Hconst : ∀ (kn : kername) (cb : PCUICAst.PCUICEnvironment.constant_body) (cb' : EAst.constant_body),
PCUICAst.declared_constant Σ kn cb →
EGlobalEnv.declared_constant Σ' kn cb' →
erases_constant_body (Σ, cst_universes cb) cb cb' →
(∀ body : Extract.E.term, Extract.E.cst_body cb' = Some body → erases_deps Σ Σ' body) →
(∀ body : Extract.E.term, Extract.E.cst_body cb' = Some body → P body) →
P (Extract.E.tConst kn))
(Hconstruct : ∀ (ind : inductive) (c : nat) mdecl idecl cdecl mdecl' idecl' cdecl',
PCUICAst.declared_constructor Σ (ind, c) mdecl idecl cdecl →
declared_constructor Σ' (ind, c) mdecl' idecl' cdecl' →
erases_one_inductive_body idecl idecl' →
erases_mutual_inductive_body mdecl mdecl' →
P (Extract.E.tConstruct ind c []))
(Hcase : ∀ (p : inductive × nat) mdecl idecl mdecl' idecl' (discr : Extract.E.term) (brs : list (list name × Extract.E.term)),
PCUICAst.declared_inductive Σ (fst p) mdecl idecl →
EGlobalEnv.declared_inductive Σ' (fst p) mdecl' idecl' →
erases_mutual_inductive_body mdecl mdecl' →
erases_one_inductive_body idecl idecl' →
erases_deps Σ Σ' discr →
P discr →
Forall (fun br : _ × Extract.E.term ⇒ erases_deps Σ Σ' br.2) brs →
Forall (fun br ⇒ P br.2) brs →
P (Extract.E.tCase p discr brs))
(Hproj : ∀ (p : projection) mdecl idecl cdecl pdecl mdecl' idecl' cdecl' pdecl' (t : Extract.E.term),
PCUICAst.declared_projection Σ p mdecl idecl cdecl pdecl →
EGlobalEnv.declared_projection Σ' p mdecl' idecl' cdecl' pdecl' →
erases_mutual_inductive_body mdecl mdecl' →
erases_one_inductive_body idecl idecl' →
erases_deps Σ Σ' t → P t → P (Extract.E.tProj p t))
(Hfix : ∀ (defs : list (Extract.E.def Extract.E.term)) (i : nat),
Forall (fun d : Extract.E.def Extract.E.term ⇒ erases_deps Σ Σ' (Extract.E.dbody d)) defs →
Forall (fun d ⇒ P (E.dbody d)) defs →
P (Extract.E.tFix defs i))
(Hcofix : ∀ (defs : list (Extract.E.def Extract.E.term)) (i : nat),
Forall (fun d : Extract.E.def Extract.E.term ⇒ erases_deps Σ Σ' (Extract.E.dbody d)) defs →
Forall (fun d ⇒ P (E.dbody d)) defs →
P (Extract.E.tCoFix defs i)) :
∀ t, erases_deps Σ Σ' t → P t.
Proof.
fix f 2.
intros t ed.
move f at top.
destruct ed;
try solve [match goal with
| [H: _ |- _] ⇒ apply H
end; auto].
- apply Hevar; [|assumption].
revert l H.
fix f' 2.
intros l [].
+ now constructor.
+ constructor; [now apply f|now apply f'].
- eapply Hconst; try eassumption.
intros.
apply f.
now apply H2.
- eauto.
- eapply Hcase; try eassumption.
+ now apply f.
+ revert brs H3.
fix f' 2.
intros brs []; [now constructor|].
constructor; [now apply f|now apply f'].
- eapply Hproj; try eassumption.
now apply f.
- eapply Hfix; try assumption.
revert defs H.
fix f' 2.
intros defs []; [now constructor|].
constructor; [now apply f|now apply f'].
- apply Hcofix; try assumption.
revert defs H.
fix f' 2.
intros defs []; [now constructor|].
constructor; [now apply f|now apply f'].
Defined.
Lemma erases_deps_cons Σ Σ' kn decl decl' t :
on_global_univs Σ.(universes) →
on_global_decls cumulSpec0 (lift_typing typing) Σ.(universes) ((kn, decl) :: Σ.(declarations)) →
erases_deps Σ Σ' t →
erases_deps (add_global_decl Σ (kn, decl)) ((kn, decl') :: Σ') t.
Proof.
intros wfu wfΣ er.
induction er using erases_deps_forall_ind; try solve [now constructor].
apply PCUICWeakeningEnv.lookup_env_Some_fresh in H as not_fresh.
econstructor.
- unfold PCUICAst.declared_constant in *; cbn.
inversion wfΣ; subst.
destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
eassumption.
- unfold EGlobalEnv.declared_constant in ×. cbn -[ReflectEq.eqb].
inversion wfΣ; subst.
destruct (ReflectEq.eqb_spec kn0 kn); [congruence|].
eassumption.
- unfold erases_constant_body in ×.
destruct PCUICAst.PCUICEnvironment.cst_body eqn:body.
+ destruct E.cst_body eqn:ebody; [|easy].
assert (PCUICAst.declared_constant (add_global_decl Σ (kn, decl)) kn0 cb).
{ unfold PCUICAst.declared_constant.
cbn.
inversion wfΣ; subst.
destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
easy. }
inversion wfΣ; subst.
eapply declared_constant_inv in H4; eauto.
2:eapply weaken_env_prop_typing.
red in H4.
rewrite body in ×.
cbn in ×.
eapply (erases_extends (_, cst_universes cb)); cbn. 5:tea.
1,3,5,6:constructor; auto.
2:{ split; auto. eexists [_]; reflexivity. }
eapply declared_constant_inv in H.
2:eapply weaken_env_prop_typing.
2: easy.
2: easy.
unfold on_constant_decl in H.
rewrite body in ×.
apply H.
+ now destruct E.cst_body.
- easy.
- econstructor; eauto. eapply weakening_env_declared_constructor; eauto with pcuic; tc.
{ eapply extends_decls_extends. econstructor; try reflexivity. eexists [(_, _)]; reflexivity. }
invs wfΣ.
destruct H0. split. 2: eauto.
destruct d. split; eauto.
red. cbn. cbn in ×.
destruct (eqb_spec (inductive_mind ind) kn). cbn in ×.
subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H5. eauto. eapply H. exact H0.
- econstructor; eauto.
destruct H as [H H'].
split; eauto. red in H |- ×.
inv wfΣ.
unfold PCUICEnvironment.lookup_env.
simpl. destruct (eqb_spec (inductive_mind p.1) kn); auto. subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H; eauto. contradiction.
destruct H0 as [H0 H0'].
split; eauto. red in H0 |- ×.
inv wfΣ. cbn. change (eq_kername (inductive_mind p.1) kn) with (ReflectEq.eqb (inductive_mind p.1) kn).
destruct (ReflectEq.eqb_spec (inductive_mind p.1) kn); auto. subst.
destruct H as [H _].
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H. eauto. contradiction.
- econstructor; eauto.
destruct H as [[[declm decli] declc] [declp hp]].
repeat split; eauto.
inv wfΣ. unfold PCUICAst.declared_minductive in ×.
unfold PCUICEnvironment.lookup_env.
simpl in ×.
destruct (ReflectEq.eqb_spec (inductive_mind p.(proj_ind)) kn). subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in declm; eauto. contradiction.
apply declm.
destruct H0 as [[[]]]. destruct a.
repeat split; eauto.
inv wfΣ. simpl. unfold declared_minductive. cbn.
destruct (ReflectEq.eqb_spec (inductive_mind p.(proj_ind)) kn); auto. subst.
destruct H as [[[]]].
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H. eauto. contradiction.
Qed.
Derive Signature for erases_global_decls.
Derive Signature for Forall2.
Definition globals_erased_with_deps Σ Σ' :=
(∀ k cst,
PCUICAst.declared_constant Σ k cst →
∃ cst',
EGlobalEnv.declared_constant Σ' k cst' ∧
erases_constant_body (Σ, cst_universes cst) cst cst' ∧
(∀ body, cst_body cst' = Some body → erases_deps Σ Σ' body)) ∧
(∀ k mdecl idecl,
PCUICAst.declared_inductive Σ k mdecl idecl →
∃ mdecl' idecl',
EGlobalEnv.declared_inductive Σ' k mdecl' idecl' ∧
erases_mutual_inductive_body mdecl mdecl').
Lemma erases_declared_constructor {Σ : global_env_ext} Σ' kn k mind idecl cdecl :
PCUICAst.declared_constructor Σ.1 (kn, k) mind idecl cdecl →
globals_erased_with_deps Σ Σ' →
∃ mind' idecl',
declared_constructor Σ' (kn, k) mind' idecl' (mkConstructor (PCUICEnvironment.cstr_name cdecl) (PCUICEnvironment.cstr_arity cdecl)) ∧
erases_one_inductive_body idecl idecl' ∧
erases_mutual_inductive_body mind mind'.
Proof.
intros [Hcon1 Hcon2] H.
eapply H in Hcon1 as Hcon3. destruct Hcon3 as (mdecl' & idecl' & H1 & H2).
pose proof H2 as H2'.
destruct H1. destruct H2. cbn in ×.
destruct Hcon1 as [Hcon1 Hcon3]. red in Hcon1.
eapply Forall2_nth_error_Some_l in H2 as (? & ? & ?); eauto.
rewrite H2 in H1. invs H1. pose proof H4 as H4'.
destruct H4 as (? & ? & ? & ? & ?).
eapply Forall2_nth_error_Some_l in H1 as ([] & ? & ? & ?); subst; eauto.
eexists. eexists. split; [ | split]; eauto.
repeat eapply conj; try eassumption. cbn in ×. now rewrite H8, H9.
Qed.
Lemma erases_deps_single Σ Σ' Γ t T et :
wf_ext Σ →
Σ;;; Γ |- t : T →
Σ;;; Γ |- t ⇝ℇ et →
globals_erased_with_deps Σ Σ' →
erases_deps Σ Σ' et.
Proof.
intros wf wt er Σer.
induction er in er, t, T, wf, wt |- × using erases_forall_list_ind;
cbn in *; try solve [constructor].
- now apply inversion_Evar in wt.
- constructor.
now apply inversion_Lambda in wt as (? & ? & ? & ? & ?); eauto.
- apply inversion_LetIn in wt as (? & ? & ? & ? & ? & ?); eauto.
now constructor; eauto.
- apply inversion_App in wt as (? & ? & ? & ? & ? & ?); eauto.
now constructor; eauto.
- apply inversion_Const in wt as (? & ? & ? & ? & ?); eauto.
apply Σer in d as d'; destruct d' as (? & ? & ? & ?).
now econstructor; eauto.
- eapply inversion_Construct in wt as (? & ? & ? & ? & ? & ? & ?); eauto.
pose proof d as d'. destruct d'.
destruct (proj2 Σer _ _ _ H0) as (? & ? & ? & ? & ?).
edestruct @erases_declared_constructor as (? & ? & ? & ? & ?); eauto.
econstructor; eauto.
- apply inversion_Case in wt as (? & ? & ? & ? & [] & ?); eauto.
destruct (proj2 Σer _ _ _ x1) as (? & ? & ? & ?).
econstructor; eauto.
destruct H2. destruct x1; eauto. destruct H1.
eapply Forall2_All2 in H2. eapply All2_nth_error in H2; eauto.
clear -wf brs_ty X H0 Σer.
subst predctx ptm.
clear X.
revert brs_ty brs' H0 Σer.
generalize (PCUICEnvironment.ind_ctors x0).
induction 1; intros er deps.
{ now depelim er. }
depelim deps.
destruct r0 as (? & ? & ? & ?).
intros er.
constructor; eauto. eapply H; auto.
now rewrite <-(PCUICCasesContexts.inst_case_branch_context_eq a).
- apply inversion_Proj in wt as (?&?&?&?&?&?&?&?&?&?); eauto.
destruct (proj2 Σer _ _ _ (proj1 (proj1 d))) as (? & ? & ? & ?).
destruct d as [[[declm decli] declc] [declp hp]].
set (H1' := H1). destruct H1'.
eapply Forall2_All2 in H2. eapply All2_nth_error_Some in H2 as [bod' [hnth' ebod']]; eauto.
set (H1' := ebod'). destruct H1' as [Hctors [Hprojs _]].
eapply Forall2_All2 in Hctors. eapply All2_nth_error_Some in Hctors as [ctor' [hnth'' [Hctor' Hctor'']]]; eauto.
eapply Forall2_All2 in Hprojs. eapply All2_nth_error_Some in Hprojs as [proj' [hnthp ?]]; eauto.
econstructor; eauto. repeat split; eauto.
repeat split; eauto. cbn. apply H0. now rewrite <- H3, hp.
- constructor.
apply inversion_Fix in wt as (?&?&?&?&?&?&?); eauto.
clear -wf a0 X H Σer.
revert a0 X H Σer.
generalize mfix at 1 2 4 6.
intros mfix_gen.
revert mfix'.
induction mfix; cbn in *; intros mfix' typ er all_deps deps.
{ now depelim er. }
depelim typ.
depelim er.
depelim all_deps.
destruct a0 as [? ? ? ?].
now constructor; eauto.
- constructor.
apply inversion_CoFix in wt as (?&?&?&?&?&?&?); eauto.
clear -wf a0 X H Σer.
revert a0 X H Σer.
generalize mfix at 1 2 4 6.
intros mfix_gen.
revert mfix'.
induction mfix; cbn in *; intros mfix' typ er all_deps deps.
{ now depelim er. }
depelim typ.
depelim er.
depelim all_deps.
destruct p as (?&?&?).
now constructor; eauto.
Qed.
Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' →
∀ n x, nth_error l n = Some x →
∃ x', nth_error l' n = Some x' ∧ P x x'.
Proof.
induction 1; destruct n; simpl; auto; try discriminate.
intros x' [= ->]. eexists; eauto.
Qed.
Lemma erases_global_all_deps Σ Σ' :
wf Σ →
erases_global Σ Σ' →
globals_erased_with_deps Σ Σ'.
Proof.
intros wf erg.
set (Σg := Σ). destruct Σ as [univs Σ]; cbn in ×.
induction Σ as [|(kn, decl) Σ IH] in Σ', Σg, wf, erg |- *; cbn in ×.
- depelim erg.
split; [intros ? ? decl; discriminate decl|].
intros ? ? ? [decl _]; discriminate decl.
- split.
intros kn' cst' decl'.
destruct (eq_dec kn kn') as [<-|].
+ unfold PCUICAst.declared_constant, EGlobalEnv.declared_constant in *; cbn in ×.
rewrite eq_kername_refl in ×.
noconf decl'.
depelim erg.
∃ cb'.
cbn. rewrite eq_kername_refl.
split; [easy|].
inversion wf; subst.
cbn in ×.
split.
× unfold erases_constant_body, on_constant_decl in ×.
destruct ?; [|easy].
destruct ?; [|easy].
depelim wf. depelim o0. cbn in ×.
eapply (erases_extends ({| universes := univs; declarations := Σ |}, cst_universes cst')); eauto.
cbn. 4:{ split; eauto; cbn; try reflexivity. eexists [_]; cbn; reflexivity. }
constructor; auto. cbn. red in o2. rewrite E in o2. exact o2.
split; auto.
× intros.
eapply (erases_deps_cons {| universes := univs; declarations := Σ |} _ kn (PCUICEnvironment.ConstantDecl cst')); auto.
unfold erases_constant_body in ×.
rewrite H1 in ×.
destruct ?; [|easy].
unfold on_constant_decl in ×.
cbn in ×.
eapply (erases_deps_single (_, _)). 3:eauto.
depelim wf. depelim o0.
now split; cbn; eauto.
depelim wf. depelim o0. do 2 red in o2. now rewrite E in o2.
apply IH; eauto. depelim wf. now depelim o0.
+ set (Σu := {| universes := univs; declarations := Σ |}).
assert (wfΣu : PCUICTyping.wf Σu).
{ depelim wf. now depelim o0. }
assert (∃ decl' Σ'', Σ' = (kn, decl') :: Σ'' ∧ erases_global Σu Σ'')
as (erdecl & ? & → & erg')
by now depelim erg; eexists _, _.
apply IH in erg'. 2:{ depelim wf. now depelim o0. }
assert (decl_ext: PCUICAst.declared_constant Σu kn' cst').
{ unfold PCUICAst.declared_constant in *; cbn in ×.
destruct (eqb_spec kn' kn); [|congruence]. subst. contradiction. }
specialize (proj1 erg' kn' cst' decl_ext) as (cst & decl'' & ? & ?).
∃ cst.
split; [|split].
× unfold declared_constant in *; cbn. rewrite decl''.
change (eq_kername kn' kn) with (ReflectEq.eqb kn' kn).
destruct (ReflectEq.eqb_spec kn' kn); auto. congruence.
× inversion wf; subst.
eapply declared_constant_inv in decl_ext; eauto.
2: exact weaken_env_prop_typing.
unfold on_constant_decl, erases_constant_body in ×.
destruct ?; [|easy].
destruct ?; [|easy].
eapply (erases_extends (Σu, cst_universes cst')).
4:{ split; cbn; auto. eexists [_]; cbn; reflexivity. }
all: cbn; eauto.
× intros.
apply H0 in H1.
eapply (erases_deps_cons Σu); eauto. apply wfΣu. apply wf.
+ intros k mdecl idecl decli.
depelim erg.
× inv wf. inv X.
specialize (IH _ (H0, X0) erg).
apply proj2 in IH. specialize (IH k mdecl idecl).
forward IH.
destruct decli as [decli ?]. split; auto.
red in decli |- ×. simpl in decli |- ×.
unfold PCUICEnvironment.lookup_env in decli |- ×. simpl in ×.
destruct (eqb_spec (inductive_mind k) kn). subst. discriminate. auto.
destruct IH as [mdecl' [idecl' [decli' er]]].
∃ mdecl', idecl'. split; auto.
red. destruct decli'; split; auto.
red in decli.
unfold declared_minductive in ×.
simpl. destruct (eqb_spec (inductive_mind k) kn); subst; auto.
unfold PCUICAst.declared_minductive in decli.
unfold PCUICEnvironment.lookup_env in decli.
simpl in decli. rewrite eq_kername_refl in decli. intuition discriminate.
× inv wf. inv X.
specialize (IH _ (H0, X0) erg).
destruct decli as [decli ?].
simpl in decli |- ×.
unfold PCUICAst.declared_minductive, PCUICEnvironment.lookup_env in decli.
simpl in decli.
destruct (eqb_specT (inductive_mind k) kn). simpl in ×. subst. noconf decli.
destruct (Forall2_nth_error_left (proj1 H) _ _ H3); eauto.
eexists _, _; intuition eauto. split; eauto. red.
simpl. rewrite eqb_refl. congruence.
destruct (proj2 IH _ _ _ (conj decli H3)) as [m' [i' [decli' ei]]].
eexists _, _; intuition eauto.
destruct decli'; red; split; eauto.
red in d |- ×. simpl.
apply neqb in n. destruct eqb; cbn in n; try congruence.
Qed.
Lemma erases_global_erases_deps Σ Γ t T et Σ' :
wf_ext Σ →
Σ;;; Γ |- t : T →
Σ;;; Γ |- t ⇝ℇ et →
erases_global Σ Σ' →
erases_deps Σ Σ' et.
Proof.
intros.
eapply erases_deps_single; eauto.
now eapply erases_global_all_deps.
Qed.
From Equations Require Import Equations.
From MetaCoq.PCUIC Require Import
PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
Set Warnings "-notation-overridden".
From MetaCoq.Erasure Require Import EAst EAstUtils ECSubst EInduction
ELiftSubst EGlobalEnv EWcbvEval Extract ESubstitution.
From MetaCoq.Erasure Require EExtends.
Set Warnings "+notation-overridden".
From MetaCoq.Template Require Import config utils monad_utils.
Derive NoConfusion for term.
Derive Signature for erases_deps.
Derive Signature for Forall.
Lemma erases_deps_mkApps Σ Σ' hd args :
erases_deps Σ Σ' hd →
Forall (erases_deps Σ Σ') args →
erases_deps Σ Σ' (mkApps hd args).
Proof.
intros er erall.
induction args using rev_ind; [easy|].
rewrite !mkApps_app.
cbn in ×.
apply Forall_app in erall as (? & ?).
depelim H0.
now constructor.
Qed.
Lemma erases_deps_mkApps_inv Σ Σ' hd args :
erases_deps Σ Σ' (mkApps hd args) →
erases_deps Σ Σ' hd ∧ Forall (erases_deps Σ Σ') args.
Proof.
intros er.
induction args using rev_ind; [easy|].
rewrite mkApps_app in ×.
cbn in ×.
depelim er.
intuition auto.
now apply app_Forall.
Qed.
Lemma erases_deps_lift Σ Σ' n k t :
erases_deps Σ Σ' t →
erases_deps Σ Σ' (lift n k t).
Proof.
intros er.
induction t in k, t, er |- × using EInduction.term_forall_list_ind; cbn in *; auto.
- now destruct (_ <=? _); constructor.
- depelim er.
constructor.
induction H; cbn in *; [easy|].
now depelim X.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
econstructor; eauto.
- depelim er.
econstructor; eauto.
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_subst Σ Σ' s k t :
All (erases_deps Σ Σ') s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (subst s k t).
Proof.
intros aller er.
induction t in k, aller, er |- × using term_forall_list_ind; cbn in *; auto.
- destruct (_ <=? _); [|now constructor].
destruct nth_error eqn:nth; [|now constructor].
eapply All_nth_error in nth; [|now eauto].
now apply erases_deps_lift.
- depelim er.
constructor.
induction H; [simpl; easy|].
depelim X.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
econstructor; eauto.
- depelim er.
econstructor; eauto.
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_subst1 Σ Σ' t k u :
erases_deps Σ Σ' t →
erases_deps Σ Σ' u →
erases_deps Σ Σ' (subst1 t k u).
Proof.
intros.
apply erases_deps_subst; [|easy].
now constructor.
Qed.
Lemma erases_deps_csubst Σ Σ' s k t :
erases_deps Σ Σ' s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (csubst s k t).
Proof.
intros aller er.
induction t in k, aller, er |- × using term_forall_list_ind; cbn in *; auto.
- destruct (_ ?= _); try constructor; easy.
- depelim er.
constructor.
induction H; [simpl; easy|].
depelim X.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
now constructor.
- depelim er.
cbn. econstructor; eauto.
- depelim er.
econstructor; [easy|easy|easy|easy|easy|].
induction X; [easy|].
depelim H3.
constructor; [|easy].
now cbn.
- depelim er.
now econstructor.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl;easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
- depelim er.
constructor.
induction H in k, H, X |- *; [simpl; easy|].
cbn in ×.
rewrite <- !Nat.add_succ_r.
depelim X.
constructor; [|easy].
now apply e.
Qed.
Lemma erases_deps_substl Σ Σ' s t :
Forall (fun s ⇒ erases_deps Σ Σ' s) s →
erases_deps Σ Σ' t →
erases_deps Σ Σ' (substl s t).
Proof.
intros all exp.
unfold substl.
induction s using List.rev_ind; [easy|].
rewrite fold_left_app.
cbn.
apply Forall_app in all as (? & erx).
depelim erx.
now apply erases_deps_csubst.
Qed.
Lemma Forall_erases_deps_fix_subst Σ Σ' defs :
Forall (erases_deps Σ Σ' ∘ dbody) defs →
Forall (erases_deps Σ Σ') (fix_subst defs).
Proof.
intros all.
unfold EGlobalEnv.fix_subst.
induction defs at 2; constructor; cbn in ×.
- now constructor.
- now apply IHl.
Qed.
Lemma Forall_erases_deps_cofix_subst Σ Σ' defs :
Forall (erases_deps Σ Σ' ∘ dbody) defs →
Forall (erases_deps Σ Σ') (EGlobalEnv.cofix_subst defs).
Proof.
intros all.
unfold EGlobalEnv.cofix_subst.
induction defs at 2; constructor; cbn in ×.
- now constructor.
- now apply IHl.
Qed.
Lemma erases_deps_cunfold_fix Σ Σ' defs i narg f :
cunfold_fix defs i = Some (narg, f) →
Forall (fun d ⇒ erases_deps Σ Σ' (dbody d)) defs →
erases_deps Σ Σ' f.
Proof.
intros cuf all.
unfold cunfold_fix in ×.
destruct (nth_error _ _) eqn:nth; [|congruence].
eapply nth_error_forall in nth; [|eassumption].
noconf cuf.
apply erases_deps_substl; [|easy].
now apply Forall_erases_deps_fix_subst.
Qed.
Lemma erases_deps_cunfold_cofix Σ Σ' defs i narg f :
cunfold_cofix defs i = Some (narg, f) →
Forall (fun d ⇒ erases_deps Σ Σ' (dbody d)) defs →
erases_deps Σ Σ' f.
Proof.
intros cuf all.
unfold cunfold_cofix in ×.
destruct (nth_error _ _) eqn:nth; [|congruence].
eapply nth_error_forall in nth; [|eassumption].
noconf cuf.
apply erases_deps_substl; [|easy].
now apply Forall_erases_deps_cofix_subst.
Qed.
Notation "Σ ⊢ s ▷ t" := (eval Σ s t) (at level 50, s, t at next level) : type_scope.
Lemma erases_deps_eval {wfl:WcbvFlags} {hcon : with_constructor_as_block = false} Σ t v Σ' :
Σ' ⊢ t ▷ v →
erases_deps Σ Σ' t →
erases_deps Σ Σ' v.
Proof.
intros ev er.
induction ev in t, v, ev, er |- *; cbn in ×.
- now constructor.
- depelim er.
apply IHev3.
apply erases_deps_csubst; [easy|].
intuition auto.
now depelim H.
- depelim er.
now apply IHev2, erases_deps_csubst.
- depelim er.
apply IHev2.
unfold EGlobalEnv.iota_red.
apply erases_deps_substl.
+ intuition auto.
apply erases_deps_mkApps_inv in H4.
now apply Forall_rev, Forall_skipn.
+ eapply nth_error_forall in e1; [|now eauto].
assumption.
- congruence.
- depelim er.
subst brs; cbn in ×.
depelim H3.
cbn in ×.
apply IHev2.
apply erases_deps_substl; [|easy].
apply All_Forall, All_repeat.
now constructor.
- depelim er.
intuition auto.
eapply erases_deps_mkApps_inv in H as (? & ?).
depelim H.
apply IHev3.
constructor; [|easy].
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_fix.
- depelim er.
intuition auto.
apply erases_deps_mkApps_inv in H as (? & ?).
constructor; [|easy].
now apply erases_deps_mkApps.
- depelim er.
specialize (IHev1 er1).
specialize (IHev2 er2).
eapply IHev3. econstructor; eauto.
eapply erases_deps_cunfold_fix; eauto.
now depelim IHev1.
- depelim er.
specialize (IHev1 er).
apply erases_deps_mkApps_inv in IHev1 as (? & ?).
depelim H4.
apply IHev2.
econstructor; [easy|easy|easy|easy| |easy].
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_cofix; eauto.
- depelim er.
specialize (IHev1 er).
apply erases_deps_mkApps_inv in IHev1 as (? & ?).
depelim H3.
apply IHev2.
econstructor; eauto.
apply erases_deps_mkApps; [|easy].
now eapply erases_deps_cunfold_cofix.
- depelim er.
now apply IHev, H2.
- depelim er.
intuition auto.
apply erases_deps_mkApps_inv in H3 as (? & ?).
apply IHev2.
now eapply nth_error_forall in e2.
- congruence.
- constructor.
- depelim er.
now constructor.
- congruence.
- depelim er. now constructor.
- easy.
Qed.
#[global]
Hint Resolve erases_deps_eval erases_deps_subst erases_deps_subst1 : core.
Local Existing Instance config.extraction_checker_flags.
Lemma erases_deps_forall_ind Σ Σ'
(P : Extract.E.term → Prop)
(Hbox : P Extract.E.tBox)
(Hrel : ∀ i : nat, P (Extract.E.tRel i))
(Hvar : ∀ n : ident, P (Extract.E.tVar n))
(Hevar :
∀ (m : nat) (l : list Extract.E.term),
Forall P l →
Forall (erases_deps Σ Σ') l → P (Extract.E.tEvar m l))
(Hlam : ∀ (na : name) (body : Extract.E.term),
erases_deps Σ Σ' body → P body → P (Extract.E.tLambda na body))
(Hletin : ∀ (na : name) (val body : Extract.E.term),
erases_deps Σ Σ' val →
P val → erases_deps Σ Σ' body → P body → P (Extract.E.tLetIn na val body))
(Happ : ∀ hd arg : Extract.E.term,
erases_deps Σ Σ' hd → P hd → erases_deps Σ Σ' arg → P arg → P (Extract.E.tApp hd arg))
(Hconst : ∀ (kn : kername) (cb : PCUICAst.PCUICEnvironment.constant_body) (cb' : EAst.constant_body),
PCUICAst.declared_constant Σ kn cb →
EGlobalEnv.declared_constant Σ' kn cb' →
erases_constant_body (Σ, cst_universes cb) cb cb' →
(∀ body : Extract.E.term, Extract.E.cst_body cb' = Some body → erases_deps Σ Σ' body) →
(∀ body : Extract.E.term, Extract.E.cst_body cb' = Some body → P body) →
P (Extract.E.tConst kn))
(Hconstruct : ∀ (ind : inductive) (c : nat) mdecl idecl cdecl mdecl' idecl' cdecl',
PCUICAst.declared_constructor Σ (ind, c) mdecl idecl cdecl →
declared_constructor Σ' (ind, c) mdecl' idecl' cdecl' →
erases_one_inductive_body idecl idecl' →
erases_mutual_inductive_body mdecl mdecl' →
P (Extract.E.tConstruct ind c []))
(Hcase : ∀ (p : inductive × nat) mdecl idecl mdecl' idecl' (discr : Extract.E.term) (brs : list (list name × Extract.E.term)),
PCUICAst.declared_inductive Σ (fst p) mdecl idecl →
EGlobalEnv.declared_inductive Σ' (fst p) mdecl' idecl' →
erases_mutual_inductive_body mdecl mdecl' →
erases_one_inductive_body idecl idecl' →
erases_deps Σ Σ' discr →
P discr →
Forall (fun br : _ × Extract.E.term ⇒ erases_deps Σ Σ' br.2) brs →
Forall (fun br ⇒ P br.2) brs →
P (Extract.E.tCase p discr brs))
(Hproj : ∀ (p : projection) mdecl idecl cdecl pdecl mdecl' idecl' cdecl' pdecl' (t : Extract.E.term),
PCUICAst.declared_projection Σ p mdecl idecl cdecl pdecl →
EGlobalEnv.declared_projection Σ' p mdecl' idecl' cdecl' pdecl' →
erases_mutual_inductive_body mdecl mdecl' →
erases_one_inductive_body idecl idecl' →
erases_deps Σ Σ' t → P t → P (Extract.E.tProj p t))
(Hfix : ∀ (defs : list (Extract.E.def Extract.E.term)) (i : nat),
Forall (fun d : Extract.E.def Extract.E.term ⇒ erases_deps Σ Σ' (Extract.E.dbody d)) defs →
Forall (fun d ⇒ P (E.dbody d)) defs →
P (Extract.E.tFix defs i))
(Hcofix : ∀ (defs : list (Extract.E.def Extract.E.term)) (i : nat),
Forall (fun d : Extract.E.def Extract.E.term ⇒ erases_deps Σ Σ' (Extract.E.dbody d)) defs →
Forall (fun d ⇒ P (E.dbody d)) defs →
P (Extract.E.tCoFix defs i)) :
∀ t, erases_deps Σ Σ' t → P t.
Proof.
fix f 2.
intros t ed.
move f at top.
destruct ed;
try solve [match goal with
| [H: _ |- _] ⇒ apply H
end; auto].
- apply Hevar; [|assumption].
revert l H.
fix f' 2.
intros l [].
+ now constructor.
+ constructor; [now apply f|now apply f'].
- eapply Hconst; try eassumption.
intros.
apply f.
now apply H2.
- eauto.
- eapply Hcase; try eassumption.
+ now apply f.
+ revert brs H3.
fix f' 2.
intros brs []; [now constructor|].
constructor; [now apply f|now apply f'].
- eapply Hproj; try eassumption.
now apply f.
- eapply Hfix; try assumption.
revert defs H.
fix f' 2.
intros defs []; [now constructor|].
constructor; [now apply f|now apply f'].
- apply Hcofix; try assumption.
revert defs H.
fix f' 2.
intros defs []; [now constructor|].
constructor; [now apply f|now apply f'].
Defined.
Lemma erases_deps_cons Σ Σ' kn decl decl' t :
on_global_univs Σ.(universes) →
on_global_decls cumulSpec0 (lift_typing typing) Σ.(universes) ((kn, decl) :: Σ.(declarations)) →
erases_deps Σ Σ' t →
erases_deps (add_global_decl Σ (kn, decl)) ((kn, decl') :: Σ') t.
Proof.
intros wfu wfΣ er.
induction er using erases_deps_forall_ind; try solve [now constructor].
apply PCUICWeakeningEnv.lookup_env_Some_fresh in H as not_fresh.
econstructor.
- unfold PCUICAst.declared_constant in *; cbn.
inversion wfΣ; subst.
destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
eassumption.
- unfold EGlobalEnv.declared_constant in ×. cbn -[ReflectEq.eqb].
inversion wfΣ; subst.
destruct (ReflectEq.eqb_spec kn0 kn); [congruence|].
eassumption.
- unfold erases_constant_body in ×.
destruct PCUICAst.PCUICEnvironment.cst_body eqn:body.
+ destruct E.cst_body eqn:ebody; [|easy].
assert (PCUICAst.declared_constant (add_global_decl Σ (kn, decl)) kn0 cb).
{ unfold PCUICAst.declared_constant.
cbn.
inversion wfΣ; subst.
destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
easy. }
inversion wfΣ; subst.
eapply declared_constant_inv in H4; eauto.
2:eapply weaken_env_prop_typing.
red in H4.
rewrite body in ×.
cbn in ×.
eapply (erases_extends (_, cst_universes cb)); cbn. 5:tea.
1,3,5,6:constructor; auto.
2:{ split; auto. eexists [_]; reflexivity. }
eapply declared_constant_inv in H.
2:eapply weaken_env_prop_typing.
2: easy.
2: easy.
unfold on_constant_decl in H.
rewrite body in ×.
apply H.
+ now destruct E.cst_body.
- easy.
- econstructor; eauto. eapply weakening_env_declared_constructor; eauto with pcuic; tc.
{ eapply extends_decls_extends. econstructor; try reflexivity. eexists [(_, _)]; reflexivity. }
invs wfΣ.
destruct H0. split. 2: eauto.
destruct d. split; eauto.
red. cbn. cbn in ×.
destruct (eqb_spec (inductive_mind ind) kn). cbn in ×.
subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H5. eauto. eapply H. exact H0.
- econstructor; eauto.
destruct H as [H H'].
split; eauto. red in H |- ×.
inv wfΣ.
unfold PCUICEnvironment.lookup_env.
simpl. destruct (eqb_spec (inductive_mind p.1) kn); auto. subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H; eauto. contradiction.
destruct H0 as [H0 H0'].
split; eauto. red in H0 |- ×.
inv wfΣ. cbn. change (eq_kername (inductive_mind p.1) kn) with (ReflectEq.eqb (inductive_mind p.1) kn).
destruct (ReflectEq.eqb_spec (inductive_mind p.1) kn); auto. subst.
destruct H as [H _].
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H. eauto. contradiction.
- econstructor; eauto.
destruct H as [[[declm decli] declc] [declp hp]].
repeat split; eauto.
inv wfΣ. unfold PCUICAst.declared_minductive in ×.
unfold PCUICEnvironment.lookup_env.
simpl in ×.
destruct (ReflectEq.eqb_spec (inductive_mind p.(proj_ind)) kn). subst.
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in declm; eauto. contradiction.
apply declm.
destruct H0 as [[[]]]. destruct a.
repeat split; eauto.
inv wfΣ. simpl. unfold declared_minductive. cbn.
destruct (ReflectEq.eqb_spec (inductive_mind p.(proj_ind)) kn); auto. subst.
destruct H as [[[]]].
eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H. eauto. contradiction.
Qed.
Derive Signature for erases_global_decls.
Derive Signature for Forall2.
Definition globals_erased_with_deps Σ Σ' :=
(∀ k cst,
PCUICAst.declared_constant Σ k cst →
∃ cst',
EGlobalEnv.declared_constant Σ' k cst' ∧
erases_constant_body (Σ, cst_universes cst) cst cst' ∧
(∀ body, cst_body cst' = Some body → erases_deps Σ Σ' body)) ∧
(∀ k mdecl idecl,
PCUICAst.declared_inductive Σ k mdecl idecl →
∃ mdecl' idecl',
EGlobalEnv.declared_inductive Σ' k mdecl' idecl' ∧
erases_mutual_inductive_body mdecl mdecl').
Lemma erases_declared_constructor {Σ : global_env_ext} Σ' kn k mind idecl cdecl :
PCUICAst.declared_constructor Σ.1 (kn, k) mind idecl cdecl →
globals_erased_with_deps Σ Σ' →
∃ mind' idecl',
declared_constructor Σ' (kn, k) mind' idecl' (mkConstructor (PCUICEnvironment.cstr_name cdecl) (PCUICEnvironment.cstr_arity cdecl)) ∧
erases_one_inductive_body idecl idecl' ∧
erases_mutual_inductive_body mind mind'.
Proof.
intros [Hcon1 Hcon2] H.
eapply H in Hcon1 as Hcon3. destruct Hcon3 as (mdecl' & idecl' & H1 & H2).
pose proof H2 as H2'.
destruct H1. destruct H2. cbn in ×.
destruct Hcon1 as [Hcon1 Hcon3]. red in Hcon1.
eapply Forall2_nth_error_Some_l in H2 as (? & ? & ?); eauto.
rewrite H2 in H1. invs H1. pose proof H4 as H4'.
destruct H4 as (? & ? & ? & ? & ?).
eapply Forall2_nth_error_Some_l in H1 as ([] & ? & ? & ?); subst; eauto.
eexists. eexists. split; [ | split]; eauto.
repeat eapply conj; try eassumption. cbn in ×. now rewrite H8, H9.
Qed.
Lemma erases_deps_single Σ Σ' Γ t T et :
wf_ext Σ →
Σ;;; Γ |- t : T →
Σ;;; Γ |- t ⇝ℇ et →
globals_erased_with_deps Σ Σ' →
erases_deps Σ Σ' et.
Proof.
intros wf wt er Σer.
induction er in er, t, T, wf, wt |- × using erases_forall_list_ind;
cbn in *; try solve [constructor].
- now apply inversion_Evar in wt.
- constructor.
now apply inversion_Lambda in wt as (? & ? & ? & ? & ?); eauto.
- apply inversion_LetIn in wt as (? & ? & ? & ? & ? & ?); eauto.
now constructor; eauto.
- apply inversion_App in wt as (? & ? & ? & ? & ? & ?); eauto.
now constructor; eauto.
- apply inversion_Const in wt as (? & ? & ? & ? & ?); eauto.
apply Σer in d as d'; destruct d' as (? & ? & ? & ?).
now econstructor; eauto.
- eapply inversion_Construct in wt as (? & ? & ? & ? & ? & ? & ?); eauto.
pose proof d as d'. destruct d'.
destruct (proj2 Σer _ _ _ H0) as (? & ? & ? & ? & ?).
edestruct @erases_declared_constructor as (? & ? & ? & ? & ?); eauto.
econstructor; eauto.
- apply inversion_Case in wt as (? & ? & ? & ? & [] & ?); eauto.
destruct (proj2 Σer _ _ _ x1) as (? & ? & ? & ?).
econstructor; eauto.
destruct H2. destruct x1; eauto. destruct H1.
eapply Forall2_All2 in H2. eapply All2_nth_error in H2; eauto.
clear -wf brs_ty X H0 Σer.
subst predctx ptm.
clear X.
revert brs_ty brs' H0 Σer.
generalize (PCUICEnvironment.ind_ctors x0).
induction 1; intros er deps.
{ now depelim er. }
depelim deps.
destruct r0 as (? & ? & ? & ?).
intros er.
constructor; eauto. eapply H; auto.
now rewrite <-(PCUICCasesContexts.inst_case_branch_context_eq a).
- apply inversion_Proj in wt as (?&?&?&?&?&?&?&?&?&?); eauto.
destruct (proj2 Σer _ _ _ (proj1 (proj1 d))) as (? & ? & ? & ?).
destruct d as [[[declm decli] declc] [declp hp]].
set (H1' := H1). destruct H1'.
eapply Forall2_All2 in H2. eapply All2_nth_error_Some in H2 as [bod' [hnth' ebod']]; eauto.
set (H1' := ebod'). destruct H1' as [Hctors [Hprojs _]].
eapply Forall2_All2 in Hctors. eapply All2_nth_error_Some in Hctors as [ctor' [hnth'' [Hctor' Hctor'']]]; eauto.
eapply Forall2_All2 in Hprojs. eapply All2_nth_error_Some in Hprojs as [proj' [hnthp ?]]; eauto.
econstructor; eauto. repeat split; eauto.
repeat split; eauto. cbn. apply H0. now rewrite <- H3, hp.
- constructor.
apply inversion_Fix in wt as (?&?&?&?&?&?&?); eauto.
clear -wf a0 X H Σer.
revert a0 X H Σer.
generalize mfix at 1 2 4 6.
intros mfix_gen.
revert mfix'.
induction mfix; cbn in *; intros mfix' typ er all_deps deps.
{ now depelim er. }
depelim typ.
depelim er.
depelim all_deps.
destruct a0 as [? ? ? ?].
now constructor; eauto.
- constructor.
apply inversion_CoFix in wt as (?&?&?&?&?&?&?); eauto.
clear -wf a0 X H Σer.
revert a0 X H Σer.
generalize mfix at 1 2 4 6.
intros mfix_gen.
revert mfix'.
induction mfix; cbn in *; intros mfix' typ er all_deps deps.
{ now depelim er. }
depelim typ.
depelim er.
depelim all_deps.
destruct p as (?&?&?).
now constructor; eauto.
Qed.
Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' →
∀ n x, nth_error l n = Some x →
∃ x', nth_error l' n = Some x' ∧ P x x'.
Proof.
induction 1; destruct n; simpl; auto; try discriminate.
intros x' [= ->]. eexists; eauto.
Qed.
Lemma erases_global_all_deps Σ Σ' :
wf Σ →
erases_global Σ Σ' →
globals_erased_with_deps Σ Σ'.
Proof.
intros wf erg.
set (Σg := Σ). destruct Σ as [univs Σ]; cbn in ×.
induction Σ as [|(kn, decl) Σ IH] in Σ', Σg, wf, erg |- *; cbn in ×.
- depelim erg.
split; [intros ? ? decl; discriminate decl|].
intros ? ? ? [decl _]; discriminate decl.
- split.
intros kn' cst' decl'.
destruct (eq_dec kn kn') as [<-|].
+ unfold PCUICAst.declared_constant, EGlobalEnv.declared_constant in *; cbn in ×.
rewrite eq_kername_refl in ×.
noconf decl'.
depelim erg.
∃ cb'.
cbn. rewrite eq_kername_refl.
split; [easy|].
inversion wf; subst.
cbn in ×.
split.
× unfold erases_constant_body, on_constant_decl in ×.
destruct ?; [|easy].
destruct ?; [|easy].
depelim wf. depelim o0. cbn in ×.
eapply (erases_extends ({| universes := univs; declarations := Σ |}, cst_universes cst')); eauto.
cbn. 4:{ split; eauto; cbn; try reflexivity. eexists [_]; cbn; reflexivity. }
constructor; auto. cbn. red in o2. rewrite E in o2. exact o2.
split; auto.
× intros.
eapply (erases_deps_cons {| universes := univs; declarations := Σ |} _ kn (PCUICEnvironment.ConstantDecl cst')); auto.
unfold erases_constant_body in ×.
rewrite H1 in ×.
destruct ?; [|easy].
unfold on_constant_decl in ×.
cbn in ×.
eapply (erases_deps_single (_, _)). 3:eauto.
depelim wf. depelim o0.
now split; cbn; eauto.
depelim wf. depelim o0. do 2 red in o2. now rewrite E in o2.
apply IH; eauto. depelim wf. now depelim o0.
+ set (Σu := {| universes := univs; declarations := Σ |}).
assert (wfΣu : PCUICTyping.wf Σu).
{ depelim wf. now depelim o0. }
assert (∃ decl' Σ'', Σ' = (kn, decl') :: Σ'' ∧ erases_global Σu Σ'')
as (erdecl & ? & → & erg')
by now depelim erg; eexists _, _.
apply IH in erg'. 2:{ depelim wf. now depelim o0. }
assert (decl_ext: PCUICAst.declared_constant Σu kn' cst').
{ unfold PCUICAst.declared_constant in *; cbn in ×.
destruct (eqb_spec kn' kn); [|congruence]. subst. contradiction. }
specialize (proj1 erg' kn' cst' decl_ext) as (cst & decl'' & ? & ?).
∃ cst.
split; [|split].
× unfold declared_constant in *; cbn. rewrite decl''.
change (eq_kername kn' kn) with (ReflectEq.eqb kn' kn).
destruct (ReflectEq.eqb_spec kn' kn); auto. congruence.
× inversion wf; subst.
eapply declared_constant_inv in decl_ext; eauto.
2: exact weaken_env_prop_typing.
unfold on_constant_decl, erases_constant_body in ×.
destruct ?; [|easy].
destruct ?; [|easy].
eapply (erases_extends (Σu, cst_universes cst')).
4:{ split; cbn; auto. eexists [_]; cbn; reflexivity. }
all: cbn; eauto.
× intros.
apply H0 in H1.
eapply (erases_deps_cons Σu); eauto. apply wfΣu. apply wf.
+ intros k mdecl idecl decli.
depelim erg.
× inv wf. inv X.
specialize (IH _ (H0, X0) erg).
apply proj2 in IH. specialize (IH k mdecl idecl).
forward IH.
destruct decli as [decli ?]. split; auto.
red in decli |- ×. simpl in decli |- ×.
unfold PCUICEnvironment.lookup_env in decli |- ×. simpl in ×.
destruct (eqb_spec (inductive_mind k) kn). subst. discriminate. auto.
destruct IH as [mdecl' [idecl' [decli' er]]].
∃ mdecl', idecl'. split; auto.
red. destruct decli'; split; auto.
red in decli.
unfold declared_minductive in ×.
simpl. destruct (eqb_spec (inductive_mind k) kn); subst; auto.
unfold PCUICAst.declared_minductive in decli.
unfold PCUICEnvironment.lookup_env in decli.
simpl in decli. rewrite eq_kername_refl in decli. intuition discriminate.
× inv wf. inv X.
specialize (IH _ (H0, X0) erg).
destruct decli as [decli ?].
simpl in decli |- ×.
unfold PCUICAst.declared_minductive, PCUICEnvironment.lookup_env in decli.
simpl in decli.
destruct (eqb_specT (inductive_mind k) kn). simpl in ×. subst. noconf decli.
destruct (Forall2_nth_error_left (proj1 H) _ _ H3); eauto.
eexists _, _; intuition eauto. split; eauto. red.
simpl. rewrite eqb_refl. congruence.
destruct (proj2 IH _ _ _ (conj decli H3)) as [m' [i' [decli' ei]]].
eexists _, _; intuition eauto.
destruct decli'; red; split; eauto.
red in d |- ×. simpl.
apply neqb in n. destruct eqb; cbn in n; try congruence.
Qed.
Lemma erases_global_erases_deps Σ Γ t T et Σ' :
wf_ext Σ →
Σ;;; Γ |- t : T →
Σ;;; Γ |- t ⇝ℇ et →
erases_global Σ Σ' →
erases_deps Σ Σ' et.
Proof.
intros.
eapply erases_deps_single; eauto.
now eapply erases_global_all_deps.
Qed.