Merge pull request #793 from MetaCoq/more-abstract-environment

remove direct access to the environment and more compact interface
MetaCoq · Dec 1, 2022 · ca64d72 · ca64d72
2 parents 48f47f8 + 10deba0
commit ca64d72
Show file tree

Hide file tree

Showing 48 changed files with 727 additions and 678 deletions.
diff --git a/erasure/_PluginProject.in b/erasure/_PluginProject.in
@@ -38,8 +38,8 @@ src/pCUICAstUtils.mli
 # src/eqDecInstances.mli
 # src/pCUICReduction.ml
 # src/pCUICReduction.mli
-src/pCUICEquality.mli
-src/pCUICEquality.ml
+# src/pCUICEquality.mli
+# src/pCUICEquality.ml
 src/pCUICTyping.ml
 src/pCUICTyping.mli
 src/pCUICPosition.mli

diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v
@@ -841,7 +841,7 @@ Proof.
   unfold isPropositional.
   eapply PCUICValidity.inversion_mkApps in HT as (? & ? & ?); auto.
   eapply inversion_Construct in t as (? & ? & ? & ? & ? & ? & ?); auto.
-  rewrite (declared_inductive_lookup d).
+  unfold lookup_inductive. rewrite (declared_inductive_lookup d.p1).
   destruct (on_declared_constructor d).
   destruct p as [onind oib].
   rewrite oib.(ind_arity_eq).
@@ -876,7 +876,7 @@ Proof.
   pose proof d as [decli ?].
   destruct (on_declared_constructor d).
   destruct p as [onind oib].
-  red. rewrite (declared_inductive_lookup decli).
+  red. unfold lookup_inductive. rewrite (declared_inductive_lookup decli).
   rewrite oib.(ind_arity_eq).
   rewrite /isPropositionalArity !destArity_it_mkProd_or_LetIn /=.
   destruct (is_propositional (ind_sort x0)) eqn:isp; auto.
@@ -921,7 +921,7 @@ Lemma isPropositional_propositional Σ (Σ' : E.global_context) ind mdecl idecl
 Proof.
   intros decli decli' [_ indp] [] b.
   unfold isPropositional, EGlobalEnv.inductive_isprop_and_pars.
-  rewrite (declared_inductive_lookup decli).
+  unfold lookup_inductive. rewrite (declared_inductive_lookup decli).
   rewrite (EGlobalEnv.declared_inductive_lookup decli') /=
     /isPropositionalArity.
   destruct H0 as [_ [_ [_ isP]]]. red in isP.

diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
@@ -472,7 +472,7 @@ Proof.
   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.
+  - unfold PCUICAst.declared_constant, PCUICAst.declared_constant_gen in *; cbn.
     inversion wfΣ; subst. destruct X0.
     destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
     eassumption.
@@ -484,7 +484,7 @@ Proof.
     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.
+      { unfold PCUICAst.declared_constant, declared_constant_gen.
         cbn.
         inversion wfΣ; subst. destruct X0.
         destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
@@ -532,7 +532,7 @@ Proof.
   - econstructor; eauto.
     destruct H as [[[declm decli] declc] [declp hp]].
     repeat split; eauto.
-    inv wfΣ. destruct X0. unfold PCUICAst.declared_minductive in *.
+    inv wfΣ. destruct X0. unfold PCUICAst.declared_minductive, declared_minductive_gen in *.
     unfold PCUICEnvironment.lookup_env.
     simpl in *.
     destruct (ReflectEq.eqb_spec (inductive_mind p.(proj_ind)) kn). subst.
@@ -690,7 +690,7 @@ Proof.
   - split.
     intros kn' cst' decl'.
     destruct (eq_dec kn kn') as [<-|].
-    + unfold PCUICAst.declared_constant, EGlobalEnv.declared_constant in *; cbn in *.
+    + unfold PCUICAst.declared_constant, declared_constant_gen, EGlobalEnv.declared_constant in *; cbn in *.
       rewrite eq_kername_refl in *.
       noconf decl'.
       depelim erg.
@@ -728,7 +728,7 @@ Proof.
           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 *.
+      { unfold PCUICAst.declared_constant, declared_constant_gen in *; cbn in *.
         destruct (eqb_spec kn' kn); [|congruence]. subst. contradiction. }
       specialize (proj1 erg' kn' cst' decl_ext) as (cst & decl'' & ? & ?).
       exists cst.
@@ -764,14 +764,14 @@ Proof.
       red in decli.
       unfold declared_minductive in *.
       simpl. destruct (eqb_spec (inductive_mind k) kn); subst; auto.
-      unfold PCUICAst.declared_minductive in decli.
+      unfold declared_inductive_gen, declared_minductive_gen in decli.
       unfold PCUICEnvironment.lookup_env in decli.
       simpl in decli. rewrite eq_kername_refl in decli. intuition discriminate.
     * 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.
+      unfold declared_minductive_gen, 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) _ _ H1); eauto.

diff --git a/erasure/theories/ESubstitution.v b/erasure/theories/ESubstitution.v
@@ -59,7 +59,7 @@ Proof.
 
   eapply weakening_env_declared_inductive in H; eauto; tc.
   destruct H, H1.
-  unfold PCUICAst.declared_minductive in *.
+  unfold PCUICAst.declared_minductive, declared_minductive_gen in *.
 
   eapply PCUICWeakeningEnv.extends_lookup in H1; eauto; tc.
   2:{ cbn. apply extends_refl. }
@@ -80,10 +80,11 @@ Proof.
   all: try now (econstructor; eauto).
   all: try now (econstructor; eapply Is_type_extends; eauto; tc).
   - econstructor.
-    red. red in H4. rewrite (PCUICAst.declared_inductive_lookup isdecl) in H4.
+    red. red in H4. unfold PCUICAst.lookup_inductive in H4. 
+    rewrite (PCUICAst.declared_inductive_lookup isdecl.p1) in H4.
     destruct isdecl as [decli declc].
     eapply PCUICWeakeningEnv.weakening_env_declared_inductive in decli; tea; eauto; tc.
-    now rewrite (PCUICAst.declared_inductive_lookup decli).
+    unfold PCUICAst.lookup_inductive. now rewrite (PCUICAst.declared_inductive_lookup decli).
   - econstructor. all:eauto.
     eapply Informative_extends; eauto.
     eapply All2i_All2_All2; tea. cbv beta.
@@ -93,7 +94,7 @@ Proof.
     eapply e; tea.
     now rewrite [_.1](PCUICCasesContexts.inst_case_branch_context_eq a).
   - econstructor. destruct isdecl. 2:eauto.
-    eapply Informative_extends; eauto. exact H.
+    eapply Informative_extends; eauto. exact H.p1.
   - econstructor.
     eapply All2_All_mix_left in X1; eauto.
     eapply All2_impl. exact X1.

diff --git a/erasure/theories/ETransform.v b/erasure/theories/ETransform.v
@@ -6,7 +6,7 @@ From MetaCoq.Template Require Pretty Environment Typing WcbvEval EtaExpand.
 Set Warnings "-notation-overridden".
 From MetaCoq.PCUIC Require PCUICAst PCUICAstUtils PCUICProgram PCUICTransform.
 Set Warnings "+notation-overridden".
-From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnvImpl.
+From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl.
 From MetaCoq.Erasure Require EAstUtils ErasureFunction ErasureCorrectness Extract
    EOptimizePropDiscr ERemoveParams EProgram.
 
@@ -24,7 +24,7 @@ Program Definition erase_pcuic_program {guard : abstract_guard_impl} (p : pcuic_
   (wfΣ : ∥ PCUICTyping.wf_ext (H := config.extraction_checker_flags) p.1 ∥)
   (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 wfext := @abstract_make_wf_env_ext _ optimized_abstract_env_impl wfe p.1.2 _ in
   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

diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
@@ -187,7 +187,7 @@ Proof.
     pose proof e as Hnth.
     assert (lenppars : ind_npars mdecl = #|pparams p|).
     { now rewrite (wf_predicate_length_pars wf_pred). }
-    destruct (declared_inductive_inj d decli); subst mdecl0 idecl0.
+    destruct (declared_inductive_inj d.p1 decli); subst mdecl0 idecl0.
     eapply erases_mkApps_inv in Hv' as [(? & ? & ? & ? & [] & ? & ? & ?) | (? & ? & ? & ? & ?)]; eauto.
     * subst.
       eapply Is_type_app in X1; auto. destruct X1.
@@ -440,7 +440,7 @@ Proof.
     rename e0 into hnth. rename e into eargs.
     eapply inversion_Proj in Hty' as (? & ? & ? & [] & ? & ? & ? & ? & ? & ?); [|easy].
     assert (Hpars : p.(proj_npars) = ind_npars x0).
-    { destruct (declared_constructor_inj d0 d). now subst. }
+    { destruct (declared_constructor_inj d0.p1 d.p1). now subst. }
     invs He.
 
     + depelim Hed.
@@ -449,7 +449,7 @@ Proof.
       eapply erases_mkApps_inv in Hvc'; eauto.
       destruct Hvc' as [ (? & ? & ? & ? & [] & ? & ? & ?) | (? & ? & ? & ? & ?)]; subst.
       * exists EAst.tBox.
-        destruct (declared_inductive_inj decli d) as [<- <-].
+        destruct (declared_inductive_inj decli.p1 d.p1) as [<- <-].
         assert (isprop : inductive_isprop_and_pars Σ' p.(proj_ind) = Some (true, ind_npars mdecl)).
         { eapply isPropositional_propositional. exact d. all:eauto. apply decli'.
           eapply isErasable_Propositional; eauto. }
@@ -1174,9 +1174,10 @@ Proof.
   rewrite H2.
   pose proof (onProjections p) as X.
   rewrite H1 in X.
-  destruct (ind_ctors hd) as [|ctor []] eqn:hctors => //.
+  destruct (ind_ctors hd) as [|ctor []] eqn:hctors ; edestruct X => //.
+  clear X. 
   depelim H. rewrite H1.
-  depelim H0. cbn. destruct X.
+  depelim H0. cbn.
   destruct H. rewrite -H.
   rewrite H3 in on_projs_all. cbn in on_projs_all.
   eapply Forall2_length in Hprojs. rewrite Hprojs in on_projs_all.

diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
@@ -794,10 +794,11 @@ Proof.
     rewrite -(abstract_env_lookup_correct _ _ H0).
     rewrite H2 H3. pose proof (abstract_env_ext_wf _ H) as [?].
     eapply extends_lookup_env in H3; try apply e; eauto. clear -H2 H3. congruence.
-    destruct X0.
-    rewrite -(abstract_env_ext_retroknowledge_correct _ H).
-    rewrite -(abstract_env_ext_retroknowledge_correct _ H0).
-    congruence. }
+    destruct X0. intros tag.
+    rewrite (abstract_primitive_constant_correct _ _ _ H).
+    rewrite (abstract_primitive_constant_correct _ _ _ H0).
+    unfold primitive_constant.
+    rewrite e0. congruence. }
   simp is_erasableb.
   set (obl := is_erasableb_obligation_2 _ _ _ _). clearbody obl.
   set(ty := (type_of_typing X_type' _ _ _ wt')) in *.
@@ -1117,7 +1118,7 @@ Proof.
     pose proof (declared_constant_inj _ _ d declc'). subst x.
     now econstructor; eauto.
     destruct H as [mib [mib' [declm declm']]].
-    red in declm, d. rewrite d in declm. noconf declm.
+    red in declm, d. unfold declared_minductive_gen in declm. rewrite d in declm. noconf declm.
   - apply inversion_Construct in wt as (? & ? & ? & ? & ? & ?); eauto.
     red in Σer. destruct kn.
     setoid_rewrite KernameSetFact.singleton_iff in Σer.
@@ -1137,11 +1138,11 @@ Proof.
     specialize (H1 kn). forward H1.
     now rewrite KernameSet.singleton_spec. red in H1. destruct H1.
     elimtype False. destruct H1 as [cst [declc _]].
-    { red in declc. destruct x1 as [d _]. red in d. rewrite d in declc. noconf declc. }
+    { red in declc. destruct x1 as [d _]. red in d. unfold declared_constant_gen in declc. rewrite d in declc. noconf declc. }
     destruct H1 as [mib [mib' [declm [declm' em]]]].
     pose proof em as em'. destruct em'.
     destruct x1 as [x1 hnth].
-    red in x1, declm. rewrite x1 in declm. noconf declm.
+    red in x1, declm. unfold declared_minductive_gen in declm. rewrite x1 in declm. noconf declm.
     eapply Forall2_nth_error_left in H1; eauto. destruct H1 as [? [? ?]].
     eapply erases_deps_tCase; eauto.
     split; eauto. split; eauto.
@@ -1161,11 +1162,12 @@ Proof.
     specialize (H0 (inductive_mind p.(proj_ind))). forward H0.
     now rewrite KernameSet.singleton_spec. red in H0. destruct H0.
     elimtype False. destruct H0 as [cst [declc _]].
-    { red in declc. destruct d as [[[d _] _] _]. red in d. rewrite d in declc. noconf declc. }
+    { red in declc. destruct d as [[[d _] _] _]. red in d. 
+      unfold declared_constant_gen in declc.  rewrite d in declc. noconf declc. }
     destruct H0 as [mib [mib' [declm [declm' em]]]].
     assert (mib = x0).
     { destruct d as [[[]]].
-      red in H0, declm. rewrite H0 in declm. now noconf declm. }
+      red in H0, declm. unfold declared_minductive_gen in declm. rewrite H0 in declm. now noconf declm. }
     subst x0.
     pose proof em as em'. destruct em'.
     eapply Forall2_nth_error_left in H0 as (x' & ? & ?); eauto.
@@ -1220,7 +1222,7 @@ Proof.
     { inv wfΣ. inv X. intros <-.
       eapply lookup_env_Some_fresh in H. destruct X1. contradiction. }
     eapply erases_deps_tConst with cb cb'; eauto.
-    red. rewrite /lookup_env lookup_env_cons_fresh //.
+    red. rewrite /declared_constant_gen /lookup_env lookup_env_cons_fresh //.
     red.
     red in H1.
     destruct (cst_body cb) eqn:cbe;
@@ -1286,7 +1288,7 @@ Proof.
   intros wf [[cst [declc [cst' [declc' [ebody IH]]]]]|].
   red. inv wf. inv X. left.
   exists cst. split.
-  red in declc |- *. unfold lookup_env in *.
+  red in declc |- *. unfold declared_constant_gen, lookup_env in *.
   rewrite lookup_env_cons_fresh //.
   { eapply lookup_env_Some_fresh in declc. destruct X1.
     intros <-; contradiction. }
@@ -1309,7 +1311,7 @@ Proof.
 
   right. destruct H as [mib [mib' [? [? ?]]]].
   exists mib, mib'. intuition eauto.
-  * red. red in H. pose proof (lookup_env_ext wf H).
+  * red. red in H. pose proof (lookup_env_ext wf H). unfold declared_minductive_gen.
     now rewrite lookup_env_cons_disc.
   * red. pose proof (lookup_env_ext wf H).
     now rewrite elookup_env_cons_disc.
@@ -1324,7 +1326,7 @@ Proof.
   red. inv wf. inv X. left.
   exists cst. split.
   red in declc |- *.
-  unfold lookup_env in *.
+  unfold declared_constant_gen, lookup_env in *. 
   rewrite lookup_env_cons_fresh //.
   { eapply lookup_env_Some_fresh in declc.
     intros <-. destruct X1. contradiction. }
@@ -1345,7 +1347,7 @@ Proof.
 
   right. destruct H as [mib [mib' [Hm [? ?]]]].
   exists mib, mib'; intuition auto.
-  red. unfold lookup_env in *.
+  red. unfold declared_minductive_gen, lookup_env in *.
   rewrite lookup_env_cons_fresh //.
   now epose proof (lookup_env_ext wf Hm).
 Qed.
@@ -1431,7 +1433,8 @@ Proof.
         epose proof (abstract_env_exists Xpop) as [[Σpop wfpop]].
         epose proof (abstract_env_ext_exists Xmake) as [[Σmake wfmake]].
         exists c. split; auto. red.
-        unfold lookup_env; simpl; rewrite (prf _ wfΣ). cbn. rewrite eq_kername_refl //.
+        unfold declared_constant_gen, lookup_env; simpl; rewrite (prf _ wfΣ). cbn. 
+        rewrite eq_kername_refl //.
         pose proof (sub _ hin) as indeps.
         eapply KernameSet.mem_spec in indeps.
         unfold EGlobalEnv.declared_constant.
@@ -1477,15 +1480,15 @@ Proof.
           intros x hin'. eapply KernameSet.union_spec. right; auto.
           now rewrite -Heqdeps. } }
         { eexists m, _; intuition eauto.
-          simpl. rewrite /declared_minductive /lookup_env prf; eauto.
+          simpl. rewrite /declared_minductive /declared_minductive_gen /lookup_env prf; eauto.
           simpl. rewrite eq_kername_refl. reflexivity.
           specialize (sub _ hin).
           eapply KernameSet.mem_spec in sub.
           simpl. rewrite sub.
           red. cbn. rewrite eq_kername_refl.
           reflexivity.
           assert (declared_minductive Σ kn m).
-          { red. unfold lookup_env. rewrite prf; eauto. cbn. now rewrite eqb_refl. }
+          { red. unfold declared_minductive_gen, lookup_env. rewrite prf; eauto. cbn. now rewrite eqb_refl. }
           eapply on_declared_minductive in H0; tea.
           now eapply erases_mutual. }
 
@@ -2371,14 +2374,14 @@ Proof.
     + econstructor. econstructor; eauto. eauto.
   - intros. eapply erases_mkApps_inv in Herase as [(? & ? & ? & -> & [Herasable] & ? & ? & ->)|(? & ? & -> & ? & ?)]. all:eauto.
     + exfalso. eapply isErasable_Propositional in Herasable; eauto.
-      red in H1, Herasable. unfold PCUICAst.lookup_inductive, PCUICAst.lookup_minductive, isPropositionalArity in *.
+      red in H1, Herasable. unfold PCUICAst.lookup_inductive, lookup_inductive_gen, PCUICAst.lookup_minductive, lookup_minductive_gen, isPropositionalArity in *.
       edestruct PCUICEnvironment.lookup_env as [ [] | ], nth_error, destArity as [[] | ]; auto; try congruence.
     + inv H2.
       * cbn. unfold erase_clause_1. destruct (inspect_bool (is_erasableb X_type Xext [] (tConstruct i n ui) Hyp0)).
         -- exfalso. sq. destruct (@is_erasableP _ _ [] (tConstruct i n ui) Hyp0) => //.
            specialize_Σ Hrel. sq.
            eapply (isErasable_Propositional (args := [])) in s; eauto.
-           red in H1, s. unfold PCUICAst.lookup_inductive, PCUICAst.lookup_minductive, isPropositionalArity in *.
+           red in H1, s. unfold PCUICAst.lookup_inductive, lookup_inductive_gen, PCUICAst.lookup_minductive, lookup_minductive_gen, isPropositionalArity in *.
            edestruct PCUICEnvironment.lookup_env as [ [] | ], nth_error, destArity as [[] | ]; auto; congruence.
         -- f_equal. eapply Forall2_eq. clear X0 H wt. induction H3.
            ++ cbn. econstructor.
@@ -2387,15 +2390,15 @@ Proof.
                ** inv H0. eapply IHForall2. eauto.
       * exfalso. eapply (isErasable_Propositional (args := [])) in X1; eauto.
         red in H1, X1.
-        unfold PCUICAst.lookup_inductive, PCUICAst.lookup_minductive, isPropositionalArity in *.
+        unfold PCUICAst.lookup_inductive, lookup_inductive_gen, PCUICAst.lookup_minductive, lookup_minductive_gen, isPropositionalArity in *.
         edestruct PCUICEnvironment.lookup_env as [ [] | ], nth_error, destArity as [[] | ]; auto; congruence.
   - eauto.
   - intros ? ? H3. assert (Hext_ : ∥ wf_ext Σ0∥) by now eapply heΣ.
     sq.
     specialize_Σ H2.
     eapply (isErasable_Propositional) in H3; eauto.
     pose proof (abstract_env_ext_irr _ H2 Hrel). subst.
-    red in H1, H3. unfold PCUICAst.lookup_inductive, PCUICAst.lookup_minductive, isPropositionalArity in *.
+    red in H1, H3. unfold PCUICAst.lookup_inductive, lookup_inductive_gen, PCUICAst.lookup_minductive, lookup_minductive_gen, isPropositionalArity in *.
     edestruct PCUICEnvironment.lookup_env as [ [] | ], nth_error, destArity as [[] | ]; auto; congruence.
   - intros.  assert (Hext__ : ∥ wf_ext Σ0∥) by now eapply heΣ.
     specialize_Σ H2. eapply welltyped_mkApps_inv in wt; eauto. eapply wt.
@@ -2463,8 +2466,8 @@ Definition decls_prefix decls (Σ' : global_env) :=
   ∑ Σ'', declarations Σ' = Σ'' ++ decls.
 
 Lemma on_global_decls_prefix {cf} Pcmp P univs retro decls decls' :
-  on_global_decls Pcmp P univs retro (decls ++ decls') ->
-  on_global_decls Pcmp P univs retro decls'.
+  PCUICAst.on_global_decls Pcmp P univs retro (decls ++ decls') ->
+  PCUICAst.on_global_decls Pcmp P univs retro decls'.
 Proof.
   induction decls => //.
   intros ha; depelim ha.