8.18 warnings and deprecations fixes

common/theories/BasicAst.v

@@ -245,9 +245,9 @@ Notation TermoptTyp tm typ := (Judge tm typ None).
 Notation TypUniv ty u := (Judge None ty (Some u)).
 Notation TermTypUniv tm ty u := (Judge (Some tm) ty (Some u)).
 
-Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)).
-Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)).
-Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)).
+Notation j_vass na ty := (Typ ty (* na.(binder_relevance) *)) (only parsing).
+Notation j_vass_s na ty s := (TypUniv ty s (* na.(binder_relevance) *)) (only parsing).
+Notation j_vdef na b ty := (TermTyp b ty (* na.(binder_relevance) *)) (only parsing).
 Notation j_decl d := (TermoptTyp (decl_body d) (decl_type d) (* (decl_name d).(binder_relevance) *)).
 Notation j_decl_s d s := (Judge (decl_body d) (decl_type d) s (* (decl_name d).(binder_relevance) *)).
 

common/theories/Environment.v

@@ -4,6 +4,8 @@ From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes.
 From Equations.Prop Require Import Classes EqDecInstances.
 
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Module Type Term.
 
   Parameter Inline term : Type.

common/theories/EnvironmentReflect.v

@@ -4,6 +4,8 @@ From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes Environment Reflect.
 From Equations.Prop Require Import Classes EqDecInstances.
 
+Ltac Tauto.intuition_solver ::= auto with *.
+
 Module EnvironmentReflect (T : Term) (Import E : EnvironmentSig T) (Import TDec : TermDecide T) (Import EDec : EnvironmentDecide T E).
 
   Local Notation extendsb_decls_part Σ Σ'

common/theories/EnvironmentTyping.v

@@ -1012,12 +1012,12 @@ Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E).
 
   Notation lift_sorting_size csize ssize := (lift_sorting_size_gen csize ssize 1).
   Notation typing_sort_size typing_size := (fun t s (tu: typing_sort _ t s) => typing_size t (tSort s) tu).
-  Notation lift_typing_size typing_size := (lift_sorting_size_gen typing_size (typing_sort_size typing_size) 0).
+  Notation lift_typing_size typing_size := (lift_sorting_size_gen typing_size%function (typing_sort_size typing_size%function) 0).
   Notation typing_sort_size1 typing_size := (fun Γ t s (tu: typing_sort1 _ Γ t s) => typing_size Γ t (tSort s) tu).
   Notation on_def_type_sorting_size ssize := (on_def_type_size_gen ssize 1).
   Notation on_def_type_size typing_size := (on_def_type_size_gen (typing_sort_size1 typing_size) 0).
   Notation on_def_body_sorting_size csize ssize := (on_def_body_size_gen csize ssize 1).
-  Notation on_def_body_size typing_size := (on_def_body_size_gen typing_size (typing_sort_size1 typing_size) 0).
+  Notation on_def_body_size typing_size := (on_def_body_size_gen typing_size%function (typing_sort_size1 typing_size%function) 0).
   (* Will probably not pass the guard checker if in a list, must be unrolled like in on_def_* *)
 
   Lemma lift_sorting_size_impl {checking sorting Qc Qs j} csize ssize :

common/theories/uGraph.v

@@ -2144,28 +2144,30 @@ Section CheckLeq2.
     contradiction HG.
   Defined.
 
-  Let Huctx': global_gc_uctx_invariants uctx'.
+  #[clearbody] Let Huctx' : global_gc_uctx_invariants uctx'.
     unfold uctx'; cbn.
     eapply gc_of_uctx_invariants; tea.
     unfold is_graph_of_uctx, gc_of_uctx in *. cbn.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     reflexivity. contradiction HG.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let HC' : gc_consistent uctx'.2.
     unfold uctx'; cbn. clear Huctx'.
     apply gc_consistent_iff in HC.
     unfold is_graph_of_uctx, gc_of_uctx in *.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     exact HC. contradiction HG.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let HG' : Equal_graph G (make_graph uctx').
     unfold uctx' in *; cbn. clear Huctx'.
     unfold is_graph_of_uctx, gc_of_uctx in *.
     destruct (gc_of_constraints uctx.2) as [ctrs|].
     symmetry; exact HG. contradiction HG.
-  Qed.
+  Defined.
 
   Let level_declared (l : Level.t) := LevelSet.In l uctx.1.
 

erasure-plugin/theories/ErasureCorrectness.v

@@ -292,17 +292,27 @@ Section PCUICProof.
     lookup_env Σ kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl') ->
     decl = erase_mutual_inductive_body decl').
 
+  Definition erase_decl_equal cmp decl decl' :=
+    match decl, decl' with 
+        EAst.InductiveDecl decl , InductiveDecl decl' => decl = cmp decl'
+      | EAst.ConstantDecl _ , ConstantDecl _ => True
+      | _ , _ => False 
+    end. 
+
   Lemma lookup_env_in_erase_global_deps X_type X deps decls kn normalization_in prf decl :
     EnvMap.EnvMap.fresh_globals decls ->
-    EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some (EAst.InductiveDecl decl) ->
-    exists decl', lookup_global decls kn = Some (InductiveDecl decl') /\ decl = erase_mutual_inductive_body decl'.
+    EGlobalEnv.lookup_env (erase_global_deps X_type deps X decls normalization_in prf).1 kn = Some decl ->
+    exists decl', lookup_global decls kn = Some decl' /\ 
+                  erase_decl_equal erase_mutual_inductive_body decl decl'.
   Proof.
     induction decls in deps, X, normalization_in, prf |- *; cbn [erase_global_deps] => //.
     destruct a => //. destruct g => //.
     - case: (knset_mem_spec k deps) => // hdeps.
       cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global].
       { destruct (eqb_spec kn k) => //.
-        intros hl. eapply IHdecls. now depelim hl. }
+        intro hl; depelim hl; cbn. intro e; noconf e.  
+        eexists; split; eauto. cbn; eauto.    
+        intros hl. cbn. eapply IHdecls. now depelim hl. }
       { intros hl. depelim hl.
         intros hl'.
         eapply IHdecls in hl. destruct hl.
@@ -311,12 +321,12 @@ Section PCUICProof.
         destruct (eqb_spec kn k) => //. subst k.
         destruct H0.
         now eapply PCUICWeakeningEnv.lookup_global_Some_fresh in H0.
-        exact hl'. }
+        exact hl'. } 
     - intros hf; depelim hf.
       case: (knset_mem_spec k deps) => // hdeps.
       cbn [EGlobalEnv.lookup_env fst lookup_env lookup_global].
-      { destruct (eqb_spec kn k) => //.
-        intros hl. noconf hl. subst k. eexists; split; cbn; eauto.
+      { destruct (eqb_spec kn k) => //; cbn.
+        intros hl. noconf hl. subst k. eexists; split; cbn; eauto. cbn; eauto.  
         intros hl'. eapply IHdecls => //. tea. }
       { intros hl'. eapply IHdecls in hf; tea. destruct hf.
         exists x.
@@ -1663,15 +1673,15 @@ Section pipeline_theorem.
   Import PCUICWfEnv.
 
   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}  :
-    EGlobalEnv.lookup_env Σ_v kn = Some (EAst.InductiveDecl decl) ->
+    EGlobalEnv.lookup_env Σ_t kn = Some decl ->
     exists decl',
       PCUICAst.PCUICEnvironment.lookup_global (PCUICExpandLets.trans_global_decls
-      (PCUICAst.PCUICEnvironment.declarations
-         Σ.1)) kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl')
-       /\ decl = ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl').
+      (PCUICAst.PCUICEnvironment.declarations Σ.1)) kn = Some decl'
+      /\  erase_decl_equal (fun decl => ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl))
+             decl decl'.
   Proof.
     Opaque compose.
-    unfold Σ_v, verified_erasure_pipeline.
+    unfold Σ_t, verified_erasure_pipeline.
     repeat rewrite -transform_compose_assoc.
     destruct_compose; intro. cbn.
     destruct_compose; intro. cbn.
@@ -1713,21 +1723,18 @@ Section pipeline_theorem.
     intro.
     set (EAstUtils.term_global_deps _).
     set (build_wf_env_from_env _ _).
-    epose proof
-      (lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0
-      _ kn _ Hyp0).
     set (EGlobalEnv.lookup_env _ _).
     case_eq o. 2: { intros ?. inversion 1. }
-    destruct g3; intro Ho; [inversion 1|].
-    cbn. inversion 1.
-    specialize (H8 m). forward H8.
-    epose proof (wf_fresh_globals _ HΣ). clear - H10.
-    revert H10. cbn. set (Σ.1). induction 1; econstructor; eauto.
-    cbn. clear -H. induction H; econstructor; eauto.
-    unfold o in Ho; rewrite Ho in H8.
-    specialize (H8 eq_refl).
-    destruct H8 as [decl' [? ?]]. exists decl'; split ; eauto.
-    rewrite <- H10. now destruct decl, m.
+    intros decl' Heq.
+    unshelve epose proof
+      (Hlookup := lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0
+      _ kn _ Hyp0 decl' _ Heq).
+    { epose proof (wf_fresh_globals _ HΣ). clear - H8.
+      revert H8. cbn. set (Σ.1). induction 1; econstructor; eauto.
+      cbn. clear -H. induction H; econstructor; eauto. }
+    destruct Hlookup as [decl'' [? ?]]. exists decl''; split ; eauto.
+    cbn in H10. inversion H10. 
+    now destruct decl' , decl''.
   Qed.
 
   Lemma verified_erasure_pipeline_firstorder_evalue_block :

erasure/theories/EArities.v

@@ -835,7 +835,7 @@ Proof.
   rewrite oib.(ind_arity_eq).
   rewrite /isPropositionalArity !destArity_it_mkProd_or_LetIn /=.
   destruct (Sort.is_propositional (ind_sort x0)) eqn:isp; auto.
-  elimtype False; eapply ise.
+  exfalso; eapply ise.
   red. eexists; intuition eauto. right.
   unfold type_of_constructor in e, X.
   destruct s as [indctors [nthcs onc]].

erasure/theories/EConstructorsAsBlocks.v

@@ -67,7 +67,7 @@ Section transform_blocks.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
     - change (fun x => size (id x)) with size in H.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H.
@@ -82,6 +82,8 @@ Section transform_blocks.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - eapply (In_size dbody size) in H; lia.
+    - eapply (In_size dbody size) in H; lia.
     - now eapply InPrim_size in H.
   Qed.
 

erasure/theories/EEtaExpanded.v

@@ -79,23 +79,18 @@ Section isEtaExp.
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
-    all:try apply (In_size); tea.
-    all:try lia.
-    - now apply (In_size id size).
-    - rewrite size_mkApps.
-      eapply (In_size id size) in H.
-      change (fun x => size (id x)) with size in H. unfold id in *; cbn.
-      lia.
-    - now eapply size_mkApps_f.
-    - change (fun x => size (id x)) with size in H.
-      eapply (In_size id size) in H. unfold id in H.
-      change (fun x => size x) with size in H.
-      pose proof (size_mkApps_l napp nnil). lia.
+    3:now eapply size_mkApps_f.
+    3:{ pose proof (size_mkApps_l napp nnil).
+        setoid_rewrite <- (In_size id size H) in H0. unfold id in H0. lia. }
+    all:try rewrite size_mkApps.
+    all:try setoid_rewrite <- (In_size id size H); unfold id.
+    all: try (cbn; lia).
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; intuition eauto.
       subst. lia.
-      eapply (In_size id size) in H0. unfold id in H0.
-      change (fun x => size x) with size in H0. lia.
+      setoid_rewrite <- (In_size id size H0); unfold id. lia.
   Qed.
 
 End isEtaExp.

erasure/theories/EEtaExpandedFix.v

@@ -176,6 +176,7 @@ Inductive expanded_global_declarations : forall (Σ : global_declarations), Prop
 | expanded_global_nil : expanded_global_declarations []
 | expanded_global_cons decl Σ : expanded_global_declarations Σ ->
   expanded_decl Σ decl.2 -> expanded_global_declarations (decl :: Σ).
+Derive Signature for expanded_global_declarations.
 
 Definition expanded_global_env := expanded_global_declarations.
 
@@ -301,7 +302,8 @@ Section isEtaExp.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
+    - setoid_rewrite (In_size id size); tea. unfold id.
+      now change (fun x => size x) with size.
     - rewrite size_mkApps. cbn.
       apply (In_size id size) in H.
       unfold id in H. change (fun x => size x) with size in H. lia.
@@ -320,6 +322,7 @@ Section isEtaExp.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H. cbn in H; lia.
     - destruct p as [? []]; cbn in *; eauto. destruct H; subst; try lia.
       eapply (In_size id size) in H. unfold id in H.
       change (fun x => size x) with size in H. lia.

erasure/theories/EImplementBox.v

@@ -59,9 +59,11 @@ Section implement_box.
     all:try lia.
     all:try apply (In_size); tea.
     all:try lia.
-    - now apply (In_size id size).
-    - now eapply (In_size id size).
-    - eapply (In_size snd size) in H. cbn in *. lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size id size H); unfold id; lia.
+    - setoid_rewrite <- (In_size snd size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
+    - setoid_rewrite <- (In_size dbody size H); cbn; lia.
     - now eapply InPrim_size in H.
   Qed.
 

erasure/theories/ERemoveParams.v

@@ -63,7 +63,8 @@ Section strip.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
-    - now eapply (In_size id size).
+    - eapply (In_size id size) in H. unfold id in H.
+      change (fun x => size x) with size in *. lia.
     - rewrite size_mkApps.
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H.  cbn. lia.
     - rewrite size_mkApps.
@@ -72,6 +73,8 @@ Section strip.
     - pose proof (size_mkApps_l napp nnil).
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H. lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
+    - eapply (In_size dbody size) in H; cbn in H; lia.
     - destruct p as [? []]; cbn in H; eauto.
       intuition auto; subst; cbn; try lia.
       eapply (In_size id size) in H0. unfold id in H0.

erasure/theories/EWcbvEvalNamed.v

@@ -1976,7 +1976,7 @@ Proof.
                        lazymatch B with context[x] => idtac | context[z] => idtac end;
                        pose proof (pair H H'); clear H H'
                   end.
-           revert dependent x; intros x H'; exact H'. }
+           generalize dependent x; intros x H'; exact H'. }
        assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. { let X := match goal with H : All2 _ ?x ?y |- context[All3 _ _ ?x ?y] => H end in
          clear - X; induction X. eexists; econstructor. repeat (destruct_head'_sigT; destruct_head'_prod).
          eexists (_ :: _). econstructor; eauto.

erasure/theories/ErasureFunction.v

@@ -338,7 +338,7 @@ Proof.
 
     + intros hl.
       case: (knset_mem_spec kn0 _) => hin.
-      * elimtype False.
+      * exfalso.
         eapply lookup_global_deps in hl; tea.
         now eapply fresh_global_In in H1.
       * case: (knset_mem_spec kn0 _).
@@ -668,7 +668,7 @@ Proof.
     * rewrite global_deps_union KernameSet.union_spec.
       intros [] fr.
     ** depelim fr. now eapply IHΣ.
-    ** depelim fr. elimtype False. eapply IHΣ in H1; eauto.
+    ** depelim fr. exfalso. eapply IHΣ in H1; eauto.
       destruct d as [[[]]|] eqn:eqd; cbn in H.
       + cbn in H1. eapply (term_global_deps_fresh Σ) in H1; tea. cbn in H2.
         eapply (Forall_map (fun x => x <> kn) fst) in fr.