Avoid Ee := EWcbvEval module aliases which result in ugly extraction …

…issues (#1057)
MetaCoq · Feb 17, 2024 · 07c0a82 · 07c0a82
1 parent 6a26f38
commit 07c0a82
Show file tree

Hide file tree

Showing 9 changed files with 83 additions and 87 deletions.
diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v
@@ -1872,7 +1872,7 @@ Section PCUICErase.
     have prev : Transform.pre verified_lambdabox_pipeline (Σ', v'').
     { clear -wfl pre' H1. cbn in H1.
       destruct pre' as [[] []]. split; split => //=.
-      eapply Prelim.Ee.eval_wellformed; eauto.
+      eapply EWcbvEval.eval_wellformed; eauto.
       eapply EEtaExpandedFix.isEtaExp_expanded.
       eapply (@EEtaExpandedFix.eval_etaexp wfl); eauto.
       now eapply EEtaExpandedFix.expanded_global_env_isEtaExp_env.
@@ -1927,7 +1927,7 @@ Section PCUICErase.
     have prev : Transform.pre verified_lambdabox_pipeline (Σ', v'').
     { clear -wfl pre' H1. cbn in H1.
       destruct pre' as [[] []]. split; split => //=.
-      eapply Prelim.Ee.eval_wellformed; eauto.
+      eapply EWcbvEval.eval_wellformed; eauto.
       eapply EEtaExpandedFix.isEtaExp_expanded.
       eapply (@EEtaExpandedFix.eval_etaexp wfl); eauto.
       now eapply EEtaExpandedFix.expanded_global_env_isEtaExp_env.
@@ -2275,8 +2275,8 @@ Section pipeline_theorem.
 
   Variable Normalisation :  (forall Σ, wf_ext Σ -> PCUICSN.NormalizationIn Σ).
 
-  Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)  
-    {has_rel : has_tRel} {has_box : has_tBox} 
+  Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)
+    {has_rel : has_tRel} {has_box : has_tBox}
     T (typing: ∥PCUICTyping.typing Σ [] t T∥):
   let Σ_t := (transform verified_erasure_pipeline (Σ, t) (precond _ _ _ _ expΣ expt typing _)).1 in
     EGlobalEnv.lookup_env Σ_t kn = Some decl ->
@@ -2356,7 +2356,7 @@ Section pipeline_theorem.
   Let v_t := compile_value_box (PCUICExpandLets.trans_global_env Σ) v [].
 
 
-  Lemma verified_erasure_pipeline_extends (efl := EInlineProjections.switch_no_params all_env_flags) 
+  Lemma verified_erasure_pipeline_extends (efl := EInlineProjections.switch_no_params all_env_flags)
     {has_rel : has_tRel} {has_box : has_tBox} :
    EGlobalEnv.extends Σ_v Σ_t.
   Proof.

diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v
@@ -623,7 +623,7 @@ Lemma value_trans {efl : EEnvFlags} {fl : WcbvFlags} {hasc : cstr_as_blocks = tr
   value (trans_env Σ) (trans Σ c).
 Proof.
   intros hasapp wfg wf h.
-  revert c h wf. apply: Ee.value_values_ind.
+  revert c h wf. apply: EWcbvEval.value_values_ind.
   - intros t; destruct t => //; cbn -[lookup_constructor GlobalContextMap.lookup_inductive_kind].
     all:try solve [intros; repeat constructor => //].
     destruct args => //.
@@ -673,9 +673,9 @@ Lemma trans_correct {efl : EEnvFlags} {fl} {wcon : with_constructor_as_block = t
   has_tApp ->
   wf_glob Σ ->
   closed_env Σ ->
-  @Ee.eval fl Σ t v ->
+  @EWcbvEval.eval fl Σ t v ->
   wellformed Σ 0 t ->
-  @Ee.eval fl (trans_env Σ) (trans Σ t) (trans Σ v).
+  @EWcbvEval.eval fl (trans_env Σ) (trans Σ t) (trans Σ v).
 Proof.
   intros hasapp wfΣ clΣ ev wf.
   revert t v wf ev.
@@ -715,7 +715,7 @@ Proof.
     + eapply eval_beta. eapply e0; eauto.
       constructor; eauto.
       rewrite closed_subst // simpl_subst_k //.
-      eapply Ee.eval_to_value in H.
+      eapply EWcbvEval.eval_to_value in H.
       eapply value_constructor_as_block in H.
       eapply constructor_isprop_pars_decl_constructor in H1 as [mdecl [idecl [hl' hp]]].
       econstructor; eauto.
@@ -763,7 +763,7 @@ Qed.
     eapply eval_closed in ev1 => //.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
-    eapply Ee.eval_fix; eauto.
+    eapply EWcbvEval.eval_fix; eauto.
     rewrite map_length.
     eapply trans_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
@@ -778,15 +778,15 @@ Qed.
     move: ev1 => /andP [] clfix clargs.
     eapply eval_closed in ev2; tas.
     rewrite trans_mkApps in IHev1 |- *.
-    simpl in *. eapply Ee.eval_fix_value. auto. auto. auto.
+    simpl in *. eapply EWcbvEval.eval_fix_value. auto. auto. auto.
     eapply trans_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     now rewrite map_length.
 
   - move/andP => [] clf cla.
     eapply eval_closed in ev1 => //.
     eapply eval_closed in ev2; tas.
-    simpl in *. eapply Ee.eval_fix'. auto. auto.
+    simpl in *. eapply EWcbvEval.eval_fix'. auto. auto.
     eapply trans_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     eapply IHev2; tea. eapply IHev3.
@@ -805,15 +805,15 @@ Qed.
     rewrite GlobalContextMap.lookup_inductive_kind_spec in IHev2 |- *.
     destruct EGlobalEnv.lookup_inductive_kind as [[]|] eqn:isp => //.
     simpl in IHev1.
-    eapply Ee.eval_cofix_case. tea.
+    eapply EWcbvEval.eval_cofix_case. tea.
     apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     apply IHev2.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     simpl in *.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply trans_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
 
   - intros cd. specialize (IHev1 cd).
@@ -845,7 +845,7 @@ Qed.
     rewrite (constructor_isprop_pars_decl_inductive e1).
     rewrite trans_mkApps in IHev1.
     specialize (IHev1 cld).
-    eapply Ee.eval_proj; tea.
+    eapply EWcbvEval.eval_proj; tea.
     now rewrite -is_propositional_cstr_trans.
     now len. rewrite nth_error_map e3 //.
     eapply IHev2.
@@ -868,8 +868,8 @@ Qed.
 
   - move/andP => [] clf cla.
     specialize (IHev1 clf). specialize (IHev2 cla).
-    eapply Ee.eval_app_cong; eauto.
-    eapply Ee.eval_to_value in ev1.
+    eapply EWcbvEval.eval_app_cong; eauto.
+    eapply EWcbvEval.eval_to_value in ev1.
     destruct ev1; simpl in *; eauto.
     * destruct t => //; rewrite trans_mkApps /=.
     * destruct with_guarded_fix.

diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
@@ -544,9 +544,9 @@ Qed.
 Lemma remove_match_on_box_correct {efl : EEnvFlags} {fl}{wcon : with_constructor_as_block = false} {Σ : GlobalContextMap.t} t v :
   wf_glob Σ ->
   closed_env Σ ->
-  @Ee.eval fl Σ t v ->
+  @EWcbvEval.eval fl Σ t v ->
   closed t ->
-  @Ee.eval (disable_prop_cases fl) (remove_match_on_box_env Σ) (remove_match_on_box Σ t) (remove_match_on_box Σ v).
+  @EWcbvEval.eval (disable_prop_cases fl) (remove_match_on_box_env Σ) (remove_match_on_box Σ t) (remove_match_on_box Σ v).
 Proof.
   intros wfΣ clΣ ev.
   induction ev; simpl in *.
@@ -599,7 +599,7 @@ Proof.
     eapply eval_closed in ev1 => //.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
-    eapply Ee.eval_fix; eauto.
+    eapply EWcbvEval.eval_fix; eauto.
     rewrite map_length.
     eapply remove_match_on_box_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
@@ -614,15 +614,15 @@ Proof.
     move: ev1 => /andP [] clfix clargs.
     eapply eval_closed in ev2; tas.
     rewrite remove_match_on_box_mkApps in IHev1 |- *.
-    simpl in *. eapply Ee.eval_fix_value. auto. auto. auto.
+    simpl in *. eapply EWcbvEval.eval_fix_value. auto. auto. auto.
     eapply remove_match_on_box_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     now rewrite map_length.
 
   - move/andP => [] clf cla.
     eapply eval_closed in ev1 => //.
     eapply eval_closed in ev2; tas.
-    simpl in *. eapply Ee.eval_fix'. auto. auto.
+    simpl in *. eapply EWcbvEval.eval_fix'. auto. auto.
     eapply remove_match_on_box_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     eapply IHev2; tea. eapply IHev3.
@@ -642,15 +642,15 @@ Proof.
     destruct EGlobalEnv.inductive_isprop_and_pars as [[[] pars]|] eqn:isp => //.
     destruct brs as [|[a b] []]; simpl in *; auto.
     simpl in IHev1.
-    eapply Ee.eval_cofix_case. tea.
+    eapply EWcbvEval.eval_cofix_case. tea.
     apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     apply IHev2.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     simpl in *.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
-    eapply Ee.eval_cofix_case; tea.
+    eapply EWcbvEval.eval_cofix_case; tea.
     apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
 
   - intros cd. specialize (IHev1 cd).
@@ -682,7 +682,7 @@ Proof.
     rewrite (constructor_isprop_pars_decl_inductive e1).
     rewrite remove_match_on_box_mkApps in IHev1.
     specialize (IHev1 cld).
-    eapply Ee.eval_proj; tea.
+    eapply EWcbvEval.eval_proj; tea.
     now rewrite -is_propositional_cstr_remove_match_on_box.
     now len. rewrite nth_error_map e3 //.
     eapply IHev2.
@@ -705,8 +705,8 @@ Proof.
 
   - move/andP => [] clf cla.
     specialize (IHev1 clf). specialize (IHev2 cla).
-    eapply Ee.eval_app_cong; eauto.
-    eapply Ee.eval_to_value in ev1.
+    eapply EWcbvEval.eval_app_cong; eauto.
+    eapply EWcbvEval.eval_to_value in ev1.
     destruct ev1; simpl in *; eauto.
     * depelim a0. destruct t => //; rewrite ?remove_match_on_box_mkApps /=.
       cbn in i. now rewrite !orb_false_r orb_true_r in i.

diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
@@ -265,8 +265,8 @@ Proof.
         now eapply isErasable_Proof. }
       2:{
       exists x2. split; eauto. constructor. eapply eval_iota_sing => //.
-      pose proof (Ee.eval_to_value _ _ He_v').
-      let X0 := match goal with H : Ee.value _ (EAst.mkApps _ _) |- _ => H end in
+      pose proof (EWcbvEval.eval_to_value _ _ He_v').
+      let X0 := match goal with H : EWcbvEval.value _ (EAst.mkApps _ _) |- _ => H end in
       eapply value_app_inv in X0. subst. eassumption.
       depelim H2.
       eapply isErasable_Propositional in X0; eauto.
@@ -446,7 +446,7 @@ Proof.
          constructor.
          destruct x1 as [n br'].
          eapply eval_iota_sing => //.
-         pose proof (Ee.eval_to_value _ _ He_v') as X0.
+         pose proof (EWcbvEval.eval_to_value _ _ He_v') as X0.
          apply value_app_inv in X0; subst x0.
          apply He_v'.
          now rewrite -eq_npars.
@@ -517,7 +517,7 @@ Proof.
         eapply isErasable_Proof. constructor. eauto.
 
         eapply eval_proj_prop => //.
-        pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
+        pose proof (EWcbvEval.eval_to_value _ _ Hty_vc') as X0.
         eapply value_app_inv in X0. subst. eassumption.
         now rewrite -eqpars.
       * rename H3 into Hinf.
@@ -534,7 +534,7 @@ Proof.
         destruct (declared_projection_inj d d0) as [? [? []]]; subst mdecl0 idecl0 pdecl0 cdecl.
         invs H2.
         -- exists x9. split; eauto. constructor.
-            eapply Ee.eval_proj; eauto. rewrite -eqpars.
+            eapply EWcbvEval.eval_proj; eauto. rewrite -eqpars.
             erewrite isPropositional_propositional_cstr; eauto.
             move/negbTE: H9 => ->. reflexivity.
             eapply declared_constructor_from_gen. apply d0. cbn. eapply decli'. cbn. rewrite -lenx5 //.
@@ -558,7 +558,7 @@ Proof.
           eassumption.
           eapply isErasable_Proof.
           constructor. eapply eval_proj_prop => //.
-          pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
+          pose proof (EWcbvEval.eval_to_value _ _ Hty_vc') as X0.
           eapply value_app_inv in X0. subst. eassumption.
           now rewrite -eqpars.
         -- eapply erases_deps_eval in Hty_vc'; [|now eauto].
@@ -675,11 +675,11 @@ Proof.
              - now eapply erases_deps_eval in ev_arg; eauto. }
 
            exists x3. split. eauto.
-           constructor. eapply Ee.eval_fix.
+           constructor. eapply EWcbvEval.eval_fix.
            ++ eauto.
            ++ eauto.
            ++ eauto.
-           ++ rewrite <- Ee.closed_unfold_fix_cunfold_eq.
+           ++ rewrite <- EWcbvEval.closed_unfold_fix_cunfold_eq.
               { unfold EGlobalEnv.unfold_fix. rewrite e.
                 eapply All2_nth_error in Hmfix' as []; tea. cbn in *.
                 rewrite -eargsv -(Forall2_length H4); trea. }
@@ -727,7 +727,7 @@ Proof.
               eapply eval_fix; eauto.
               1-2:eapply value_final, eval_to_value; eauto.
               rewrite /cunfold_fix e0 //. congruence.
-           ++ constructor. eapply Ee.eval_box; [|now eauto].
+           ++ constructor. eapply EWcbvEval.eval_box; [|now eauto].
               apply eval_to_mkApps_tBox_inv in ev_stuck as ?; subst.
               eauto.
         -- eauto.
@@ -744,7 +744,7 @@ Proof.
 
     eapply erases_App in He as [(-> & [])|(? & ? & -> & ? & ?)].
     + exists E.tBox.
-      split; [|now constructor; eauto using @Ee.eval].
+      split; [|now constructor; eauto using @EWcbvEval.eval].
       constructor.
       eapply Is_type_red.
       * eauto.
@@ -765,7 +765,7 @@ Proof.
         rewrite -> !app_nil_r in *.
         cbn in *.
         exists E.tBox.
-        split; [|now constructor; eauto using @Ee.eval].
+        split; [|now constructor; eauto using @EWcbvEval.eval].
         eapply (Is_type_app _ _ _ [av]) in X as [].
         -- constructor.
            apply X.
@@ -779,7 +779,7 @@ Proof.
            unfold cunfold_fix in *.
            destruct (nth_error _ _) eqn:nth; [|congruence].
            eapply All2_nth_error_Some in X as (?&?&[? ? ? ? ?]); [|eauto].
-           constructor. eapply Ee.eval_fix_value.
+           constructor. eapply EWcbvEval.eval_fix_value.
            ++ eauto.
            ++ eauto.
            ++ eauto.
@@ -788,7 +788,7 @@ Proof.
 
         -- exists E.tBox.
            apply eval_to_mkApps_tBox_inv in H3 as ?; subst.
-           split; [|now constructor; eauto using @Ee.eval].
+           split; [|now constructor; eauto using @EWcbvEval.eval].
            eapply Is_type_app in X as [].
            ++ constructor.
               rewrite <- mkApps_snoc.
@@ -897,13 +897,13 @@ Proof.
             - now apply Forall_All, Forall_erases_deps_cofix_subst; eauto.
             - now eapply nth_error_forall in H2; eauto. }
           exists v'. split => //. split.
-          eapply Ee.eval_cofix_case; tea.
+          eapply EWcbvEval.eval_cofix_case; tea.
           rewrite /EGlobalEnv.cunfold_cofix nth' //. f_equal.
           f_equal.
-          rewrite -(Ee.closed_cofix_substl_subst_eq (idx:=idx)) //. }
+          rewrite -(EWcbvEval.closed_cofix_substl_subst_eq (idx:=idx)) //. }
         { eapply eval_to_mkApps_tBox_inv in H1 as H'; subst L'; cbn in *. depelim hl'.
           edestruct IHeval1 as (? & ? & [?]); tea.
-          pose proof (Ee.eval_deterministic H1 H3). subst x0.
+          pose proof (EWcbvEval.eval_deterministic H1 H3). subst x0.
           eapply erases_deps_eval in Hed; tea.
           specialize (IHeval2 (E.tCase (ip, ci_npar ip) E.tBox brs')).
           forward IHeval2.
@@ -1017,13 +1017,13 @@ Proof.
             - now apply Forall_All, Forall_erases_deps_cofix_subst; eauto.
             - now eapply nth_error_forall in H1; eauto. }
           exists v'. split => //. split.
-          eapply Ee.eval_cofix_proj; tea.
+          eapply EWcbvEval.eval_cofix_proj; tea.
           rewrite /EGlobalEnv.cunfold_cofix nth' //. f_equal.
           f_equal.
-          rewrite -(Ee.closed_cofix_substl_subst_eq (idx:=idx)) //. }
+          rewrite -(EWcbvEval.closed_cofix_substl_subst_eq (idx:=idx)) //. }
         { eapply eval_to_mkApps_tBox_inv in H2 as H'; subst L'; cbn in *. depelim hl'.
           edestruct IHeval1 as (? & ? & [?]); tea.
-          pose proof (Ee.eval_deterministic H3 H2). subst x0.
+          pose proof (EWcbvEval.eval_deterministic H3 H2). subst x0.
           eapply erases_deps_eval in Hed; tea.
           specialize (IHeval2 (E.tProj p E.tBox)).
           forward IHeval2.
@@ -1083,7 +1083,7 @@ Proof.
         eapply erases_deps_eval in Hed1; tea.
         eapply erases_deps_mkApps_inv in Hed1 as [].
         depelim H8.
-        constructor. eapply Ee.eval_construct; tea. eauto.
+        constructor. eapply EWcbvEval.eval_construct; tea. eauto.
         eapply (EGlobalEnv.declared_constructor_lookup H9).
         rewrite -(Forall2_length H7).
         rewrite /EAst.cstr_arity.
@@ -1129,7 +1129,7 @@ Proof.
         eapply wcbveval_red; eauto.
       * exists (E.tApp x2 x3).
         split; [econstructor; eauto|].
-        constructor; eapply Ee.eval_app_cong; eauto.
+        constructor; eapply EWcbvEval.eval_app_cong; eauto.
         eapply ssrbool.negbT.
         repeat eapply orb_false_intro.
         -- destruct x2; try reflexivity.