Fix warnings

Author: 4ever2

embedding/theories/EvalE.v

@@ -8,6 +8,7 @@ From ConCert.Utils Require Import Env.
    but (as actually comment in the [monad_utils] says, we
    should use a real monad library) *)
 (* We need some definitions like [All] from utils *)
+#[warnings="-notation-incompatible-prefix"]
 From MetaCoq.Utils Require Import utils.
 
 From Coq Require Import String.

embedding/theories/Misc.v

@@ -94,7 +94,7 @@ Section CombineProp.
     + simpl. intros l1 Heq. destruct l1; eauto.
       simpl; destruct (rev l1 ++ [a]); reflexivity.
     + simpl. intros l1 Heq. destruct l1 using rev_ind; auto.
-      repeat rewrite app_length in Heq; simpl in *.
+      repeat rewrite length_app in Heq; simpl in *.
       assert (#|l1| = #|l2|) by lia.
       repeat rewrite rev_unit. simpl.
       rewrite IHl2 by auto.

embedding/theories/TranslationUtils.v

@@ -3,6 +3,7 @@ From ConCert.Embedding Require Utils.
 From ConCert.Embedding Require Import PCUICTranslate.
 From ConCert.Embedding Require Import PCUICtoTemplate.
 From ConCert.Utils Require Import Env.
+#[warnings="-notation-incompatible-prefix"]
 From MetaCoq.Template Require Import All.
 
 From Coq Require Import String.

embedding/theories/pcuic/PCUICCorrectness.v

@@ -95,7 +95,7 @@ Proof.
       assert (ty_expr_env_ok (exprs ρ # [e ~> of_val_i v0]) 0 e1_2).
       { change (exprs ρ # [e ~> of_val_i v0]) with (exprs (ρ # [e ~> v0])).
         eapply eval_ty_expr_env_ok; eauto with hints. simpl.
-        replace #|ρ| with (#|exprs ρ|) by apply map_length.
+        replace #|ρ| with (#|exprs ρ|) by apply length_map.
         eapply subst_env_iclosed_n_inv with (n := 1); eauto with hints. }
 
       assert (val_ok Σ1 v0) by (eapply eval_val_ok; eauto with hints).
@@ -135,7 +135,7 @@ Proof.
           now rewrite Hres. }
         rewrite Hc.
         eapply IHn; eauto with hints.
-        repeat rewrite map_length. unfold PcbvCurr.cstr_arity. propify. lia.
+        repeat rewrite length_map. unfold PcbvCurr.cstr_arity. propify. lia.
       * destruct c.
         ** (* the closure corresponds to lambda *)
           simpl in *. rename e0 into n0.
@@ -300,7 +300,7 @@ Proof.
       destruct (resolve_inductive _ _) eqn:HresI; tryfalse.
       destruct (lookup_with_ind _ _) eqn:Hfind_i; tryfalse.
       destruct p as [nparams cs]. destruct p0 as [i ci]. simpl in *.
-      rewrite map_length.
+      rewrite length_map.
       destruct_match eqn:Hnparams; tryfalse.
       assert (HresC: resolve_constr Σ1 i0 e = Some (nparams,i, ci)).
       { unfold resolve_constr. rewrite HresI. rewrite Hfind_i. reflexivity. }
@@ -330,7 +330,7 @@ Proof.
       destruct H2 as [Hdctor?].
       eapply PcbvCurr.eval_iota; eauto.
       * now eapply map_nth_error.
-      * cbn. rewrite map_length. unfold PcbvCurr.cstr_arity. propify. lia.
+      * cbn. rewrite length_map. unfold PcbvCurr.cstr_arity. propify. lia.
       * cbn.
         unfold etrans_branch.
         unfold fun_prod,id; cbn.
@@ -343,8 +343,8 @@ Proof.
         rewrite Heq; cbn.
         assert (Hvass : forall xs, context_assumptions (map (fun '(nm, ty) => vass (aRelevant (nNamed (TCString.of_string nm))) ty) xs) = #|xs|).
         { intros; rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
-          now rewrite map_length. }
-        rewrite Hvass. rewrite combine_length, map_length.
+          now rewrite length_map. }
+        rewrite Hvass. rewrite length_combine, length_map.
         lia.
       * unfold iota_red in *. simpl in *.
         unfold expand_lets,expand_lets_k,inst_case_branch_context,inst_case_context; cbn.
@@ -358,7 +358,7 @@ Proof.
         inversion Hnth_eq; subst; clear Hnth_eq.
         assert (Heq : (#|pVars v2.1| =? #|remove_proj c|)%nat) by (propify; lia).
         rewrite Heq; cbn.
-        repeat rewrite map_length. rewrite combine_length,map_length.
+        repeat rewrite length_map. rewrite length_combine,length_map.
         replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
         rewrite <- map_skipn.
         rewrite <- map_rev.
@@ -401,12 +401,12 @@ Proof.
         specialize (find_forallb_map _ Hfnd HH) as Hclosed_t2; cbn in Hclosed_t2.
 
         erewrite PCUICInstConv.subst_id with (s := rev (_)); eauto.
-        2: { rewrite rev_length. rewrite to_extended_list_k_length. rewrite Hvass_eq.
-             subst g. repeat rewrite map_length. rewrite combine_length.
+        2: { rewrite length_rev. rewrite to_extended_list_k_length. rewrite Hvass_eq.
+             subst g. repeat rewrite length_map. rewrite length_combine.
              replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
              rewrite PCUICSigmaCalculus.context_assumptions_context.
              * rewrite subst_context_length.
-               repeat rewrite map_length. rewrite combine_length,map_length.
+               repeat rewrite length_map. rewrite length_combine,length_map.
                replace (min #|pVars v2.1| #|remove_proj c|) with (#|pVars v2.1|) by lia.
                replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
                rewrite <- Hf.
@@ -419,11 +419,11 @@ Proof.
                    (subst_context (rev (map (fun x : type => T⟦ subst_env_i_ty 0 (exprs ρ) x ⟧) l0)) 0 g)) = #|pVars v2.1|).
         { rewrite PCUICSigmaCalculus.context_assumptions_context by auto with hints.
           rewrite subst_context_length. subst g.
-          repeat rewrite map_length. rewrite combine_length.
+          repeat rewrite length_map. rewrite length_combine.
           replace #|remove_proj c| with #|pVars v2.1| by (propify; lia).
           now replace (min #|pVars v2.1| #|pVars v2.1|) with #|pVars v2.1| by lia.
         }
-        assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite skipn_length; lia).
+        assert (#|pVars v2.1| = #|skipn (ind_npars mib) l2|) by (rewrite length_skipn; lia).
 
         rewrite Hvass_eq1.
 
@@ -445,7 +445,7 @@ Proof.
                  rewrite <- map_map with (g := (expr_to_term Σ1) ∘ of_val_i)
                                         (f := snd).
                  rewrite map_combine_snd. now subst.
-                 now repeat rewrite rev_length. }
+                 now repeat rewrite length_rev. }
         rewrite Hmap. subst h te3.
         replace (#|pVars v2.1| + 0) with #|pVars v2.1| in * by lia.
         apply Nat.eqb_eq in Hnparams.
@@ -458,9 +458,9 @@ Proof.
            rewrite map_app.
            remember (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) as l_rev.
            assert (Hlrev : #|pVars v2.1| = #|exprs l_rev|).
-           { subst. rewrite map_length.
-             rewrite rev_length. rewrite combine_length.
-             rewrite skipn_length; lia. }
+           { subst. rewrite length_map.
+             rewrite length_rev. rewrite length_combine.
+             rewrite length_skipn; lia. }
            rewrite Hlrev.
            symmetry. eapply subst_env_swap_app with (n := 0);
              eauto with hints.
@@ -474,55 +474,55 @@ Proof.
            eapply subst_env_iclosed_0; eauto with hints.
            remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
            assert (Hlen : #|l_comb| = #|pVars v2.1|).
-           { subst. rewrite combine_length. rewrite map_length.
-             repeat rewrite rev_length. rewrite skipn_length; lia. }
+           { subst. rewrite length_combine. rewrite length_map.
+             repeat rewrite length_rev. rewrite length_skipn; lia. }
            rewrite <- Hlen.
            eapply ty_expr_env_ok_subst_env with (k := 0).
            assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))) = l_comb).
            { subst. repeat rewrite map_rev. rewrite combine_rev.
              apply f_equal. now rewrite map_combine_snd_funprod.
-             rewrite map_length. rewrite skipn_length; lia. }
+             rewrite length_map. rewrite length_skipn; lia. }
            rewrite <- Hcomb. rewrite <- map_app.
            eapply eval_ty_expr_env_ok; eauto with hints.
-           rewrite app_length.
+           rewrite length_app.
            replace (#|rev (combine (pVars v2.1) (skipn (ind_npars mib) l2))|) with #|pVars v2.1| by
-             (rewrite rev_length, combine_length, skipn_length; lia).
-           replace #|ρ| with #|exprs ρ| by apply map_length. eauto with hints.
+             (rewrite length_rev, length_combine, length_skipn; lia).
+           replace #|ρ| with #|exprs ρ| by apply length_map. eauto with hints.
 
            eapply closed_exprs; eauto.
 
            eapply All_snd_combine with (p := iclosed_n 0); eauto with hints.
            apply All_map. apply All_rev.
            eapply All_expr_iclosed_of_val; eauto using All_skipn.
 
-           rewrite combine_length. rewrite map_length.
-           repeat rewrite rev_length. rewrite skipn_length by lia.
+           rewrite length_combine. rewrite length_map.
+           repeat rewrite length_rev. rewrite length_skipn by lia.
            replace (min #|pVars v2.1| (#|l2| - ind_npars mib)) with #|pVars v2.1| by lia.
            eauto with hints.
 
         ** rewrite <- combine_rev by auto.
            rewrite map_combine_snd_funprod.
            remember ((combine (rev (pVars v2.1)) (map of_val_i (rev (skipn _ l2))))) as l_comb.
            assert (Hlen : #|l_comb| = #|pVars v2.1|).
-           { subst. rewrite combine_length. rewrite map_length.
-             repeat rewrite rev_length. rewrite skipn_length; lia. }
+           { subst. rewrite length_combine. rewrite length_map.
+             repeat rewrite length_rev. rewrite length_skipn; lia. }
            rewrite <- Hlen.
            eapply ty_expr_env_ok_subst_env with (k := 0).
            remember (ind_npars mib) as nparams.
            assert (Hcomb : exprs (rev (combine (pVars v2.1) (skipn nparams l2))) = l_comb).
            { subst. repeat rewrite map_rev. rewrite combine_rev.
              apply f_equal. now rewrite map_combine_snd_funprod.
-             rewrite map_length. rewrite skipn_length; lia. }
+             rewrite length_map. rewrite length_skipn; lia. }
            rewrite <- Hcomb. rewrite <- map_app.
            subst nparams. eapply eval_ty_expr_env_ok; eauto with hints.
-           rewrite app_length.
+           rewrite length_app.
            replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
-             (rewrite rev_length, combine_length, skipn_length; lia).
-           replace #|ρ| with #|exprs ρ| by apply map_length. eauto with hints.
+             (rewrite length_rev, length_combine, length_skipn; lia).
+           replace #|ρ| with #|exprs ρ| by apply length_map. eauto with hints.
            eapply closed_exprs; eauto.
-        ** rewrite map_length.
+        ** rewrite length_map.
            replace (#|rev (combine (pVars v2.1) (skipn _ l2))|) with #|pVars v2.1| by
-             (rewrite rev_length, combine_length, skipn_length; lia).
+             (rewrite length_rev, length_combine, length_skipn; lia).
            eauto with hints.
         ** apply All_map. subst.
            apply All_rev. unfold compose. simpl.

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -177,7 +177,7 @@ Proof.
   destruct (syncEnv _ _ _ _ _ Hres) as [[[??]?][?[??]]].
   erewrite <- mkApps_vars_to_apps_constr; eauto.
   eapply PcbvCurr.value_app.
-  + rewrite map_length. cbn in *.
+  + rewrite length_map. cbn in *.
     subst. rewrite H1 in *.
     econstructor; eauto.
   + now apply All_map.
@@ -420,7 +420,7 @@ Proof.
       assert (closed T⟦ t ⟧).
       { eapply nth_error_all in Hn; eauto; auto with hints. }
       now rewrite lift_closed by auto with hints.
-    * rewrite map_length. apply f_equal.
+    * rewrite length_map. apply f_equal.
       apply nth_error_None in Hn; lia.
   + f_equal; auto.
     rewrite <- IHty2 by auto.
@@ -632,7 +632,7 @@ Proof.
     inversion Hlen as [Hlen0]; subst; clear Hlen.
     propify; split.
     * inversion Htys; subst; apply IHtys; eauto.
-    * rewrite map_length, combine_length, map_length.
+    * rewrite length_map, length_combine, length_map.
       rewrite Hlen0. replace (Init.Nat.min #|tys| #|tys|) with #|tys| by lia.
       inversion Htys; subst; clear Htys.
       replace (#|tys| + n) with (n + #|tys|) by lia.
@@ -672,7 +672,7 @@ Proof.
       ** cbn. rewrite closedn_mkApps; eauto. cbn.
          replace (#|map type_to_term l0|) with
            (#|map (fun x : type => vass (aRelevant nAnon) T⟦ x ⟧) l0|)
-           by now repeat rewrite map_length.
+           by now repeat rewrite length_map.
          apply closedn_to_extended_list.
     * destruct p as [np cs]. cbn in *.
       rewrite forallb_map.
@@ -683,7 +683,7 @@ Proof.
       unfold etrans_branch in Heqtb.
       destruct (find (fun x => _)) as [ p0 | ] eqn:Hnm.
       2: subst; simpl; auto.
-      destruct p0 as [pt e1]. cbn in *. rewrite map_length in *.
+      destruct p0 as [pt e1]. cbn in *. rewrite length_map in *.
       destruct (#|pVars pt| =? #|tys|)%nat eqn:Hlen; auto.
       2: subst; simpl; auto.
       apply find_some in Hnm. destruct Hnm as [Hin' Heqs]; cbn in *.
@@ -698,7 +698,7 @@ Proof.
       propify; split.
       ** rewrite map_map.
          now apply closedn_ctx_branches.
-      ** rewrite map_length,combine_length. rewrite_all map_length.
+      ** rewrite length_map,length_combine. rewrite_all length_map.
          rewrite Hlen. replace (min #|tys| #|tys|) with (#|tys|) by lia.
          apply forallb_Forall in H3.
          eapply Forall_In in H; eauto; cbn in *.
@@ -718,8 +718,8 @@ Lemma closed_exprs_len_iff e n (ρ : env val) :
   iclosed_n (n + #|ρ|) e = true.
 Proof.
   split.
-  intros H. rewrite map_length in H. assumption.
-  intros H. rewrite map_length. assumption.
+  intros H. rewrite length_map in H. assumption.
+  intros H. rewrite length_map. assumption.
 Qed.
 
 
@@ -876,7 +876,7 @@ Proof.
     cbn in *. destruct p as [ind tys]. unfold is_true in *; simpl in *.
     propify. destruct Hc as [Hce1 Hce2].
     destruct (resolve_inductive Σ ind) eqn:Hres; auto.
-    rewrite map_length. destruct (_ =? _)%nat eqn:Hnparams; auto.
+    rewrite length_map. destruct (_ =? _)%nat eqn:Hnparams; auto.
     cbn.
     repeat f_equal.
     * unfold map_predicate_k; cbn.
@@ -894,7 +894,7 @@ Proof.
                       reln xs n (map (vass (aRelevant nAnon)) ys2)).
          { induction ys1; intros ys2 xs n Heq; destruct ys2; cbn in *; inversion Heq; cbn; auto. }
          rewrite <- map_map. rewrite <- map_map with (f := fun x => T⟦ x ⟧ {n1 := t⟦ e0 ⟧ Σ}).
-         apply Hreln. now repeat rewrite map_length.
+         apply Hreln. now repeat rewrite length_map.
       ** rewrite commut_lift_subst. auto with all hints solve_subterm.
     * apply IHe; auto with solve_subterm.
     * rewrite_all map_map. simpl.
@@ -920,10 +920,10 @@ Proof.
                (#|pVars (fst a)| + S n1) by lia.
            assumption. }
          rewrite <- Hmap. unfold id in *. rewrite Hfnd. simpl.
-         rewrite map_length.
+         rewrite length_map.
          destruct (Nat.eqb #|pVars (fst p0)| #|l0|) eqn:Hlen; simpl; auto.
-         unfold map_branch_k; cbn. rewrite_all map_length. rewrite combine_length.
-         rewrite_all map_length. rewrite PeanoNat.Nat.eqb_eq in Hlen.
+         unfold map_branch_k; cbn. rewrite_all length_map. rewrite length_combine.
+         rewrite_all length_map. rewrite PeanoNat.Nat.eqb_eq in Hlen.
          rewrite Hlen. replace (min _ _) with #|l0| by lia.
          f_equal.
       ** change (fun x : pat * term => pName (fst x) =? s)%string with
@@ -1324,8 +1324,8 @@ Proof.
   + unfold subst_env_i. destruct x as [nm e0]. simpl in *.
     apply All_app in Hall as [Hl He0]. inversion He0; subst; clear He0. simpl in *.
     unfold subst_env_i. rewrite map_app. simpl.
-    rewrite subst_app_simpl. rewrite map_length. simpl.
-    rewrite app_length in *. simpl in *.
+    rewrite subst_app_simpl. rewrite length_map. simpl.
+    rewrite length_app in *. simpl in *.
     replace (#|l| + 1) with (1 + #|l|) in Hc by lia.
     replace (k + (1 + #|l|)) with (1+ k + #|l|) in Hc by lia.
     rewrite subst_term_subst_env_rec with (e := e)(nm := nm) by eauto with hints.
@@ -1677,7 +1677,7 @@ Proof.
       simpl in Hge_ok. rewrite Hres in *.
       inversion Hok_constr. subst. clear Hok_constr.
       apply All_app_inv; eauto with hints.
-      rewrite app_length; cbn.
+      rewrite length_app; cbn.
       now propify; cbn in *.
     * simpl in *. unfold is_true in *; repeat rewrite Bool.andb_true_iff in *.
       assert (Hok_v0 : val_ok Σ v0) by now eapply IHn.
@@ -1725,7 +1725,7 @@ Proof.
     { apply rev_env_ok; apply All_env_ok; eauto; eapply All_skipn; eauto. }
 
     assert (iclosed_n #|rev (combine (pVars pt) (skipn n1 l1)) ++ ρ| e2 = true).
-    { rewrite app_length. rewrite rev_length,combine_length,skipn_length.
+    { rewrite length_app. rewrite length_rev,length_combine,length_skipn.
       replace (min #|pVars pt| (#|l1| - n1)) with #|pVars pt| by lia.
       now specialize (find_forallb _ H H4) as Hc. }
     eapply IHn with (ρ := (rev (combine (pVars pt) (skipn n1 l1)) ++ ρ)); eauto.
@@ -1880,11 +1880,11 @@ Lemma of_val_closed_0 e ρ :
   iclosed_n 0 (e.[exprs ρ]) = true -> iclosed_n #|ρ| e.
 Proof.
   intros H ?.
-  replace #|ρ| with (#|exprs ρ|) by now apply map_length.
+  replace #|ρ| with (#|exprs ρ|) by now apply length_map.
   eauto with hints.
 Qed.
 
-#[export] Hint Resolve map_length of_val_closed_0 val_ok_ge_val_ok rev_length
+#[export] Hint Resolve length_map of_val_closed_0 val_ok_ge_val_ok length_rev
   subst_env_compose_1 subst_env_compose_2 : hints.
 
 #[export] Hint Constructors PcbvCurr.value : hints.

embedding/theories/pcuic/PCUICFacts.v

@@ -383,7 +383,7 @@ Section Values.
               unfold AllEnv,compose,fun_prod in *.
               eapply All_impl_inner. apply X0.
               now eapply (All_impl X).
-          ** now rewrite map_length.
+          ** now rewrite length_map.
       * unfold subst_env_i. simpl in *.
         inversion Hv. subst.
         propify. destruct_and_split.
@@ -404,7 +404,7 @@ Section Values.
                unfold AllEnv,compose,fun_prod in *.
                eapply All_impl_inner. apply X0.
                now eapply (All_impl X).
-           *** now rewrite map_length.
+           *** now rewrite length_map.
     + simpl in *.
       inversion Hv. subst. clear Hv.
       eapply iclosed_m_n with (n := 1).
@@ -414,7 +414,7 @@ Section Values.
           unfold AllEnv,compose,fun_prod in *.
           eapply All_impl_inner. apply X0. simpl.
           now eapply (All_impl X).
-      ** now rewrite map_length.
+      ** now rewrite length_map.
     + simpl.
       inversion Hv. subst.
       eauto with facts.

embedding/theories/pcuic/PCUICTranslate.v

@@ -27,7 +27,7 @@ Import ListNotations.
 
 (** ** Translation of types *)
 
-Reserved Notation "T⟦ ty ⟧ " (at level 5).
+Reserved Notation "T⟦ ty ⟧ " (at level 0).
 
 (** Translation of types to PCUIC terms. Universal types become Pi-types with the
     first argument being of type [Set]. Keeping them in [Set] is crucial,

examples/AllTests.v

@@ -2,6 +2,7 @@ Set Warnings "-extraction-inside-module".
 
 From Coq Require Import BinNat.
 From ConCert.Execution Require Import Blockchain.
+#[warnings="-notation-incompatible-prefix"]
 From ConCert.Execution.Test Require Import QCTest.
 From ConCert.Examples.Congress Require CongressTests.
 From ConCert.Examples.Congress Require Congress_BuggyTests.
@@ -174,7 +175,7 @@ Module EIP20Token.
   Time QuickChick (token_cb ~~> person_has_tokens creator 0).
   (* Success - found witness satisfying the predicate!
   +++ Failed (as expected) after 1 tests and 0 shrinks. (0 discards)*)
-  
+
   Time QuickChick (expectFailure (
     token_cb
     ~~~> (fun cs => if person_has_tokens creator 5 cs.(chain_state_env) then Some tt else None)