Merge pull request #761 from MetaCoq/port-globenv-changes-8.15

Port globenv changes 8.15
MetaCoq · Sep 22, 2022 · 0f2c6b7 · 0f2c6b7
2 parents 7acb6d7 + 02763e7
commit 0f2c6b7
Show file tree

Hide file tree

Showing 27 changed files with 274 additions and 305 deletions.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
@@ -473,11 +473,11 @@ Proof.
   apply PCUICWeakeningEnv.lookup_env_Some_fresh in H as not_fresh.
   econstructor.
   - unfold PCUICAst.declared_constant in *; cbn.
-    inversion wfΣ; subst.
+    inversion wfΣ; subst. destruct X0. 
     destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
     eassumption.
   - unfold EGlobalEnv.declared_constant in *. cbn -[ReflectEq.eqb].
-    inversion wfΣ; subst.
+    inversion wfΣ; subst. destruct X0.
     destruct (ReflectEq.eqb_spec kn0 kn); [congruence|].
     eassumption.
   - unfold erases_constant_body in *.
@@ -486,10 +486,10 @@ Proof.
       assert (PCUICAst.declared_constant (add_global_decl Σ (kn, decl)) kn0 cb).
       { unfold PCUICAst.declared_constant.
         cbn.
-        inversion wfΣ; subst.
+        inversion wfΣ; subst. destruct X0.
         destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
         easy. }
-      inversion wfΣ; subst.
+      inversion wfΣ; subst. destruct X0.
       eapply declared_constant_inv in H4; eauto.
       2:eapply weaken_env_prop_typing.
       red in H4.
@@ -512,35 +512,35 @@ Proof.
     invs wfΣ.
     destruct H0. split. 2: eauto.
     destruct d. split; eauto.
-    red. cbn. cbn in *.
+    red. cbn. cbn in *. destruct X0.
     destruct (eqb_spec (inductive_mind ind) kn). cbn in *.
     subst. 
-    eapply PCUICWeakeningEnv.lookup_env_Some_fresh in H5. eauto. eapply H. exact H0.
+    eapply PCUICWeakeningEnv.lookup_env_Some_fresh in kn_fresh. eauto. eapply H. exact H0.
   - econstructor; eauto.
     destruct H as [H H'].
     split; eauto. red in H |- *.
-    inv wfΣ.
+    inv wfΣ. destruct X0.
     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).    
+    inv wfΣ. destruct X0. 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 *.
+    inv wfΣ. destruct X0. 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.
+    inv wfΣ. destruct X0. 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.
@@ -703,10 +703,10 @@ Proof.
       * unfold erases_constant_body, on_constant_decl in *.
         destruct ?; [|easy].
         destruct ?; [|easy].
-        depelim wf. depelim o0. cbn in *.
+        depelim wf. depelim o0. destruct o1. 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.
+        constructor; auto. cbn. red in on_global_decl_d. rewrite E in on_global_decl_d. exact on_global_decl_d.
         split; auto. 
       * intros.
         eapply (erases_deps_cons {| universes := univs; declarations := Σ |} _ kn (PCUICEnvironment.ConstantDecl cst')); auto.
@@ -716,9 +716,9 @@ Proof.
         unfold on_constant_decl in *.
         cbn in *.
         eapply (erases_deps_single (_, _)). 3:eauto.
-        depelim wf. depelim o0.
+        depelim wf. depelim o0. destruct o1.
         now split; cbn; eauto.
-        depelim wf. depelim o0. do 2 red in o2. now rewrite E in o2.
+        depelim wf. depelim o0. destruct o1. do 2 red in on_global_decl_d. now rewrite E in on_global_decl_d.
         apply IH; eauto. depelim wf. now depelim o0.
     + set (Σu := {| universes := univs; declarations := Σ; retroknowledge := retro |}).
       assert (wfΣu : PCUICTyping.wf Σu).
@@ -767,17 +767,17 @@ Proof.
       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.
+    * inv wf. inv X. destruct X1.
       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.
+      destruct (Forall2_nth_error_left (proj1 H) _ _ H1); eauto.
       eexists _, _; intuition eauto. split; eauto. red.
       simpl. rewrite eqb_refl. congruence.
-      destruct (proj2 IH _ _ _ (conj decli H3)) as [m' [i' [decli' ei]]].
+      destruct (proj2 IH _ _ _ (conj decli H1)) as [m' [i' [decli' ei]]].
       eexists _, _; intuition eauto.
       destruct decli'; red; split; eauto.
       red in d |- *. simpl.

diff --git a/erasure/theories/ETransform.v b/erasure/theories/ETransform.v
@@ -25,7 +25,7 @@ Program Definition erase_pcuic_program {guard : abstract_guard_impl} (p : pcuic_
   (wt : ∥ ∑ T, PCUICTyping.typing (H := config.extraction_checker_flags) p.1 [] p.2 T ∥) : eprogram_env :=
   let wfe := build_wf_env_from_env p.1.1 (map_squash (PCUICTyping.wf_ext_wf _) wfΣ) in
   let wfext := optim_make_wf_env_ext (guard:=guard) wfe p.1.2 _ in
-  let t := ErasureFunction.erase (nor:=PCUICSN.extraction_normalizing) optimized_abstract_env_ext_impl wfext nil p.2
+  let t := ErasureFunction.erase (nor:=PCUICSN.extraction_normalizing) optimized_abstract_env_impl wfext nil p.2
     (fun Σ wfΣ => let '(sq (T; ty)) := wt in PCUICTyping.iswelltyped ty) in
   let Σ' := ErasureFunction.erase_global_fast optimized_abstract_env_impl
     (EAstUtils.term_global_deps t) wfe (p.1.(PCUICAst.PCUICEnvironment.declarations)) _ in
@@ -39,7 +39,7 @@ Qed.
 Obligation Tactic := idtac.
 
 Import Extract.
-  
+
 Definition erase_program {guard : abstract_guard_impl} (p : pcuic_program) 
   (wtp : ∥ wt_pcuic_program (cf:=config.extraction_checker_flags) p ∥) : eprogram_env :=
   erase_pcuic_program (guard := guard) p (map_squash fst wtp) (map_squash snd wtp).
@@ -52,8 +52,8 @@ Proof.
   intros [etaenv etat]. split;
   unfold erase_program, erase_pcuic_program; cbn.
   eapply ErasureFunction.expanded_erase_global_fast, etaenv; reflexivity.
-  eapply (ErasureFunction.expanded_erase_fast (X_type:=optimized_abstract_env_impl)).
-  reflexivity. eapply etat.
+  apply: (ErasureFunction.expanded_erase_fast (X_type:=optimized_abstract_env_impl)).
+  reflexivity. exact etat.
 Qed.
 
 Lemma expanded_eprogram_env_expanded_eprogram_cstrs p :
@@ -83,7 +83,7 @@ Next Obligation.
   - unfold erase_program, erase_pcuic_program in e. simpl. cbn in e. injection e. intros <- <-.
     split. 
     eapply ErasureFunction.erase_global_fast_wf_glob.
-    eapply (ErasureFunction.erase_wellformed_fast (X_type:=optimized_abstract_env_impl)).
+    apply: (ErasureFunction.erase_wellformed_fast (X_type:=optimized_abstract_env_impl)).
   - rewrite -e. cbn.
     now eapply expanded_erase_program.
 Qed.

diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
@@ -1136,10 +1136,10 @@ Proof.
   induction er; intros wf.
   - constructor.
   - cbn. destruct cb' as [[]].
-    cbn in *. depelim wf. 
+    cbn in *. depelim wf. destruct o. 
     rewrite [forallb _ _](IHer wf) andb_true_r.
     red in H. destruct cb as [ty []]; cbn in *.
-    unshelve eapply PCUICClosedTyp.subject_closed in o0. cbn. split; auto.
+    unshelve eapply PCUICClosedTyp.subject_closed in on_global_decl_d. cbn. split; auto.
     eapply erases_closed in H; tea. elim H.
     cbn. apply IHer. now depelim wf.
   - depelim wf.
@@ -1194,11 +1194,11 @@ Proof.
   move: wf. red in er; cbn in er.
   induction er; intros wf.
   - constructor.
-  - cbn. depelim wf.
+  - cbn. depelim wf. destruct o. 
     constructor; eauto.
     2:eapply erases_global_decls_fresh; tea.
     cbn. red in H.
-    do 2 red in o0.
+    do 2 red in on_global_decl_d.
     destruct (cst_body cb).
     destruct (E.cst_body cb') => //. cbn.
     set (Σ'' := ({| universes := _ |}, _)) in *.
@@ -1209,7 +1209,7 @@ Proof.
     specialize (H0 H Σ'). eapply H0.
     eapply erases_global_all_deps; tea. split => //.
     destruct (E.cst_body cb') => //. 
-  - depelim wf.
+  - depelim wf. destruct o. 
     constructor; eauto.
     now eapply erases_mutual_inductive_body_wf.
     now eapply erases_global_decls_fresh; tea.