Fix a bunch of Coq 8.20 deprecations

Makefile

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
+COQVERSION=  8.19.1 or-else  8.19.2 or-else 8.20.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)

aes/list_utils.v

@@ -37,7 +37,7 @@ Qed.
 Lemma repeat_op_table_nat_length: forall {T: Type} (i: nat) (x: T) (f: T -> T),
   length (repeat_op_table_nat i x f) = i.
 Proof.
-  intros. induction i. reflexivity. simpl. rewrite app_length. simpl.
+  intros. induction i. reflexivity. simpl. rewrite length_app. simpl.
   rewrite IHi. lia.
 Qed.
 

concurrency/ghosts.v

@@ -1356,7 +1356,7 @@ Proof.
   - if_tac.
     + subst; rewrite nth_error_app2, Nat.sub_diag; auto.
     + intro X; apply H; rewrite nth_error_app1 in X; auto.
-      assert (t < length (l ++ [e]))%nat; [|rewrite app_length in *; simpl in *; lia].
+      assert (t < length (l ++ [e]))%nat; [|rewrite length_app in *; simpl in *; lia].
       rewrite <- nth_error_Some, X; discriminate.
 Qed.
 
@@ -1527,7 +1527,7 @@ Proof.
     + pose proof (hist_list_lt _ _ Hl) as Hn.
       intro t; specialize (Hn t).
       subst h0; simpl; if_tac; [contradiction|].
-      intro X; specialize (Hn X); rewrite app_length in Hn; simpl in Hn; lia.
+      intro X; specialize (Hn X); rewrite length_app in Hn; simpl in Hn; lia.
     + apply IHl.
       intros t e; specialize (Hl t e).
       subst h0; simpl; if_tac.
@@ -1537,7 +1537,7 @@ Proof.
         { erewrite nth_error_app1 by auto; reflexivity. }
         split; intro X.
         -- assert (t < length (l ++ [x]))%nat by (rewrite <- nth_error_Some, X; discriminate);
-             rewrite app_length in *; simpl in *; lia.
+             rewrite length_app in *; simpl in *; lia.
         -- assert (t < length l)%nat by (rewrite <- nth_error_Some, X; discriminate); contradiction.
     + unfold map_upd; subst h0; simpl.
       extensionality k'; if_tac; subst; auto.

concurrency/memory_lemmas.v

@@ -387,7 +387,7 @@ Module MemoryLemmas.
         rewrite List.app_nth2.
         rewrite NPeano.Nat.sub_diag. reflexivity.
         omega.
-      + rewrite List.app_length in H.
+      + rewrite List.length_app in H.
         simpl in H.
         rewrite NPeano.Nat.add_1_r in H.
         simpl in H.

floyd/Clightnotations.v

@@ -23,7 +23,7 @@ to make a post-hoc adjustment to the precedence and associativity levels of
 some operators.
 *)
 
-Global Set Warnings "-notation-overridden,-parsing".
+Global Set Warnings "-notation-incompatible-prefix,-notation-overridden,-parsing".
 
 Require Import compcert.export.Clightdefs.
 From Coq Require Import String List ZArith.

floyd/Component.v

@@ -322,7 +322,7 @@ Proof.
   + split; trivial.
     eapply semax_external_binaryintersection. apply EXT1. apply EXT2.
       apply BI.
-      rewrite Sig2; simpl. rewrite map_length. trivial. 
+      rewrite Sig2; simpl. rewrite length_map. trivial. 
 Qed.
 
 Lemma find_funspec_sub: forall specs' specs 

floyd/base2.v

@@ -17,7 +17,9 @@ Fixpoint delete_id {A: Type} i (al: list (ident*A)) : option (A * list (ident*A)
   | nil => None
  end.
 
+Unset Automatic Proposition Inductives.
 Inductive Impossible : Type := .
+Set Automatic Proposition Inductives.
 
 Definition cc_of_fundef (fd: Clight.fundef) : calling_convention :=
  match fd with

floyd/canon.v

@@ -11,7 +11,7 @@ Inductive localdef : Type :=
  | lvar: ident -> type -> val -> localdef   (* local variable *)
  | gvars: globals -> localdef.              (* global variables *)
 
-Arguments temp i%positive v.
+Arguments temp i%_positive v.
 
 Definition lvar_denote (i: ident) (t: type) (v: val) rho :=
      match Map.get (ve_of rho) i with
@@ -502,7 +502,7 @@ Notation "'EX' x .. y , P " :=
 Notation " 'ENTAIL' d ',' P '|--' Q " :=
   (@derives (environ->mpred) _ (andp (local (tc_environ d)) P%assert) Q%assert) (at level 99, P at level 79, Q at level 79).
 
-Arguments semax {CS} {Espec} Delta Pre%assert cmd Post%assert.
+Arguments semax {CS} {Espec} Delta Pre%_assert cmd Post%_assert.
 
 Lemma insert_prop : forall (P: Prop) PP QR, prop P && (PROPx PP QR) = PROPx (P::PP) QR.
 Proof.

floyd/data_at_lemmas.v

@@ -780,7 +780,7 @@ intros.
 unfold decode_int.
 unfold rev_if_be.
 destruct Archi.big_endian.
-rewrite <- rev_length.
+rewrite <- length_rev.
 apply int_of_bytes_range.
 apply int_of_bytes_range.
 Qed.

floyd/finish.v

@@ -12,6 +12,8 @@ Require Import VST.floyd.deadvars.
 Require Import VST.floyd.step.
 Require Import VST.floyd.fastforward.
 
+Local Set Warnings "-ltac2-unused-variable".
+
 (* Things that we always want to simpl *)
 
 Ltac2 mutable simpl_safe_list () : constr list := [

floyd/forward.v

@@ -1253,7 +1253,9 @@ Ltac clear_MORE_POST :=
         clear MORE_COMMANDS
       end.
 
+Unset Automatic Proposition Inductives.
 Inductive Ridiculous: Type := .
+Set Automatic Proposition Inductives.
 
 Ltac check_witness_type ts A witness :=
   (unify A (rmaps.ConstType Ridiculous); (* because [is_evar A] doesn't seem to work *)

floyd/globals_lemmas.v

@@ -442,7 +442,7 @@ Lemma id2pred_star_ZnthV_Tint  {cs: compspecs} :
 Proof.
   intros. subst n mdata.
   replace (Zlength (map  (inttype2init_data sz) data)) with (Zlength data)
-    by (repeat rewrite Zlength_correct; rewrite map_length; auto).
+    by (repeat rewrite Zlength_correct; rewrite length_map; auto).
   go_lowerx.
   match goal with |- ?F _ _ _ _ _ _ |-- _ => change F with @id2pred_star end.
   change (offset_strict_in_range (sizeof (Tint sz sign noattr) * Zlength data) v) in H1.
@@ -694,7 +694,7 @@ Lemma id2pred_star_ZnthV_tfloat  {cs: compspecs}:
 Proof. intros.
   subst n mdata.
   replace (Zlength (map  (floattype2init_data sz) data)) with (Zlength data)
-    by (repeat rewrite Zlength_correct; rewrite map_length; auto).
+    by (repeat rewrite Zlength_correct; rewrite length_map; auto).
   go_lowerx.
   match goal with |- ?F _ _ _ _ _ _ |-- _ => change F with @id2pred_star end.
   change (offset_strict_in_range (sizeof (Tfloat sz noattr) * Zlength data) v) in H1.

floyd/proofauto.v

@@ -45,6 +45,7 @@ Require Export VST.floyd.diagnosis.
 Require Export VST.floyd.freezer.
 Require Export VST.floyd.deadvars.
 Require Export VST.floyd.hints.
+#[export] Set Warnings "-notation-incompatible-prefix".
 Require Export VST.floyd.Clightnotations.
 Require Export VST.floyd.data_at_list_solver.
 Require Export VST.floyd.data_at_lemmas.
@@ -58,7 +59,7 @@ Require VST.floyd.linking.
   "Require Import Require Import VST.floyd.Funspec_old_Notation."
   Global Close Scope funspec_scope.*)
 
-Arguments semax {CS} {Espec} Delta Pre%assert cmd%C Post%assert.
+Arguments semax {CS} {Espec} Delta Pre%_assert cmd%_C Post%_assert.
 Export ListNotations.
 Export Clight_Cop2.
 

floyd/subsume_funspec.v

@@ -105,8 +105,9 @@ Proof.
   rewrite <- derives_eq; auto.
 Qed.
  *)
-
+Unset Automatic Proposition Inductives.
 Inductive empty_type : Type := .
+Set Automatic Proposition Inductives.
 
 Definition withtype_of_NDfunspec fs := match fs with
   mk_funspec _ _ (rmaps.ConstType A) _ _ _ _ => A | _ => empty_type end.

hmacdrbg/HMAC_DRBG_nonadaptive.v

@@ -3864,7 +3864,7 @@ Proof.
         {
           assert (len_eq : length (to_list v) = length (to_list key_input ++ zeroes)).
           f_equal; trivial.
-          rewrite app_length in *.
+          rewrite length_app in *.
 
           repeat rewrite to_list_length in *.
           unfold zeroes in *.
@@ -3883,14 +3883,14 @@ Proof.
           destruct (in_split_l_if init _ in_fixed_len_list). eauto.
 
           unfold to_list in *.
-          apply inputs_len in H1; simpl in *; rewrite app_length in H1;
+          apply inputs_len in H1; simpl in *; rewrite length_app in H1;
             unfold zeroes in H1; rewrite length_replicate in H1;
               rewrite Nat.add_comm in H1; simpl in *.
           rewrite to_list_length in *. lia.
 
           (* match goal with  *)
           (*   | [ H1:  In (to_list key_input ++ zeroes, _) init |- _ ] =>  *)
-          (*      apply inputs_len in H1; simpl in *; rewrite app_length in H1; *)
+          (*      apply inputs_len in H1; simpl in *; rewrite length_app in H1; *)
           (*      unfold zeroes in H1; rewrite length_replicate in H1; *)
           (*      rewrite Nat.add_comm in H1; simpl in *; discriminate *)
           (* end. *)

hmacdrbg/HMAC_DRBG_pure_lemmas.v

@@ -162,7 +162,7 @@ Proof.
                (Z.of_nat n0 * 32 + 32 - Z.of_nat 32)) as result; destruct result.
     simpl.
     rewrite Zlength_correct.
-    rewrite app_length.
+    rewrite length_app.
     rewrite Nat2Z.inj_add.
     do 2 rewrite <- Zlength_correct.
     rewrite Hlength.

hmacdrbg/entropy_lemmas.v

@@ -140,7 +140,7 @@ Proof.
   remember (s0 0%nat) as s0_0.
   destruct s0_0; try solve [inversion H].
   inv H.
-  rewrite app_length.
+  rewrite length_app.
   simpl. replace (length l + 1)%nat with (S (length l)) by lia.
   rewrite IHk' with (s':=s0) (s:=s); auto.
 Qed.

mailbox/verif_mailbox_bad_write.v

@@ -89,7 +89,7 @@ Proof.
       entailer!.
       rewrite upd_Znth_eq with (d := Vundef); [|auto].
       apply derives_refl'; erewrite map_ext_in; [reflexivity|].
-      intros; rewrite In_upto, map_length, upto_length in *; simpl in *.
+      intros; rewrite In_upto, length_map, upto_length in *; simpl in *.
       erewrite Znth_map, Znth_upto; simpl; auto; try lia.
       erewrite sublist_split with (mid := i)(hi := i + 1), sublist_len_1 with (d := 0); auto; try lia.
       destruct (in_dec eq_dec a (sublist 0 i lasts ++ [Znth i lasts 0])); rewrite in_app in *.
@@ -1070,7 +1070,7 @@ Proof.
       rewrite !Zlength_app, !Zlength_cons, !Zlength_nil; entailer!.
       rewrite !sepcon_assoc; apply sepcon_derives.
       * apply derives_refl'; f_equal.
-        erewrite upd_Znth_eq, !map_length, upto_length, !map_map;
+        erewrite upd_Znth_eq, !length_map, upto_length, !map_map;
           [|rewrite !Zlength_map, Zlength_upto; unfold N in *; auto].
         apply map_ext_in; intros; rewrite In_upto in *.
         replace (Zlength t') with (Zlength h').

mailbox/verif_mailbox_write.v

@@ -84,7 +84,7 @@ Proof.
       entailer!.
       rewrite upd_Znth_eq; [|auto].
       apply derives_refl'; erewrite map_ext_in; [reflexivity|].
-      intros; rewrite In_upto, map_length, upto_length in *; simpl in *.
+      intros; rewrite In_upto, length_map, upto_length in *; simpl in *.
       erewrite Znth_map, Znth_upto; simpl; auto; try lia.
       erewrite sublist_split with (mid := i)(hi := i + 1), sublist_len_1; auto; try lia.
       destruct (in_dec eq_dec a (sublist 0 i lasts ++ [Znth i lasts])); rewrite in_app in *.
@@ -996,7 +996,7 @@ Proof.
       cancel.
       rewrite !sepcon_assoc; apply sepcon_derives.
       * apply derives_refl'; f_equal.
-        erewrite upd_Znth_eq, !map_length, upto_length, !map_map;
+        erewrite upd_Znth_eq, !length_map, upto_length, !map_map;
           [|rewrite !Zlength_map, Zlength_upto; unfold N in *; auto].
         apply map_ext_in; intros; rewrite In_upto in *.
         replace (Zlength t') with (Zlength h').

mc_reify/verif_sha_bdo7.v

@@ -250,7 +250,7 @@ assert (H1: firstn 1 (skipn (16 - S n) b) =
             W (nthi b) (16 - 16 + (Z.of_nat (16 - S n) - 16) mod 16) :: nil). {
  unfold firstn.
  destruct (skipn (16 - S n) b) eqn:?.
- pose proof (skipn_length b (16 - S n)).
+ pose proof (length_skipn b (16 - S n)).
  rewrite Heql in H1.
  simpl length in H1.
  omega.

progs/conc_queue_specs.v

@@ -480,7 +480,7 @@ Proof.
     - split; [rewrite Zlength_correct; lia|]; transitivity MAX; try lia; unfold MAX; computable.
     - split; [rewrite Zlength_correct; lia|]; transitivity MAX; try lia; unfold MAX; computable. }
   assert (map fst vals1 = map fst vals2) as Heq.
-  { eapply complete_inj; [|rewrite !map_length; auto].
+  { eapply complete_inj; [|rewrite !length_map; auto].
     eapply rotate_inj; eauto; try lia.
     repeat rewrite length_complete; try rewrite Zlength_map; auto.
     rewrite Zlength_complete; try rewrite Zlength_map; lia. }

progs/dry_mem_lemmas.v

@@ -749,7 +749,7 @@ Lemma encode_vals_length : forall lv,
   length (concat (map (encode_val Mint8unsigned) lv)) = length lv.
 Proof.
   induction lv; auto; simpl.
-  rewrite app_length, IHlv.
+  rewrite length_app, IHlv.
   unfold encode_val; simpl.
   destruct a; auto.
 Qed.

progs/io_mem_dry.v

@@ -20,7 +20,7 @@ Proof.
   intros.
   rewrite !Zlength_correct; f_equal.
   unfold bytes_to_memvals.
-  rewrite <- map_map, encode_vals_length, map_length; auto.
+  rewrite <- map_map, encode_vals_length, length_map; auto.
 Qed.
 
 Context {E : Type -> Type} {IO_E : @IO_event nat -< E}.