define and use on_global_decls_data everywhere

Author: tabareau

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.

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.

erasure/theories/ErasureFunction.v

@@ -772,7 +772,7 @@ Qed.
     case: eqb_spec.
     intros ->. 
     eapply lookup_global_Some_fresh in hl.
-    rewrite e in wf. destruct wf as [_ ond]; depelim ond.
+    rewrite e in wf. destruct wf as [_ ond]; depelim ond. destruct o as [f ? ? ? ].
     cbn in *. eapply Forall_app in f as []. contradiction.
     intros _.
     eapply IHx; trea.
@@ -908,7 +908,7 @@ Next Obligation.
   { now eexists. }
   destruct (abstract_pop_decls_correct X decls prop' _ _ HX H) as [? []].
   clear H. specialize (prop _ HX). destruct x, Σ, H0; cbn in *.
-  subst. sq. destruct wfX. depelim o0. split => //.
+  subst. sq. destruct wfX. depelim o0. destruct o1.  split => //.
 Qed.
 Next Obligation.
   pose proof (abstract_env_ext_wf _ H) as [wf]. 
@@ -922,7 +922,7 @@ Next Obligation.
   pose proof (abstract_make_wf_env_ext_correct _ _ _ _ _ HX' H). 
   clear H HX'. specialize (prop _ HX). destruct x, Σ as [[] u], H0; cbn in *.
   subst. sq. inversion H3. subst. clear H3. destruct wfX. cbn in *.
-  rewrite prop in o0. depelim o0. cbn in o2. apply o2.
+  rewrite prop in o0. depelim o0. destruct o1. exact on_global_decl_d.
 Qed.
 Next Obligation.
   pose proof (abstract_env_exists X) as [[? HX]]. 
@@ -1218,7 +1218,7 @@ Proof.
   induction er using erases_deps_forall_ind; try solve [now constructor].
   - assert (kn <> kn0).
     { inv wfΣ. inv X. intros <-.
-      eapply lookup_env_Some_fresh in H. contradiction. }
+      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.
@@ -1240,15 +1240,15 @@ Proof.
     red in H. red.
     inv wfΣ. inv X.
     rewrite -H. simpl. unfold lookup_env; simpl. destruct (eqb_spec (inductive_mind p.1) kn); try congruence.
-    eapply lookup_env_Some_fresh in H. subst kn; contradiction.
+    eapply lookup_env_Some_fresh in H. destruct X1. subst kn; contradiction.
   - econstructor; eauto.
     red. destruct H. split; eauto.
     destruct d0; split; eauto.
     destruct d0; split; eauto.
     inv wfΣ. inv X.
     red in H |- *.
     rewrite -H. simpl. unfold lookup_env; simpl; destruct (eqb_spec (inductive_mind p.(proj_ind)) kn); try congruence.
-    eapply lookup_env_Some_fresh in H. subst kn. contradiction.
+    eapply lookup_env_Some_fresh in H. subst kn. destruct X1. contradiction.
 Qed.
 
 Lemma lookup_env_ext {Σ kn kn' d d'} : 
@@ -1259,7 +1259,7 @@ Proof.
   intros wf hl. 
   eapply lookup_env_Some_fresh in hl.
   inv wf. inv X.
-  destruct (eqb_spec kn kn'); subst; congruence.
+  destruct (eqb_spec kn kn'); subst; destruct X1; congruence.
 Qed.
 
 Lemma lookup_env_cons_disc {Σ kn kn' d} : 
@@ -1288,11 +1288,11 @@ Proof.
   exists cst. split.
   red in declc |- *. unfold lookup_env in *.
   rewrite lookup_env_cons_fresh //.
-  { eapply lookup_env_Some_fresh in declc.
+  { eapply lookup_env_Some_fresh in declc. destruct X1. 
     intros <-; contradiction. }
   exists cst'.
   unfold EGlobalEnv.declared_constant. rewrite EGlobalEnv.elookup_env_cons_fresh //.
-  { eapply lookup_env_Some_fresh in declc.
+  { eapply lookup_env_Some_fresh in declc. destruct X1. 
     intros <-; contradiction. }
   red in ebody. unfold erases_constant_body.
   destruct (cst_body cst) eqn:bod; destruct (E.cst_body cst') eqn:bod' => //.
@@ -1327,7 +1327,7 @@ Proof.
   unfold lookup_env in *.
   rewrite lookup_env_cons_fresh //.
   { eapply lookup_env_Some_fresh in declc.
-    intros <-. contradiction. }
+    intros <-. destruct X1. contradiction. }
   exists cst'.
   unfold EGlobalEnv.declared_constant.
   red in ebody. unfold erases_constant_body.
@@ -1462,7 +1462,9 @@ Proof.
           cbn in o0, o. rewrite prf' in o0. rewrite  <- Hpop in o0. rewrite Hpop' in o. clear -o o0. 
           now depelim o0.
           depelim wf. rewrite Hpop' in o0.
-          cbn in o0, o. rewrite prf' in o0.  rewrite <- Hpop in o0. clear -o0.  now depelim o0. }
+          cbn in o0, o. rewrite prf' in o0.  rewrite <- Hpop in o0. clear -o0. depelim o0.
+          now destruct o.
+           }
         all: eauto. 
         apply IHdecls; eauto. 
         { intros. pose proof (abstract_env_wf _ wfpop) as [wf'].
@@ -1603,11 +1605,12 @@ Lemma on_global_env_ind (P : forall Σ : global_env, wf Σ -> Type)
     (pd : on_global_decl cumulSpec0 (lift_typing typing) 
     ({| universes := Σ.(universes); declarations := Σ.(declarations); retroknowledge := Σ.(retroknowledge) |}, udecl) kn d),
     P Σ wf -> P (add_global_decl Σ (kn, d)) 
-    (fst wf, globenv_decl _ _ Σ.(universes) Σ.(retroknowledge) Σ.(declarations) kn d (snd wf) Hfresh onud pd))
+    (fst wf, globenv_decl _ _ Σ.(universes) Σ.(retroknowledge) Σ.(declarations) kn d (snd wf) 
+            {| kn_fresh := Hfresh ; on_udecl_udecl := onud ; on_global_decl_d := pd |}))
   (Σ : global_env) (wfΣ : wf Σ) : P Σ wfΣ.
 Proof.
   destruct Σ as [univs Σ]. destruct wfΣ; cbn in *.
-  induction o0. apply Pnil.
+  induction o0. apply Pnil. destruct o1. 
   apply (Pcons {| universes := univs; declarations := Σ |} kn d (o, o0)).
   exact IHo0.
 Qed.
@@ -2122,19 +2125,19 @@ Proof.
   + constructor. eapply IHdecls => //; eauto. eapply erase_global_cst_decl_wf_glob; auto.
     eapply erase_global_decls_fresh; auto.
     destruct wfΣ. destruct wfΣpop.
-    rewrite (heq _ wf) in o0. now depelim o0.
+    rewrite (heq _ wf) in o0. depelim o0. now destruct o3.
   + cbn. eapply IHdecls; eauto. 
   + constructor. eapply IHdecls; eauto. 
     destruct wfΣ as [[onu ond]]. 
-    rewrite (heq _ wf) in o. depelim o.
+    rewrite (heq _ wf) in o. depelim o. destruct o0. 
     eapply (erase_global_ind_decl_wf_glob (kn:=kn)); tea.
     intros. rewrite (abstract_env_irr _ H wfpop). 
     unshelve epose proof (abstract_pop_decls_correct X decls _ _ _ wf wfpop) as [? ?].
     {intros; now eexists. }
     destruct Σpop, Σ; cbn in *. now subst.
     eapply erase_global_decls_fresh.
     destruct wfΣ as [[onu ond]].
-    rewrite (heq _ wf) in o. now depelim o.
+    rewrite (heq _ wf) in o. depelim o. now destruct o0. 
   + eapply IHdecls; eauto. 
 Qed.
 
@@ -2167,7 +2170,7 @@ Proof.
       eapply erase_global_cst_decl_wf_glob. 
       eapply erase_global_decls_fresh => //.
       pose proof (abstract_env_wf _ wf) as [wfΣ].
-      depelim wfΣ. rewrite (prf _ wf) in o0. clear - o0. now depelim o0.
+      depelim wfΣ. rewrite (prf _ wf) in o0. clear - o0. depelim o0. now destruct o. 
       unfold eg', eg'', hidebody. 
       erewrite erase_global_decls_irr.
       eapply IHdecls.
@@ -2188,12 +2191,12 @@ Proof.
       { now eexists. }
       destruct Σ, Σ0. cbn in *. rewrite prf' in wfΣ.
       depelim wfΣ. cbn in *. rewrite <- H1, H0, <- H2. 
-      now depelim o0.
+      depelim o0. now destruct o1. 
       eapply erase_global_decls_fresh => //.
       pose proof (abstract_env_wf _ wf) as [wfΣ].
       pose proof (prf _ wf) as prf'.
       destruct Σ. cbn in *. rewrite prf' in wfΣ.
-      clear -wfΣ. destruct wfΣ. cbn in *. now depelim o0.
+      clear -wfΣ. destruct wfΣ. cbn in *. depelim o0. now destruct o1. 
       unfold eg'', hidebody. erewrite erase_global_decls_irr.
       eapply IHdecls. intros x hin. now eapply sub.
       eapply IHdecls => //. }
@@ -2526,8 +2529,8 @@ Next Obligation.
   pose proof (abstract_env_wf _ H) as [?].
   specialize_Σ H. sq. split. cbn. apply X3. cbn. 
   eapply decls_prefix_wf in X3; tea.
-  destruct X3 as [onu ond]. cbn in ond.
-  now depelim ond.
+  destruct X3 as [onu ond]. cbn in ond. 
+  depelim ond. now destruct o. 
 Qed.
 Next Obligation.
   pose proof (abstract_env_ext_wf _ H) as [?].
@@ -2569,7 +2572,7 @@ Proof.
   induction suffix.
   - cbn. rewrite eqb_refl //.
   - cbn. intros ond.
-    depelim ond. cbn. red in f.
+    depelim ond. destruct o as [f ? ? ? ]. cbn. red in f.
     eapply Forall_app in f as []. depelim H0. cbn in H0.
     destruct (eqb_spec kn kn0); [contradiction|].
     now apply IHsuffix.

pcuic/theories/PCUICExpandLetsCorrectness.v

@@ -4680,15 +4680,15 @@ Lemma trans_wf {cf} {Σ : global_env_ext} : wf Σ -> wf_trans Σ.
 Proof.
   rewrite /PCUICEnvironment.fst_ctx.
   destruct Σ as [[gunivs Σ retro] udecl]; cbn. intros [onu wfΣ]; cbn in *.
-  induction wfΣ as [|Σ0 kn d X IHX f udecl' onu' ond]. constructor; auto. constructor.
+  induction wfΣ as [|Σ0 kn d X IHX [f udecl' onu' ond]]. constructor; auto. constructor.
   have onud : on_udecl gunivs (PCUICLookup.universes_decl_of_decl (trans_global_decl d)).
   { apply (trans_on_udecl (Σ:= {| universes := gunivs; declarations := Σ0; retroknowledge := retro |})) in onu'. destruct d => //. }
   cbn; constructor; eauto.
   rename Σ0 into Σd.
   set (Σ0 := {| universes := gunivs; declarations := Σd; retroknowledge := retro |}).
   rename X into Xd.
   set (X := (onu, Xd) : wf Σ0).
-  constructor; auto; try apply IHX.
+  constructor; try constructor; auto; try apply IHX.
   { now apply (fresh_global_map (Σ := Σ0)). }
   destruct d; cbn in *.
   * cbn. red. move: ond; rewrite /on_constant_decl.

pcuic/theories/PCUICFirstorder.v

@@ -393,11 +393,12 @@ Proof.
   - cbn => //.
   - cbn. destruct a => //. intros gs ong.
     depelim ong. specialize (IHΣ'' _ ong).
+    destruct o as [f ? ? ?]. 
     destruct g => //.
     * intros hl. specialize (IHΣ'' hl).
       eapply plookup_env_Some_not_fresh in hl.
       cbn. case: eqb_spec.
-      + intros <-. apply fresh_global_app in f as [].
+      + intros <-.  apply fresh_global_app in f as [].
         contradiction.
       + now intros neq.
     * intros hl. specialize (IHΣ'' hl).

pcuic/theories/PCUICTyping.v

@@ -776,10 +776,12 @@ Proof.
     unfold Σg in o |- *; cbn in o.
     rename o into ongu. rename o0 into o. cbn in o |- *.
     destruct o. { constructor. }
-    rename o1 into Xg.
+    rename o0 into Xg.
     set (wfΣ := (ongu, o) : on_global_env cumulSpec0 (lift_typing typing) {| universes := univs; declarations := Σ |}).
     set (Σ':= {| universes := univs; declarations := Σ |}) in *.
-    constructor; auto.
+    destruct Xg. 
+    rename on_global_decl_d into Xg. 
+    constructor; auto; try constructor; auto.
     * unshelve eset (IH' := IH ((Σ', udecl); (wfΣ; []; (tSort Universe.lProp); _; _))).
       shelve. simpl. apply type_Prop.
       forward IH'. constructor 1; cbn. lia.
@@ -1252,7 +1254,7 @@ Section All_local_env.
         exists [(kn, decl)] => //.
         apply Retroknowledge.extends_refl.
       * split => //.
-      * apply o0.
+      * destruct o; assumption.
     - intros hl. destruct (IHΣp hl) as [Σ' []].
       exists Σ'.
       split=> //.