better spec for abstract_env_lookup_correct

erasure/theories/ErasureFunction.v

@@ -793,8 +793,8 @@ Proof.
   assert (hl : Hlookup X_type X X_type' X').
   { red. intros. specialize (ext _ _ H H0) as [[?] ?].
     split. intros.
-    rewrite -(abstract_env_lookup_correct _ _ H).
-    rewrite -(abstract_env_lookup_correct _ _ H0).
+    rewrite -(abstract_env_lookup_correct' _ _ H).
+    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. intros tag.

safechecker/theories/PCUICSafeConversion.v

@@ -1537,8 +1537,8 @@ Qed.
   exfalso;
   Tactics.program_simplify;
   CoreTactics.equations_simpl;
-  try erewrite <- abstract_env_lookup_correct in eq1; eauto ;
-  try erewrite <- abstract_env_lookup_correct in eq2; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq1; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq2; eauto ;
   try clear aux; specialize_Σ wfΣ;
   try solve
       [match goal with
@@ -1554,8 +1554,8 @@ Qed.
   exfalso;
   Tactics.program_simplify;
   CoreTactics.equations_simpl;
-  try erewrite <- abstract_env_lookup_correct in eq1; eauto ;
-  try erewrite <- abstract_env_lookup_correct in eq2; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq1; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq2; eauto ;
   try clear aux; specialize_Σ wfΣ;
   solve
       [match goal with
@@ -1573,13 +1573,13 @@ Qed.
     sq.
     eapply red_welltyped; try eapply h2; eauto.
     eapply red_zipc.
-    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     unshelve eapply R_cored2.
     all: try reflexivity.
     simpl. intros. eapply cored_zipc.
-    eapply cored_const. erewrite abstract_env_lookup_correct; eassumption.
+    eapply cored_const. erewrite abstract_env_lookup_correct'; eassumption.
   Qed.
   Next Obligation.
     rename H into wfΣ; destruct (hΣ _ wfΣ).
@@ -1591,7 +1591,7 @@ Qed.
       eapply welltyped_is_open_term in h2.
       sq. now rewrite (All2_fold_length hx).
     * eapply into_closed_red; fvs.
-      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       + red in h. sq. fvs.
    Unshelve. eauto.
   Qed.
@@ -1606,19 +1606,19 @@ Qed.
     * clear aux; eapply welltyped_zipc_zipp in h2; eauto.
       eapply welltyped_is_open_term in h2. sq. now rewrite (All2_fold_length hx).
     * eapply into_closed_red; fvs.
-      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       + sq. fvs.
   Unshelve. eauto.
   Qed.
   Next Obligation.
     pose proof (hΣ _ wfΣ). sq.
     eapply red_welltyped ; [eauto|exact (h1 _ wfΣ)|..].
     eapply red_zipc.
-    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     eapply R_cored. simpl. intros. eapply cored_zipc.
-    eapply cored_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply cored_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     rename H into wfΣ. destruct (heΣ _ wfΣ) as [wΣ].
@@ -1627,7 +1627,7 @@ Qed.
     eapply closed_red_zipp.
     { eapply welltyped_zipc_zipp in h1; auto; fvs. }
     eapply into_closed_red; fvs.
-    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     + specialize (hx _ wfΣ). clear -hx wΣ. sq.  fvs.
     Unshelve. all : eauto.
   Qed.
@@ -1640,7 +1640,7 @@ Qed.
     eapply closed_red_zipp.
     { eapply welltyped_zipc_zipp in h1; auto; fvs. }
     eapply into_closed_red; fvs.
-    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     + specialize (hx _ wfΣ). sq; fvs.
     Unshelve. eauto.
   Qed.
@@ -1652,7 +1652,7 @@ Qed.
       apply conv_cum_alt in H as [(?&?&[r1 r2 eq])]; auto.
     2: pose proof (hΣ _ wfΣ); sq ; eauto.
     rewrite zipp_as_mkApps in r1, r2.
-    erewrite <- abstract_env_lookup_correct in eq1, eq2; eauto.
+    erewrite <- abstract_env_lookup_correct' in eq1, eq2; eauto.
     symmetry in eq1, eq2.
     generalize hΣ. intros []; eauto.
     unshelve eapply closed_red_mkApps_tConst_axiom in r1 as (?&->&?); eauto.
@@ -2685,7 +2685,7 @@ Qed.
     - intros ? ? Hu Hu'; apply iff_reflect; apply (abstract_env_compare_universe_correct _ wfΣ Conv).
       + revert Hu. apply reflect_iff. apply wf_universe_reflect.
       + revert Hu'. apply reflect_iff. apply wf_universe_reflect.
-    - intros; now eapply abstract_env_lookup_correct.
+    - intros; now eapply abstract_env_lookup_correct'.
     - revert hl. apply reflect_iff, wf_universe_instanceP.
     - revert hl'. apply reflect_iff, wf_universe_instanceP.
   Qed.
@@ -3497,20 +3497,20 @@ Qed.
     eapply red_welltyped ; [auto|..].
     - exact h1.
     - eapply red_zipc.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     pose (heΣ _ wfΣ). clear aux. specialize_Σ wfΣ. sq.
     eapply red_welltyped ; [auto|..].
     - exact h2.
     - eapply red_zipc.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     eapply R_cored. simpl. intros.
     eapply cored_zipc.
     eapply cored_const.
-    erewrite abstract_env_lookup_correct; eauto.
+    erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     rename H into wfΣ. destruct (hΣ _ wfΣ).
@@ -3519,14 +3519,14 @@ Qed.
     - eapply red_conv_cum_l ; try assumption.
       eapply closed_red_zipp. 1:eapply welltyped_zipc_zipp in h1; fvs.
       eapply into_closed_red.
-      * eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      * eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       * eapply welltyped_zipc_zipp in h1; fvs.
       * eapply welltyped_zipc_zipp in h1; fvs.
     - etransitivity ; try eassumption.
       eapply red_conv_cum_r ; try assumption.
       eapply closed_red_zipp; auto.
       2:{ eapply into_closed_red; auto.
-        * eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+        * eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
         * eapply welltyped_zipc_zipp in h1; fvs. }
       clear aux. eapply welltyped_zipc_zipp in h2; eauto.
       destruct hx as [hx]. rewrite (All2_fold_length hx); fvs.
@@ -3538,9 +3538,9 @@ Qed.
     eapply conv_cum_red_inv.
     - eauto.
     - apply red_zipp.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     - apply red_zipp.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     - now eapply H.
   Qed.
   Next Obligation.
@@ -3550,24 +3550,24 @@ Qed.
     eapply conv_cum_mkApps_inv in H as [(?&?)]; eauto.
     - apply whnf_mkApps.
       eapply whne_const.
-      + erewrite abstract_env_lookup_correct; eauto.
+      + erewrite abstract_env_lookup_correct'; eauto.
       + eauto.
     - apply whnf_mkApps.
       eapply whne_const.
-      + erewrite abstract_env_lookup_correct; eauto.
+      + erewrite abstract_env_lookup_correct'; eauto.
       + eauto.
   Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
     eapply welltyped_zipc_tConst_inv in h1 as (?&?&?); eauto.
     unfold declared_constant, declared_constant_gen in *.
-    erewrite abstract_env_lookup_correct in d; eauto. congruence.
+    erewrite abstract_env_lookup_correct' in d; eauto. congruence.
   Qed.
   Next Obligation.
   destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
   eapply welltyped_zipc_tConst_inv in h1 as (?&?&?); eauto.
   unfold declared_constant, declared_constant_gen in *.
-  erewrite abstract_env_lookup_correct in d; eauto. congruence.
+  erewrite abstract_env_lookup_correct' in d; eauto. congruence.
 Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
@@ -5089,7 +5089,7 @@ Qed.
       + reflexivity.
       + eapply red_delta.
       * unfold declared_constant, declared_constant_gen.
-        erewrite abstract_env_lookup_correct; eauto.
+        erewrite abstract_env_lookup_correct'; eauto.
         * reflexivity.
     - eapply unfold_one_case_cored in eq as r; eauto.
       apply cored_red in r.
@@ -5122,7 +5122,7 @@ Qed.
       + reflexivity.
       + eapply red_delta.
         * unfold declared_constant, declared_constant_gen.
-          erewrite abstract_env_lookup_correct;  eauto.
+          erewrite abstract_env_lookup_correct';  eauto.
         * reflexivity.
     - eapply unfold_one_case_cored in eq as r; eauto. apply cored_red in r.
       destruct r as [r].
@@ -5153,7 +5153,7 @@ Qed.
     - repeat zip fold. eapply cored_context.
       constructor. eapply red_delta.
       + unfold declared_constant, declared_constant_gen.
-        erewrite abstract_env_lookup_correct; eauto.
+        erewrite abstract_env_lookup_correct'; eauto.
       + reflexivity.
     - repeat zip fold. eapply cored_context.
       eapply unfold_one_case_cored; eauto.
@@ -5256,7 +5256,7 @@ Qed.
       constructor; eexists _, [].
       eauto using whnf_red with pcuic.
     - constructor; eexists _, (decompose_stack π).1.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       split; [econstructor|]; eauto.
       split; [eauto with pcuic|].
       apply whnf_mkApps.
@@ -5267,15 +5267,15 @@ Qed.
       destruct h as (?&typ); auto.
       apply inversion_Const in typ as (?&?&?&?); auto.
       unfold declared_constant in d.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       congruence.
     - zip fold in h.
       destruct (hΣ _ wfΣ).
       eapply welltyped_context in h; eauto.
       destruct h as (?&typ); auto.
       apply inversion_Const in typ as (?&?&?&?); auto.
       unfold declared_constant in d.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       congruence.
     - clear H.
       eapply unfold_one_case_None in e as [(c'&r&whcase)]; eauto.

safechecker/theories/PCUICSafeReduce.v

@@ -593,7 +593,7 @@ Corollary R_Acc_aux :
     left. econstructor. eapply red1_context.
     econstructor.
     - unfold declared_constant, declared_constant_gen.
-      rewrite (abstract_env_lookup_correct _ _ wfΣ). rewrite <- eq. reflexivity.
+      rewrite (abstract_env_lookup_correct' _ _ wfΣ). rewrite <- eq. reflexivity.
     - cbn. reflexivity.
   Qed.
 
@@ -605,7 +605,7 @@ Corollary R_Acc_aux :
     destruct h as [T h].
     apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
     unfold declared_constant, declared_constant_gen in d.
-    rewrite (abstract_env_lookup_correct _ _ wfΣ), <- eq in d.
+    rewrite (abstract_env_lookup_correct' _ _ wfΣ), <- eq in d.
     discriminate.
   Qed.
   Next Obligation.
@@ -616,7 +616,7 @@ Corollary R_Acc_aux :
     destruct h as [T h].
     apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
     unfold declared_constant, declared_constant_gen in d.
-    rewrite (abstract_env_lookup_correct _ _ wfΣ), <- eq in d.
+    rewrite (abstract_env_lookup_correct' _ _ wfΣ), <- eq in d.
     discriminate.
   Qed.
 
@@ -1567,7 +1567,7 @@ Corollary R_Acc_aux :
       assumption.
     - unfold zipp. case_eq (decompose_stack π). intros.
       constructor. constructor. eapply whne_mkApps. econstructor.
-      + symmetry. erewrite abstract_env_lookup_correct; eauto.
+      + symmetry. erewrite abstract_env_lookup_correct'; eauto.
       + reflexivity.
     - match goal with
       | |- context [ reduce ?x ?y ?z ] =>

safechecker/theories/PCUICSafeRetyping.v

@@ -260,7 +260,7 @@ Qed.
   Next Obligation.
     split.
     - symmetry in look.
-      etransitivity. erewrite (abstract_env_lookup_correct X); eauto.
+      etransitivity. erewrite (abstract_env_lookup_correct' X); eauto.
       reflexivity.
     - now symmetry.
   Defined.
@@ -271,10 +271,10 @@ Qed.
     cbn.
     apply_funelim (lookup_ind_decl ind).
     1-2: intros * _ her [mdecl [idecl [declm decli]]];
-      red in declm; erewrite <- abstract_env_lookup_correct, declm in e0; eauto;
+      red in declm; erewrite <- abstract_env_lookup_correct', declm in e0; eauto;
       congruence.
     1-2:intros * _ _ => // => _ [mdecl [idecl [declm /= decli]]].
-    red in declm. erewrite <- abstract_env_lookup_correct, declm in look; eauto.
+    red in declm. erewrite <- abstract_env_lookup_correct', declm in look; eauto.
     noconf look.
     congruence.
   Qed.
@@ -486,22 +486,22 @@ Qed.
     cbn in *; intros. pose (hΣ _ wfΣ). specialize_Σ wfΣ.
     inversion wt. sq.
     inversion X0; subst.
-    erewrite <- abstract_env_lookup_correct in e; eauto.
+    erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e. subst.
     now constructor.
   Defined.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     specialize_Σ wfΣ. inversion wt.
     inversion X0 ; subst.
-    clear wildcard. erewrite <- abstract_env_lookup_correct in e; eauto.
+    clear wildcard. erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e.
   Defined.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     specialize_Σ wfΣ. inversion wt.
     inversion X0 ; subst.
-    clear wildcard. erewrite <- abstract_env_lookup_correct in e; eauto.
+    clear wildcard. erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e.
   Defined.
   Next Obligation.