diff --git a/Makefile b/Makefile index 27b8bfdbd..08051f382 100644 --- a/Makefile +++ b/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) diff --git a/aes/list_utils.v b/aes/list_utils.v index 5270bf5a7..ad4246fd7 100644 --- a/aes/list_utils.v +++ b/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. diff --git a/concurrency/ghosts.v b/concurrency/ghosts.v index 5152e2e17..b3631aa89 100644 --- a/concurrency/ghosts.v +++ b/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. diff --git a/concurrency/memory_lemmas.v b/concurrency/memory_lemmas.v index 881ab3e3d..7055ab961 100644 --- a/concurrency/memory_lemmas.v +++ b/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. diff --git a/floyd/Clightnotations.v b/floyd/Clightnotations.v index 97a116240..d829c665e 100644 --- a/floyd/Clightnotations.v +++ b/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. diff --git a/floyd/Component.v b/floyd/Component.v index 62e3426d3..5c52e6824 100644 --- a/floyd/Component.v +++ b/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 diff --git a/floyd/base2.v b/floyd/base2.v index f084bd3c3..73f6aa329 100644 --- a/floyd/base2.v +++ b/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 diff --git a/floyd/canon.v b/floyd/canon.v index c62eaab59..316680910 100644 --- a/floyd/canon.v +++ b/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. diff --git a/floyd/data_at_lemmas.v b/floyd/data_at_lemmas.v index 72e2a323b..65cac47cf 100644 --- a/floyd/data_at_lemmas.v +++ b/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. diff --git a/floyd/finish.v b/floyd/finish.v index 6f0816ee0..f16ea609a 100644 --- a/floyd/finish.v +++ b/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 := [ diff --git a/floyd/forward.v b/floyd/forward.v index b065e5aaf..ff6c8017d 100644 --- a/floyd/forward.v +++ b/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 *) diff --git a/floyd/globals_lemmas.v b/floyd/globals_lemmas.v index 0be6220db..7335e15f7 100644 --- a/floyd/globals_lemmas.v +++ b/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. diff --git a/floyd/proofauto.v b/floyd/proofauto.v index 7a8e9a418..af20a97b1 100644 --- a/floyd/proofauto.v +++ b/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. diff --git a/floyd/subsume_funspec.v b/floyd/subsume_funspec.v index f04d7557a..3adcb8531 100644 --- a/floyd/subsume_funspec.v +++ b/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. diff --git a/hmacdrbg/HMAC_DRBG_nonadaptive.v b/hmacdrbg/HMAC_DRBG_nonadaptive.v index 097c2081d..7c12fd23c 100644 --- a/hmacdrbg/HMAC_DRBG_nonadaptive.v +++ b/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. *) diff --git a/hmacdrbg/HMAC_DRBG_pure_lemmas.v b/hmacdrbg/HMAC_DRBG_pure_lemmas.v index 2f67e739d..a2a3b71ae 100644 --- a/hmacdrbg/HMAC_DRBG_pure_lemmas.v +++ b/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. diff --git a/hmacdrbg/entropy_lemmas.v b/hmacdrbg/entropy_lemmas.v index 12fd27b98..f5259bd09 100644 --- a/hmacdrbg/entropy_lemmas.v +++ b/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. diff --git a/mailbox/verif_mailbox_bad_write.v b/mailbox/verif_mailbox_bad_write.v index fa8335af4..49139f8c7 100644 --- a/mailbox/verif_mailbox_bad_write.v +++ b/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'). diff --git a/mailbox/verif_mailbox_write.v b/mailbox/verif_mailbox_write.v index 50a5a2ebb..896d179c3 100644 --- a/mailbox/verif_mailbox_write.v +++ b/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'). diff --git a/mc_reify/verif_sha_bdo7.v b/mc_reify/verif_sha_bdo7.v index e0ddf9200..c15b2fb14 100644 --- a/mc_reify/verif_sha_bdo7.v +++ b/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. diff --git a/progs/conc_queue_specs.v b/progs/conc_queue_specs.v index 495ad255c..93804a91b 100644 --- a/progs/conc_queue_specs.v +++ b/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. } diff --git a/progs/dry_mem_lemmas.v b/progs/dry_mem_lemmas.v index 5400ca7c5..29d969585 100644 --- a/progs/dry_mem_lemmas.v +++ b/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. diff --git a/progs/io_mem_dry.v b/progs/io_mem_dry.v index c07294c4f..5999e4409 100644 --- a/progs/io_mem_dry.v +++ b/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}. diff --git a/progs/io_os_connection.v b/progs/io_os_connection.v index d0f12be9a..8038159e5 100644 --- a/progs/io_os_connection.v +++ b/progs/io_os_connection.v @@ -585,7 +585,7 @@ Section Invariants. intros * Heq. enough (n = nth (length pre) (seq start len) O); subst. { rewrite Heq, app_nth2, Nat.sub_diag, seq_nth; auto; cbn. - rewrite <- (seq_length len start), Heq, app_length; cbn; lia. + rewrite <- (seq_length len start), Heq, length_app; cbn; lia. } rewrite Heq, app_nth2, Nat.sub_diag; auto. Qed. @@ -597,7 +597,7 @@ Section Invariants. unfold enumerate; intros * Heq. apply (f_equal (map fst)) in Heq. rewrite combine_fst, map_app in Heq; cbn in Heq. - apply seq_nth_app in Heq; subst; cbn; auto using map_length. + apply seq_nth_app in Heq; subst; cbn; auto using length_map. rewrite <- Nat2Z.id, <- Zlength_length; rewrite <- Zlength_correct. - rewrite !Zlength_correct, seq_length; auto. - apply Zlength_nonneg. @@ -625,7 +625,7 @@ Section Invariants. destruct ev; cbn; f_equal; auto. } rewrite Henum in Heq. - apply enumerate_length in Heq; subst; auto using map_length. + apply enumerate_length in Heq; subst; auto using length_map. Qed. Corollary mkRecvEvents_ordered : forall cs logIdx strIdx c strIdx' c' pre mid post, @@ -636,7 +636,7 @@ Section Invariants. pose proof Heq as Heq'. rewrite app_comm_cons, app_assoc in Heq'. apply mkRecvEvents_strIdx in Heq; apply mkRecvEvents_strIdx in Heq'; subst. - rewrite app_length; cbn; lia. + rewrite length_app; cbn; lia. Qed. Lemma mkRecvEvents_cons : forall cs c logIdx, @@ -1443,10 +1443,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. rewrite Htr; destruct Htr' as [(? & ->) | ?]; subst; auto. Qed. @@ -1461,10 +1461,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. rewrite Htr'; destruct Htr as [(? & ->) | (? & ->)]; subst; auto; constructor. Qed. @@ -1487,10 +1487,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. pose proof (Z.mod_pos_bound c 256 ltac:(lia)). rewrite Htr; destruct Htr' as [(? & ->) | ?]; subst; auto. @@ -1506,10 +1506,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. pose proof (Z.mod_pos_bound c 256 ltac:(lia)). rewrite Htr'; destruct Htr as [(? & ->) | (? & ->)]; subst; auto. @@ -1522,11 +1522,11 @@ Section Invariants. unfold cons_intr_aux, nil_trace_case; intros * Hspec; destruct_spec Hspec. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; cbn in *. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto using mkRecvEvents_not_visible. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; cbn in *. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto using mkRecvEvents_not_visible. Qed. @@ -1566,9 +1566,9 @@ Section Invariants. destruct Heq; subst; red. rewrite <- Htr; unfold strip_common_prefix. rewrite common_prefix_app, <- app_assoc, common_prefix_app. - rewrite !app_length, !leb_correct by (cbn; lia). + rewrite !length_app, !leb_correct by (cbn; lia). rewrite skipn_app1, skipn_exact_length; auto. - rewrite (app_assoc io_log), <- app_length. + rewrite (app_assoc io_log), <- length_app. rewrite skipn_app1, skipn_exact_length; cbn; auto. - prename cons_intr_aux into Hspec'. eapply cons_intr_aux_trace_case in Hspec'. @@ -1583,9 +1583,9 @@ Section Invariants. destruct Heq; subst; red. rewrite <- Htr; unfold strip_common_prefix. rewrite common_prefix_app, <- app_assoc, common_prefix_app. - rewrite !app_length, !leb_correct by (cbn; lia). + rewrite !length_app, !leb_correct by (cbn; lia). rewrite skipn_app1, skipn_exact_length; auto. - rewrite (app_assoc io_log), <- app_length. + rewrite (app_assoc io_log), <- length_app. rewrite skipn_app1, skipn_exact_length; cbn; auto. Qed. @@ -1639,12 +1639,12 @@ Section Invariants. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; red. unfold strip_common_prefix. - rewrite !app_length, leb_correct by lia. + rewrite !length_app, leb_correct by lia. rewrite common_prefix_app, skipn_app1, skipn_exact_length; auto. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; red. unfold strip_common_prefix. - rewrite !app_length, leb_correct by lia. + rewrite !length_app, leb_correct by lia. rewrite common_prefix_app, skipn_app1, skipn_exact_length; auto. Qed. @@ -1658,7 +1658,7 @@ Section Invariants. prename (cons_buf _ = _) into Hcons. destruct st; cbn in *; unfold getc_trace_case. unfold strip_common_prefix. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto. Coqlib.inv Hvalid; cbn in *. rewrite vt_trace_console0 in Hcons. diff --git a/progs/mmap_dry.v b/progs/mmap_dry.v index 16cec882a..eaf94ffd9 100644 --- a/progs/mmap_dry.v +++ b/progs/mmap_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. Definition mmap_pre (m : mem) (len : Z) := 0 <= len <= Ptrofs.max_unsigned. diff --git a/progs/verif_btree.v b/progs/verif_btree.v index 249d9fe77..98c8a85a4 100644 --- a/progs/verif_btree.v +++ b/progs/verif_btree.v @@ -303,8 +303,8 @@ Section BTree. length (replace i x l) = length l. Proof. intros; unfold replace. - rewrite app_length; simpl. - rewrite firstn_length, skipn_length. + rewrite length_app; simpl. + rewrite length_firstn, length_skipn. rewrite Min.min_l; lia. Qed. @@ -351,7 +351,7 @@ Section BTree. Proof. intros; unfold replace. assert (length (firstn i l) = i) as Hlen. - { rewrite firstn_length, Min.min_l; auto. } + { rewrite length_firstn, Min.min_l; auto. } rewrite nth_error_app2; rewrite Hlen; auto. rewrite minus_diag; auto. Qed. @@ -463,7 +463,7 @@ Section BTree. rewrite Hchildren; split; auto. apply Forall_insert. + apply Forall_replace'; auto; simpl. - repeat rewrite skipn_length. + repeat rewrite length_skipn. destruct Hover as (Hover & Hwf); rewrite Hover. rewrite NPeano.Nat.add_1_r, odd_div; simpl. split; try lia. @@ -473,13 +473,13 @@ Section BTree. rewrite (alt_Forall wf_btree_aux). apply Forall_skipn; auto. + unfold wf_btree_aux; fold wf_btree_aux. - rewrite firstn_length, Min.min_l; [|apply Nat.div_le_upper_bound; lia]. + rewrite length_firstn, Min.min_l; [|apply Nat.div_le_upper_bound; lia]. unfold wf_btree_over in Hover. destruct Hover as (Hover & Hwf); rewrite Hover. rewrite NPeano.Nat.add_1_r, odd_div; simpl. split; [lia|]. destruct Hwf as [|(Hlen & ?)]; [subst; rewrite firstn_nil; auto | right]. - rewrite firstn_length, Hlen, Hover, Min.min_l; [|lia]. + rewrite length_firstn, Hlen, Hover, Min.min_l; [|lia]. split; auto. rewrite (alt_Forall wf_btree_aux). apply Forall_firstn; auto. @@ -502,7 +502,7 @@ Section BTree. rewrite Hchildren; split; auto. apply Forall_insert. + apply Forall_replace'; auto; simpl. - repeat rewrite skipn_length. + repeat rewrite length_skipn. destruct Hover as (Hover & Hwf); rewrite Hover. rewrite NPeano.Nat.add_1_r, odd_div; simpl. split; try lia. @@ -512,13 +512,13 @@ Section BTree. rewrite (alt_Forall wf_btree_aux). apply Forall_skipn; auto. + unfold wf_btree_aux; fold wf_btree_aux. - rewrite firstn_length, Min.min_l; [|apply Nat.div_le_upper_bound; lia]. + rewrite length_firstn, Min.min_l; [|apply Nat.div_le_upper_bound; lia]. unfold wf_btree_over in Hover. destruct Hover as (Hover & Hwf); rewrite Hover. rewrite NPeano.Nat.add_1_r, odd_div; simpl. split; [lia|]. destruct Hwf as [|(Hlen & ?)]; [subst; rewrite firstn_nil; auto | right]. - rewrite firstn_length, Hlen, Hover, Min.min_l; [|lia]. + rewrite length_firstn, Hlen, Hover, Min.min_l; [|lia]. split; auto. rewrite (alt_Forall wf_btree_aux). apply Forall_firstn; auto. @@ -537,7 +537,7 @@ Section BTree. remove_at i (replace i x l) = remove_at i l. Proof. intros; unfold remove_at, replace. - assert (length (firstn i l) = i) as Hlen by (rewrite firstn_length, Min.min_l; auto). + assert (length (firstn i l) = i) as Hlen by (rewrite length_firstn, Min.min_l; auto). rewrite firstn_app1, firstn_firstn, skipn_app2; auto; rewrite Hlen; auto. rewrite <- minus_Sn_m, minus_diag; auto. Qed. @@ -795,11 +795,11 @@ Section BTree. destruct H as (Hover & Hwf'); rewrite Hover. rewrite (Nat.add_1_r (2 * d)), odd_div. unfold replace; simpl; constructor; [|constructor; auto]; simpl. - + rewrite firstn_length, Min.min_l; [split|]; try lia. + + rewrite length_firstn, Min.min_l; [split|]; try lia. destruct Hwf' as [|(? & ?)]; subst; auto; right. - rewrite firstn_length, Min.min_l; [split; auto | lia]. + rewrite length_firstn, Min.min_l; [split; auto | lia]. rewrite (alt_Forall wf_btree_aux); apply Forall_firstn; auto. - + repeat rewrite skipn_length; split; [lia|]. + + repeat rewrite length_skipn; split; [lia|]. destruct Hwf' as [|(? & ?)]; subst; auto; right. split; [lia|]. rewrite (alt_Forall wf_btree_aux); apply Forall_skipn; auto. diff --git a/progs/verif_cond_queue.v b/progs/verif_cond_queue.v index 1fdbc6a0f..3e553c3c6 100644 --- a/progs/verif_cond_queue.v +++ b/progs/verif_cond_queue.v @@ -200,7 +200,7 @@ Proof. { rewrite Z.add_simpl_r; split; auto; rewrite Zlength_correct; lia. } assert (Znth (Zlength reqs + 1 - 1) (complete MAX (reqs ++ [req])) Vundef = req) as Hnth. { rewrite Z.add_simpl_r, Znth_complete; - [|repeat rewrite Zlength_correct; rewrite app_length; simpl; Omega0]. + [|repeat rewrite Zlength_correct; rewrite length_app; simpl; Omega0]. rewrite app_Znth2, Zminus_diag; [auto | lia]. } forward. { entailer!. @@ -357,7 +357,7 @@ Proof. { simpl. Exists (reqs0 ++ [r]); cancel. unfold fold_right at 2; unfold fold_right at 1; cancel. - repeat rewrite Zlength_correct; rewrite app_length; simpl. + repeat rewrite Zlength_correct; rewrite length_app; simpl. rewrite Nat2Z.inj_add. repeat rewrite map_app; simpl; rewrite sepcon_app; simpl. unfold fold_right at 1; cancel; entailer'. @@ -411,7 +411,7 @@ Proof. - assert (reqs0 <> []) as Hreqs. { intro; subst; unfold Zlength in *; simpl in *; contradiction HRE; auto. } rewrite (app_removelast_last (Vint (Int.repr 0)) Hreqs) in *. - rewrite Zlength_correct, app_length; simpl. + rewrite Zlength_correct, length_app; simpl. rewrite Nat2Z.inj_add, <- Zlength_correct; simpl. rewrite Zlength_app, Zlength_cons, Zlength_nil in *; simpl in *. match goal with H : Forall isptr (_ ++ _) |- _ => diff --git a/progs/verif_queue_ex.v b/progs/verif_queue_ex.v index 2b0d5edae..958ae50d6 100644 --- a/progs/verif_queue_ex.v +++ b/progs/verif_queue_ex.v @@ -698,14 +698,14 @@ Proof. lqueue Tsh tint (is_int I32 Signed) q lock sh1 sh2 h'). { assert (length lshs1 = length (map (fun vals => map (fun x => let '(p, i) := x in QRem p (Vint i)) vals) (rev vals))). - { rewrite !map_length, rev_length; rewrite Zlength_correct in *; abstract lia. } + { rewrite !length_map, length_rev; rewrite Zlength_correct in *; abstract lia. } go_lowerx; eapply derives_trans; [|apply lqueue_shares_join; [eauto | rewrite Hlenl1; eauto]]. subst lsh'; cancel. rewrite combine_map_snd, map_map. rewrite <- sepcon_rev, <- map_rev, rev_combine, rev_involutive. erewrite map_ext; [apply derives_refl|]. destruct a; auto. - { rewrite rev_length, map_length, rev_length in *; auto. } } + { rewrite length_rev, length_map, length_rev in *; auto. } } Intros h'. repeat (destruct ptrs; [rewrite Zlength_nil in *; discriminate | rewrite Zlength_cons in *]). destruct ptrs; [|rewrite Zlength_cons, Zlength_correct in *; lia]. diff --git a/progs64/dry_mem_lemmas.v b/progs64/dry_mem_lemmas.v index 1e7219d92..64828e8ea 100644 --- a/progs64/dry_mem_lemmas.v +++ b/progs64/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. diff --git a/progs64/io_mem_dry.v b/progs64/io_mem_dry.v index 74e53eaab..8d842af99 100644 --- a/progs64/io_mem_dry.v +++ b/progs64/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}. diff --git a/progs64/io_os_connection.v b/progs64/io_os_connection.v index a2f557da1..d059dcbe0 100644 --- a/progs64/io_os_connection.v +++ b/progs64/io_os_connection.v @@ -587,7 +587,7 @@ Section Invariants. intros * Heq. enough (n = nth (length pre) (seq start len) O); subst. { rewrite Heq, app_nth2, Nat.sub_diag, seq_nth; auto; cbn. - rewrite <- (seq_length len start), Heq, app_length; cbn; lia. + rewrite <- (seq_length len start), Heq, length_app; cbn; lia. } rewrite Heq, app_nth2, Nat.sub_diag; auto. Qed. @@ -599,7 +599,7 @@ Section Invariants. unfold enumerate; intros * Heq. apply (f_equal (map fst)) in Heq. rewrite combine_fst, map_app in Heq; cbn in Heq. - apply seq_nth_app in Heq; subst; cbn; auto using map_length. + apply seq_nth_app in Heq; subst; cbn; auto using length_map. rewrite <- Nat2Z.id, <- Zlength_length; rewrite <- Zlength_correct. - rewrite !Zlength_correct, seq_length; auto. - apply Zlength_nonneg. @@ -627,7 +627,7 @@ Section Invariants. destruct ev; cbn; f_equal; auto. } rewrite Henum in Heq. - apply enumerate_length in Heq; subst; auto using map_length. + apply enumerate_length in Heq; subst; auto using length_map. Qed. Corollary mkRecvEvents_ordered : forall cs logIdx strIdx c strIdx' c' pre mid post, @@ -638,7 +638,7 @@ Section Invariants. pose proof Heq as Heq'. rewrite app_comm_cons, app_assoc in Heq'. apply mkRecvEvents_strIdx in Heq; apply mkRecvEvents_strIdx in Heq'; subst. - rewrite app_length; cbn; lia. + rewrite length_app; cbn; lia. Qed. Lemma mkRecvEvents_cons : forall cs c logIdx, @@ -1445,10 +1445,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. rewrite Htr; destruct Htr' as [(? & ->) | ?]; subst; auto. Qed. @@ -1463,10 +1463,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. rewrite Htr'; destruct Htr as [(? & ->) | (? & ->)]; subst; auto; constructor. Qed. @@ -1489,10 +1489,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. pose proof (Z.mod_pos_bound c 256 ltac:(lia)). rewrite Htr; destruct Htr' as [(? & ->) | ?]; subst; auto. @@ -1508,10 +1508,10 @@ Section Invariants. apply common_prefix_correct in Heq; apply common_prefix_correct in Heq'. destruct Heq, Heq'; subst. unfold strip_common_prefix in *. - rewrite !app_length, leb_correct in * by lia. + rewrite !length_app, leb_correct in * by lia. rewrite <- app_assoc. rewrite common_prefix_app, skipn_app1, skipn_exact_length in *; - rewrite ?app_length; auto; cbn in *. + rewrite ?length_app; auto; cbn in *. rewrite trace_of_ostrace_app. pose proof (Z.mod_pos_bound c 256 ltac:(lia)). rewrite Htr'; destruct Htr as [(? & ->) | (? & ->)]; subst; auto. @@ -1524,11 +1524,11 @@ Section Invariants. unfold cons_intr_aux, nil_trace_case; intros * Hspec; destruct_spec Hspec. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; cbn in *. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto using mkRecvEvents_not_visible. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; cbn in *. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto using mkRecvEvents_not_visible. Qed. @@ -1568,9 +1568,9 @@ Section Invariants. destruct Heq; subst; red. rewrite <- Htr; unfold strip_common_prefix. rewrite common_prefix_app, <- app_assoc, common_prefix_app. - rewrite !app_length, !leb_correct by (cbn; lia). + rewrite !length_app, !leb_correct by (cbn; lia). rewrite skipn_app1, skipn_exact_length; auto. - rewrite (app_assoc io_log), <- app_length. + rewrite (app_assoc io_log), <- length_app. rewrite skipn_app1, skipn_exact_length; cbn; auto. - prename cons_intr_aux into Hspec'. eapply cons_intr_aux_trace_case in Hspec'. @@ -1585,9 +1585,9 @@ Section Invariants. destruct Heq; subst; red. rewrite <- Htr; unfold strip_common_prefix. rewrite common_prefix_app, <- app_assoc, common_prefix_app. - rewrite !app_length, !leb_correct by (cbn; lia). + rewrite !length_app, !leb_correct by (cbn; lia). rewrite skipn_app1, skipn_exact_length; auto. - rewrite (app_assoc io_log), <- app_length. + rewrite (app_assoc io_log), <- length_app. rewrite skipn_app1, skipn_exact_length; cbn; auto. Qed. @@ -1641,12 +1641,12 @@ Section Invariants. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; red. unfold strip_common_prefix. - rewrite !app_length, leb_correct by lia. + rewrite !length_app, leb_correct by lia. rewrite common_prefix_app, skipn_app1, skipn_exact_length; auto. - prename (Coqlib.zeq _ _ = _) into Htmp; clear Htmp. destruct st; cbn in *; subst; red. unfold strip_common_prefix. - rewrite !app_length, leb_correct by lia. + rewrite !length_app, leb_correct by lia. rewrite common_prefix_app, skipn_app1, skipn_exact_length; auto. Qed. @@ -1660,7 +1660,7 @@ Section Invariants. prename (cons_buf _ = _) into Hcons. destruct st; cbn in *; unfold getc_trace_case. unfold strip_common_prefix. - rewrite common_prefix_app, app_length, leb_correct by lia. + rewrite common_prefix_app, length_app, leb_correct by lia. rewrite skipn_app1, skipn_exact_length; cbn; auto. Coqlib.inv Hvalid; cbn in *. rewrite vt_trace_console0 in Hcons. diff --git a/sha/ByteBitRelations.v b/sha/ByteBitRelations.v index fcc65a3d9..fa77fc862 100644 --- a/sha/ByteBitRelations.v +++ b/sha/ByteBitRelations.v @@ -296,9 +296,9 @@ Proof. intros n len. rewrite -> H0. rewrite -> bitsToBytes_app. - rewrite -> app_length. + rewrite -> length_app. rewrite -> H0 in len. - rewrite -> app_length in len. + rewrite -> length_app in len. rewrite -> H in len. destruct n as [ | n']. diff --git a/sha/HMAC256_equivalence.v b/sha/HMAC256_equivalence.v index f80ca90a0..5c1dd446c 100644 --- a/sha/HMAC256_equivalence.v +++ b/sha/HMAC256_equivalence.v @@ -69,7 +69,7 @@ Definition ipad_v: Bvector b := of_list_length _ ipad_length. *) Lemma fpad_length (v:Bvector c): length (fpad (Vector.to_list v)) = p. Proof. unfold fpad, fpad_inner. rewrite bytesToBits_len. - repeat rewrite app_length. rewrite repeat_length, length_intlist_to_bytelist. + repeat rewrite length_app. rewrite repeat_length, length_intlist_to_bytelist. rewrite (Nat.mul_comm 4), Nat.add_comm, Zlength_correct. rewrite bitsToBytes_len_gen with (n:=32%nat). reflexivity. @@ -118,7 +118,7 @@ Proof. remember ( Compare_dec.leb (length (b :: ssm)) 511) as d. destruct d. exfalso. rewrite Heql in pf. apply Forall_inv in pf. clear Heql. - rewrite firstn_length in pf. + rewrite length_firstn in pf. symmetry in Heqd. apply leb_complete in Heqd. eapply Nat.min_l_iff in pf. lia. rewrite splitAndPad_aux_consD. @@ -319,7 +319,7 @@ SearchAbout sha_splitandpad_inc. split; lia. (* key length *) - { rewrite map_length, bitsToBytes_len_gen with (n:=64%nat). + { rewrite length_map, bitsToBytes_len_gen with (n:=64%nat). reflexivity. rewrite LK; reflexivity. } diff --git a/sha/HMAC256_spec_list.v b/sha/HMAC256_spec_list.v index 569f428aa..0ef44f1ca 100644 --- a/sha/HMAC256_spec_list.v +++ b/sha/HMAC256_spec_list.v @@ -29,7 +29,7 @@ Function toBlocks (l : Blist) {measure length l} : list Blist := Proof. intros. subst. remember ((b :: l0)%list) as l. clear Heql. apply leb_complete_conv in teq0. - rewrite skipn_length; lia. + rewrite length_skipn; lia. Qed. Lemma toBlocks_injective: forall l1 l2 (BLKS: toBlocks l1 = toBlocks l2) @@ -50,7 +50,7 @@ Proof. destruct l1; try discriminate. destruct l2; try discriminate. inversion F1; clear F1. rewrite H0 in Heql. assert (L1: (511 < length (front ++ back))%nat). - rewrite app_length, H. lia. + rewrite length_app, H. lia. rewrite leb_correct_conv in Heql; trivial. rewrite firstn_exact in Heql; trivial. rewrite skipn_exact in Heql; trivial. @@ -58,7 +58,7 @@ Proof. inversion F2; clear F2. rewrite H4 in BLKS. assert (L2: (511 < length (front0 ++ back0))%nat). - rewrite app_length, H3. lia. + rewrite length_app, H3. lia. rewrite leb_correct_conv in BLKS; trivial. rewrite firstn_exact in BLKS; trivial. rewrite skipn_exact in BLKS; trivial. @@ -80,7 +80,7 @@ Proof. intros. induction l. simpl; intros. constructor. simpl; intros. rewrite toBlocks_equation in Heql. destruct b. discriminate. inversion H; clear H. - rewrite H1, app_length, H0 in Heql. + rewrite H1, length_app, H0 in Heql. rewrite leb_correct_conv in Heql. 2: lia. rewrite firstn_exact in Heql; trivial. rewrite skipn_exact in Heql; trivial. inversion Heql; clear Heql. @@ -104,8 +104,8 @@ Proof. rewrite -> toBlocks_equation. destruct full. assert (@length bool nil = length (front ++ back)). rewrite <- H0; reflexivity. - rewrite app_length, H in H1. remember (length back). clear - H1. rewrite Nat.add_comm in H1. simpl in H1. lia. - rewrite H0, app_length, H, leb_correct_conv. 2: lia. + rewrite length_app, H in H1. remember (length back). clear - H1. rewrite Nat.add_comm in H1. simpl in H1. lia. + rewrite H0, length_app, H, leb_correct_conv. 2: lia. rewrite -> firstn_exact; trivial. rewrite -> skipn_exact; trivial. (*rewrite -> length_not_emp.*) @@ -156,7 +156,7 @@ Proof. apply len_l. apply in_cons. apply H. - - rewrite -> app_length. + - rewrite -> length_app. assert (length l = 512%nat). apply len_l. unfold In. auto. rewrite -> H. specialize (len_min ls). @@ -179,7 +179,7 @@ Proof. rewrite -> length_not_emp. apply fold_ind. * apply len_ls. - * rewrite -> app_length. + * rewrite -> length_app. rewrite len_l. specialize (len_min ls). lia. @@ -228,13 +228,13 @@ Qed.*) Lemma toBlocks_app_split l1 l2: length l1 = 512%nat -> toBlocks (l1 ++ l2) = toBlocks l1 ++ toBlocks l2. Proof. intros. - rewrite toBlocks_equation. rewrite app_length. + rewrite toBlocks_equation. rewrite length_app. rewrite firstn_exact; trivial. rewrite skipn_exact; trivial. remember (l1 ++ l2). destruct l. { assert (@length bool nil = length (l1 ++ l2)). rewrite <- Heql; trivial. - rewrite app_length, H in H0. rewrite Nat.add_comm in H0. simpl in H0. lia. } + rewrite length_app, H in H0. rewrite Nat.add_comm in H0. simpl in H0. lia. } { rewrite leb_correct_conv. 2: rewrite H, Nat.add_comm; lia. remember (toBlocks l2). rewrite toBlocks_equation. diff --git a/sha/HMAC256_spec_pad.v b/sha/HMAC256_spec_pad.v index 9244df536..1e22a82fc 100644 --- a/sha/HMAC256_spec_pad.v +++ b/sha/HMAC256_spec_pad.v @@ -194,11 +194,11 @@ Proof. - apply xor_equiv_byte; trivial. - assumption. } { apply BLxor_length; erewrite bytes_bits_length; try eassumption. - rewrite map_length, padded_key_len. reflexivity. + rewrite length_map, padded_key_len. reflexivity. unfold HP.HMAC_SHA256.sixtyfour. rewrite -> repeat_length. reflexivity. } { apply BLxor_length; erewrite bytes_bits_length; try eassumption. - rewrite map_length, padded_key_len. reflexivity. + rewrite length_map, padded_key_len. reflexivity. unfold HP.HMAC_SHA256.sixtyfour. rewrite -> repeat_length. reflexivity. } Qed. diff --git a/sha/HMAC_common_defs.v b/sha/HMAC_common_defs.v index f9886863a..fa1e23aa9 100644 --- a/sha/HMAC_common_defs.v +++ b/sha/HMAC_common_defs.v @@ -15,7 +15,7 @@ Definition concat {A : Type} (l : list (list A)) : list A := Lemma concat_length {A}: forall L (l:list A), In l L -> (length (concat L) >= length l)%nat. Proof. unfold concat. induction L; simpl; intros. contradiction. - rewrite app_length. + rewrite length_app. destruct H; subst. unfold id. lia. specialize (IHL _ H). lia. Qed. @@ -62,7 +62,7 @@ Proof. subst. reflexivity. - destruct l1; destruct l2; inversion len1; inversion len2. simpl. - rewrite -> map_length. + rewrite -> length_map. rewrite -> combine_length. rewrite H0. rewrite H1. simpl. f_equal. @@ -109,13 +109,13 @@ Function hash_blocks_bits (b:nat) (B:(0 Blist Proof. intros. destruct (lt_dec (length msg) b). rewrite skipn_short. simpl; lia. rewrite <- teq; lia. - rewrite skipn_length; rewrite <- teq; lia. + rewrite length_skipn; rewrite <- teq; lia. Defined. Lemma add_blocksize_length l n: 0<=n -> BinInt.Z.add n (Zcomplements.Zlength l) = Zcomplements.Zlength ((repeat true (Z.to_nat n)) ++ l). Proof. intros. do 2 rewrite Zlength_correct. - rewrite app_length, repeat_length, Nat2Z.inj_add, Z2Nat.id; trivial. + rewrite length_app, repeat_length, Nat2Z.inj_add, Z2Nat.id; trivial. Qed. Lemma hash_blocks_bits_len c b (B:(0 H0 in inputs_eq. rewrite -> H2 in inputs_eq. apply (front_equiv DB32 back0 back front0 front H1 H inputs_eq). } - + rewrite -> H0. rewrite -> app_length. rewrite -> H. lia. - + rewrite -> H2. rewrite -> app_length. rewrite -> H1. lia. + + rewrite -> H0. rewrite -> length_app. rewrite -> H. lia. + + rewrite -> H2. rewrite -> length_app. rewrite -> H1. lia. Qed. Lemma equiv_pad shaiv shasplitandpad c p (B: (0< b c p)%nat) (DB32: (I.d*32 =b c p)%nat) diff --git a/sha/SHA256.v b/sha/SHA256.v index 624428824..e4657c5a7 100644 --- a/sha/SHA256.v +++ b/sha/SHA256.v @@ -138,9 +138,9 @@ Function hash_blocks (r: registers) (msg: list int) {measure length msg} : regis end. Proof. intros. destruct (lt_dec (length msg) 16). - rewrite skipn_length_short. simpl; lia. subst; simpl in *; lia. + rewrite length_skipn_short. simpl; lia. subst; simpl in *; lia. rewrite <- teq; auto. - rewrite skipn_length. simpl; lia. + rewrite length_skipn. simpl; lia. Qed. Definition SHA_256 (str : list byte) : list byte := diff --git a/sha/ShaInstantiation.v b/sha/ShaInstantiation.v index ea34e12af..1c547639f 100644 --- a/sha/ShaInstantiation.v +++ b/sha/ShaInstantiation.v @@ -42,7 +42,7 @@ Definition fpad_inner (msg : list byte) : list byte := Lemma fpad_inner_length l (L:length l = p): (length (fpad_inner (bitsToBytes l)) * 8)%nat = p. Proof. - unfold fpad_inner. repeat rewrite app_length. + unfold fpad_inner. repeat rewrite length_app. rewrite repeat_length, length_intlist_to_bytelist. rewrite (Nat.mul_comm 4), Nat.add_comm, Zlength_correct. rewrite bitsToBytes_len_gen with (n:=32%nat). @@ -94,7 +94,7 @@ Lemma pad_inc_length: forall l, exists k, (0 < k /\ length (pad_inc l) = k*64)%n Proof. unfold pad_inc. induction l. simpl. exists (1%nat). lia. - destruct IHl as [k [K HK]]. repeat rewrite app_length in *. rewrite repeat_length in *. + destruct IHl as [k [K HK]]. repeat rewrite length_app in *. rewrite repeat_length in *. rewrite length_intlist_to_bytelist in *. remember (BinInt.Z.to_nat (BinInt.Z.modulo @@ -275,7 +275,7 @@ Proof. symmetry in H. = length ((l2 ++ Byte.repr 128 :: nil) ++ repeat Byte.zero (Z.to_nat (- (BlockSize + Zlength l2 + 9) mod 64)))). rewrite H0; trivial. - clear H0. repeat rewrite app_length in H. + clear H0. repeat rewrite length_app in H. repeat rewrite repeat_length in H. clear - K n H. rewrite (pad_injective_aux l1 l2 k K n) in H. lia. @@ -344,7 +344,7 @@ destruct d. = length ((l2 ++ Byte.repr 128 :: nil) ++ repeat Byte.zero (Z.to_nat (- (BlockSize + Zlength l2 + 9) mod 64)))). rewrite H0; trivial. - clear H0. repeat rewrite app_length in H1. + clear H0. repeat rewrite length_app in H1. repeat rewrite repeat_length in H1. rewrite (pad_injective_aux l2 l1 (k1-k2)) in H1. lia. @@ -446,7 +446,7 @@ Lemma pad_inc_length: forall l, exists k, (0 < k /\ length (pad_inc l) = k*64)%n Proof. unfold pad_inc. induction l. simpl. exists (1%nat). lia. - destruct IHl as [k [K HK]]. repeat rewrite app_length in *. rewrite repeat_length in *. + destruct IHl as [k [K HK]]. repeat rewrite length_app in *. rewrite repeat_length in *. rewrite pure_lemmas.length_intlist_to_Zlist in *. remember (BinInt.Z.to_nat (BinInt.Z.modulo @@ -608,7 +608,7 @@ Proof. symmetry in H. = length ((l2 ++ 128 :: nil) ++ repeat 0 (Z.to_nat (- (BlockSize + Zlength l2 + 9) mod 64)))). rewrite H0; trivial. - clear H0. repeat rewrite app_length in H. + clear H0. repeat rewrite length_app in H. repeat rewrite repeat_length in H. clear - K n H. rewrite (pad_injective_aux l1 l2 k K n) in H. lia. @@ -677,7 +677,7 @@ destruct d. = length ((l2 ++ 128 :: nil) ++ repeat 0 (Z.to_nat (- (BlockSize + Zlength l2 + 9) mod 64)))). rewrite H0; trivial. - clear H0. repeat rewrite app_length in H1. + clear H0. repeat rewrite length_app in H1. repeat rewrite repeat_length in H1. rewrite (pad_injective_aux l2 l1 (k1-k2)) in H1. lia. diff --git a/sha/functional_prog.v b/sha/functional_prog.v index 1bfd3cbb2..e69fa8cc3 100644 --- a/sha/functional_prog.v +++ b/sha/functional_prog.v @@ -271,7 +271,7 @@ rewrite <- (IHi _ _ H1). reflexivity. rewrite H1. clear H1. -pose proof (firstn_length i b). +pose proof (length_firstn i b). rewrite min_l in H1. 2:{ clear - H0; revert b H0; induction i; destruct b; simpl; intros; inv H0; try lia. @@ -557,7 +557,7 @@ pose proof (roundup_ge (Zlength msg + 9) 64). spec H; [ lia | ]. assert (Zlength msg >= 0) by (rewrite Zlength_correct; lia). exists (Z.to_nat (roundup (Zlength msg+9) 64 / 4 - 2)). -repeat rewrite app_length. +repeat rewrite length_app. rewrite repeat_length. simpl length. symmetry. @@ -633,7 +633,7 @@ rewrite Z2Nat.id by lia. change (Z.of_nat 4) with 4. rewrite Z.mul_comm in H2. assert (length (skipn (Z.to_nat (Zlength msg / 4) * 4) msg) < 4)%nat. -rewrite skipn_length. +rewrite length_skipn. apply Nat2Z.inj_lt. rewrite Nat2Z.inj_sub. rewrite <- Zlength_correct. rewrite Nat2Z.inj_mul. change (Z.of_nat 4) with 4. @@ -661,7 +661,7 @@ assert (- (Zlength msg + 9) mod 64 = (3 - Zlength ccc) + 4* ((Zlength msg+8)/64 * 16 + 15 - (Zlength msg + 8) / 4)). { assert (LL: length ccc = length (skipn (Z.to_nat (Zlength msg / 4) * 4) msg)) by congruence. -rewrite skipn_length in LL. +rewrite length_skipn in LL. assert (LL': Zlength msg = Zlength ccc + (Zlength msg/4)*4). rewrite Zlength_correct at 1. rewrite Zlength_correct at 1. @@ -706,7 +706,7 @@ replace (Zlength msg / 4 * 4) with (Zlength msg - Zlength ccc). 2:{ rewrite Heqccc. rewrite (Zlength_correct (skipn _ _)). -rewrite skipn_length by lia. +rewrite length_skipn by lia. rewrite Nat2Z.inj_sub by lia. rewrite <- Zlength_correct. rewrite Nat2Z.inj_mul. change (Z.of_nat 4) with 4. @@ -790,9 +790,9 @@ lia. } rewrite skipn_app1 by lia. rewrite firstn_app1 - by (rewrite skipn_length by lia; lia). + by (rewrite length_skipn by lia; lia). assert (length (firstn 4 (skipn (Q - 4) msg)) = 4)%nat. -rewrite firstn_length. rewrite skipn_length by lia. +rewrite length_firstn. rewrite length_skipn by lia. apply min_l. lia. destruct (firstn 4 (skipn (Q - 4) msg)) as [ | z0 [| z1 [| z2 [|z3 [|]]]]];inv H3. @@ -886,7 +886,7 @@ extensionality d. rewrite <- (nth_firstn_low _ _ 16). rewrite (generate_word_lemma1 b n H). auto. -rewrite rev_length, length_generate_word, rev_length, H. +rewrite length_rev, length_generate_word, length_rev, H. lia. Qed. @@ -917,7 +917,7 @@ Lemma nth_rev_generate_word: Proof. intros. unfold nthB. -rewrite <- rev_length in H. +rewrite <- length_rev in H. forget (rev b) as b'. clear b. assert (length (generate_word b' 48) = 64)%nat @@ -1076,7 +1076,7 @@ unfold process_block. unfold hash_block. f_equal. rewrite <- (firstn_same _ 64 (rev (generate_word _ _))) - by (rewrite rev_length, length_generate_word, rev_length; lia). + by (rewrite length_rev, length_generate_word, length_rev; lia). change 64%nat with (48+16)%nat. change 63%Z with (Z.of_nat (48+16)-1). assert (48 <= 48)%nat by lia. @@ -1110,7 +1110,7 @@ rewrite (rnd_64_S _ _ _ 2:{ unfold nthi; rewrite Nat2Z.id. rewrite (@coqlib4.nth_error_nth _ _ Int.zero n). -2: rewrite rev_length, length_generate_word, rev_length, H0; +2: rewrite length_rev, length_generate_word, length_rev, H0; change c48 with 48%nat; lia. f_equal. rewrite generate_word_small by lia. @@ -1134,7 +1134,7 @@ rewrite (rnd_64_S _ _ _ 2:{ unfold nthi; rewrite Nat2Z.id. apply (@coqlib4.nth_error_nth _ _ Int.zero (n+16)). -rewrite rev_length, length_generate_word, rev_length, H0; +rewrite length_rev, length_generate_word, length_rev, H0; change c48 with 48%nat; lia. } rewrite Round_equation. @@ -1176,7 +1176,7 @@ destruct blocks; inv H. rewrite process_msg_equation, hash_blocks_equation. reflexivity. assert (length (firstn 16 blocks) = 16)%nat - by (rewrite firstn_length, H; simpl; lia). + by (rewrite length_firstn, H; simpl; lia). rewrite hash_blocks_equation. destruct blocks; [ inv H | ]. forget (i::blocks) as bb. @@ -1185,7 +1185,7 @@ rewrite <- (firstn_skipn 16 blocks) at 1. rewrite process_msg_eq2 by auto. rewrite process_block_hash_block; auto. apply IHn0. -rewrite skipn_length; lia. +rewrite length_skipn; lia. apply length_hash_block; auto. Qed. diff --git a/sha/hmac_common_lemmas.v b/sha/hmac_common_lemmas.v index 4305e5c2a..a4088342b 100644 --- a/sha/hmac_common_lemmas.v +++ b/sha/hmac_common_lemmas.v @@ -30,7 +30,7 @@ Qed. Lemma Zlength_mkArgZ k pad: Zlength (HMAC_SHA256.mkArg k pad) = Z.of_nat (min (length k) 64). Proof. intros. repeat rewrite Zlength_correct. unfold HMAC_SHA256.mkArg, HMAC_SHA256.sixtyfour. - repeat rewrite map_length. + repeat rewrite length_map. rewrite combine_length, repeat_length. trivial. Qed. @@ -78,7 +78,7 @@ Qed. Lemma zeroPad_BlockSize: forall k, (length k <= SHA256.BlockSize)%nat -> length (HMAC_SHA256.zeroPad k) = SHA256.BlockSize%nat. -Proof. unfold HMAC_SHA256.zeroPad. intros. rewrite app_length, (*length_Nlist*) repeat_length. lia. +Proof. unfold HMAC_SHA256.zeroPad. intros. rewrite length_app, (*length_Nlist*) repeat_length. lia. Qed. Lemma length_SHA256': forall l, diff --git a/sha/hmac_pure_lemmas.v b/sha/hmac_pure_lemmas.v index 9b06b7c0e..4d32e2c9a 100644 --- a/sha/hmac_pure_lemmas.v +++ b/sha/hmac_pure_lemmas.v @@ -61,9 +61,9 @@ Proof. induction l1; simpl; intros. { destruct m1; simpl in *. split; trivial. assert (length l2 = length (a :: m1 ++ m2)). rewrite <- H; trivial. - rewrite H1 in H0; clear H H1. simpl in H0. rewrite app_length in H0. lia. } + rewrite H1 in H0; clear H H1. simpl in H0. rewrite length_app in H0. lia. } { assert (length (a :: l1 ++ l2) = length (m1 ++ m2)). rewrite <- H; trivial. - simpl in H1. do 2 rewrite app_length in H1. rewrite H0 in H1. + simpl in H1. do 2 rewrite length_app in H1. rewrite H0 in H1. destruct m1; simpl in *. lia. inversion H; clear H. subst a0. destruct (IHl1 _ _ _ H4 H0). subst. split; trivial. } @@ -120,7 +120,7 @@ Proof. apply IHk; auto. lia. Qed. -Lemma skipn_length: +Lemma length_skipn: forall {A} n (al: list A), (length al >= n)%nat -> (length (skipn n al) = length al - n)%nat. diff --git a/sha/pure_lemmas.v b/sha/pure_lemmas.v index b85b9f2c7..0650250f3 100644 --- a/sha/pure_lemmas.v +++ b/sha/pure_lemmas.v @@ -251,7 +251,7 @@ rewrite <- Heql in *; clear i l Heql. rewrite firstn_same by lia. replace (skipn LBLOCK c) with (@nil int). rewrite hash_blocks_equation'; reflexivity. -pose proof (skipn_length c LBLOCK). +pose proof (length_skipn c LBLOCK). rewrite H1 in H0. destruct (skipn LBLOCK c); try reflexivity; inv H0. replace (S n * LBLOCK)%nat with (n * LBLOCK + LBLOCK)%nat in H0 by @@ -275,9 +275,9 @@ Psatz.nia. apply skipn_app1. Psatz.nia. apply length_hash_block; auto. (* fixme *) change 16%nat with LBLOCK. -rewrite firstn_length. apply min_l. +rewrite length_firstn. apply min_l. Psatz.nia. -rewrite skipn_length. +rewrite length_skipn. lia. Qed. @@ -304,8 +304,8 @@ rewrite hash_blocks_equation'; auto. forget (i::blocks) as bb. apply IHn0; auto. apply length_hash_block; auto. (* fixme *) change 16%nat with LBLOCK. -rewrite firstn_length. nia. -rewrite skipn_length. nia. +rewrite length_firstn. nia. +rewrite length_skipn. nia. Qed. Theorem Zmod_mod_mult : diff --git a/sha/sha_lemmas.v b/sha/sha_lemmas.v index 3831f93c1..dd2ce9eb0 100644 --- a/sha/sha_lemmas.v +++ b/sha/sha_lemmas.v @@ -216,7 +216,7 @@ Ltac Omega1 := Omega (helper1 || helper2). Ltac Omega1 := rep_lia. Ltac MyOmega := - rewrite ?repeat_length, ?skipn_length, ?map_length, + rewrite ?repeat_length, ?length_skipn, ?length_map, ?Zlength_map, ?Zlength_nil; pose proof CBLOCK_eq; (* pose proof CBLOCKz_eq;*) diff --git a/sha/sha_padding_lemmas.v b/sha/sha_padding_lemmas.v index c60afd957..c01ab3c33 100644 --- a/sha/sha_padding_lemmas.v +++ b/sha/sha_padding_lemmas.v @@ -37,7 +37,7 @@ Lemma fstpad_len : Proof. intros msg. simpl. - rewrite -> app_length. + rewrite -> length_app. simpl. rewrite -> repeat_length. reflexivity. @@ -73,7 +73,7 @@ Proof. intros msg. unfold pad. rewrite -> Zlength_correct. - repeat rewrite -> app_length. + repeat rewrite -> length_app. simpl. assert (succ: forall (n : nat), S n = (n + 1)%nat). intros. induction n. reflexivity. lia. @@ -162,7 +162,7 @@ Proof. pose proof pad_len_64_nat msg as pad_len_64_nat. unfold pad in *. - repeat rewrite -> app_length in *. + repeat rewrite -> length_app in *. destruct pad_len_64_nat. assert (sym: (64 * x)%nat = (x * 64)%nat) by lia. rewrite -> sym in *. clear sym. diff --git a/sha/verif_hmac_init.v b/sha/verif_hmac_init.v index f99a06488..39675c469 100644 --- a/sha/verif_hmac_init.v +++ b/sha/verif_hmac_init.v @@ -180,11 +180,11 @@ forward_if (EX shaStates:_ , remember (map Vubyte (HMAC_SHA256.mkArg (HMAC_SHA256.mkKey key) Opad)) as OPADcont. assert (ZLI: Zlength (HMAC_SHA256.mkArg (HMAC_SHA256.mkKey key) Ipad) = 64). rewrite Zlength_mkArgZ. - repeat rewrite map_length. rewrite mkKey_length. + repeat rewrite length_map. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. trivial. assert (ZLO: Zlength (HMAC_SHA256.mkArg (HMAC_SHA256.mkKey key) Opad) = 64). rewrite Zlength_mkArgZ. - repeat rewrite map_length. rewrite mkKey_length. + repeat rewrite length_map. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. trivial. unfold data_at_, tarray. Time assert_PROP (isptr pad) as Ppad by entailer!. (*1*) diff --git a/sha/verif_hmac_init_part2.v b/sha/verif_hmac_init_part2.v index b24dad6f1..c0e790d31 100644 --- a/sha/verif_hmac_init_part2.v +++ b/sha/verif_hmac_init_part2.v @@ -290,7 +290,7 @@ Proof. intros. abbreviate_semax. = Vubyte qb). (* (Int.zero_ext 8 q)).*) { unfold Znth. destruct (Z_lt_dec i 0). lia. rewrite nth_indep with (d':=Vubyte Byte.zero). - 2:{ repeat rewrite map_length. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. apply (Z2Nat.inj_lt _ 64); lia. } + 2:{ repeat rewrite length_map. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. apply (Z2Nat.inj_lt _ 64); lia. } repeat rewrite map_nth. rewrite Qb. trivial. } @@ -427,7 +427,7 @@ freeze FR1 := - (data_at _ _ _ (Vptr ckb _)) (data_block _ _ _). = Vubyte qb). (* (Int.zero_ext 8 q)).*) { unfold Znth. destruct (Z_lt_dec i 0). lia. rewrite nth_indep with (d':=Vubyte Byte.zero). - 2:{ repeat rewrite map_length. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. apply (Z2Nat.inj_lt _ 64); lia. } + 2:{ repeat rewrite length_map. rewrite mkKey_length. unfold SHA256.BlockSize; simpl. apply (Z2Nat.inj_lt _ 64); lia. } repeat rewrite map_nth. rewrite Qb. trivial. } freeze FR2 := - (data_at _ _ _ (Vptr ckb _)). diff --git a/sha/verif_sha_bdo7.v b/sha/verif_sha_bdo7.v index 3bee00c09..390769c69 100644 --- a/sha/verif_sha_bdo7.v +++ b/sha/verif_sha_bdo7.v @@ -37,7 +37,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. lia. diff --git a/tweetnacl20140427/split_array_lemmas.v b/tweetnacl20140427/split_array_lemmas.v index de6952473..689aeb5da 100644 --- a/tweetnacl20140427/split_array_lemmas.v +++ b/tweetnacl20140427/split_array_lemmas.v @@ -427,17 +427,17 @@ Lemma split3_data_at_Tarray_at_tuchar: Proof. fold reptype in *. assert (Arith1: Zlength (firstn (lo + n) data) = Z.of_nat (lo + n)). - repeat rewrite Zlength_correct. rewrite firstn_length, min_l; trivial. + repeat rewrite Zlength_correct. rewrite length_firstn, min_l; trivial. rewrite split_offset_array_at with (n := (lo + n)%nat); trivial. (* by lia.*) rewrite split_offset_array_at with (n := lo) (contents := firstn (lo + n) data); trivial. (* by - (rewrite firstn_length; rewrite Min.min_l by lia; lia).*) + (rewrite length_firstn; rewrite Min.min_l by lia; lia).*) assert (!!offset_in_range (sizeof t * Zlength data) d |-- !! offset_in_range (sizeof t * Zlength (firstn (lo + n) data)) d)%logic. remember (sizeof t) as ST; normalize; subst ST. apply offset_in_range_mid with (lo := 0%Z) (hi := Zlength data); try assumption. rewrite !Zlength_correct. - rewrite firstn_length; rewrite Min.min_l by lia. split; try lia. + rewrite length_firstn; rewrite Min.min_l by lia. split; try lia. apply inj_le, N. rewrite Zmult_0_r. unfold offset_in_range; destruct d; auto. @@ -471,17 +471,17 @@ Lemma split3_offset_array_at Proof. fold reptype in *. assert (Arith1: Zlength (firstn (lo + n) data) = Z.of_nat (lo + n)). - repeat rewrite Zlength_correct. rewrite firstn_length, min_l; trivial. + repeat rewrite Zlength_correct. rewrite length_firstn, min_l; trivial. rewrite split_offset_array_at with (n := (lo + n)%nat); trivial. (* by lia.*) rewrite split_offset_array_at with (n := lo) (contents := firstn (lo + n) data); trivial. (* by - (rewrite firstn_length; rewrite Min.min_l by lia; lia).*) + (rewrite length_firstn; rewrite Min.min_l by lia; lia).*) assert (!!offset_in_range (sizeof t * Zlength data) d |-- !! offset_in_range (sizeof t * Zlength (firstn (lo + n) data)) d)%logic. remember (sizeof t) as ST; normalize; subst ST. apply offset_in_range_mid with (lo := 0%Z) (hi := Zlength data); try assumption. rewrite !Zlength_correct. - rewrite firstn_length; rewrite Min.min_l by lia. split; try lia. + rewrite length_firstn; rewrite Min.min_l by lia. split; try lia. apply inj_le, N. rewrite Zmult_0_r. unfold offset_in_range; destruct d; auto. @@ -528,9 +528,9 @@ intros. subst. rewrite (split_offset_Tarray_at (length data1) sh t (Zlength (data1++data2)) (data1 ++ data2) d H); repeat rewrite Zlength_correct. rewrite firstn_exact, skipn_exact; trivial. -rewrite app_length, Nat2Z.inj_add, Z.add_simpl_l; trivial. -rewrite app_length, Nat2Z.inj_add. lia. -rewrite app_length, Nat2Z.inj_add. lia. +rewrite length_app, Nat2Z.inj_add, Z.add_simpl_l; trivial. +rewrite length_app, Nat2Z.inj_add. lia. +rewrite length_app, Nat2Z.inj_add. lia. Qed. Lemma append_split3_Tarray_at @@ -548,13 +548,13 @@ Lemma append_split3_Tarray_at Proof. subst. erewrite (split3_offset_Tarray_at t A (length data1) (length data2)). - 2: repeat rewrite app_length; lia. + 2: repeat rewrite length_app; lia. rewrite firstn_exact; trivial. rewrite skipn_exact; trivial. rewrite firstn_exact; trivial. - rewrite app_assoc, skipn_app2. 2: rewrite app_length; lia. + rewrite app_assoc, skipn_app2. 2: rewrite length_app; lia. assert (Arith1: (length data1 + length data2 - (length data1 + length data2) = 0)%nat) by lia. - f_equal. repeat rewrite Zlength_correct. repeat rewrite app_length. + f_equal. repeat rewrite Zlength_correct. repeat rewrite length_app. rewrite Arith1; clear Arith1. simpl. f_equal. repeat rewrite Nat2Z.inj_add. rewrite Z.mul_add_distr_l. assert (Arith: Z.of_nat (length data1) + Z.of_nat (length data2) + diff --git a/tweetnacl20140427/tweetNaclBase.v b/tweetnacl20140427/tweetNaclBase.v index 56925092f..734eec731 100644 --- a/tweetnacl20140427/tweetNaclBase.v +++ b/tweetnacl20140427/tweetNaclBase.v @@ -18,11 +18,11 @@ Lemma isptrD v: isptr v -> exists b ofs, v = Vptr b ofs. Proof. intros. destruct v; try contradiction. exists b, i; trivial. Qed. Lemma firstn_Zlength {A} (l:list A) n: (n <= length l)%nat -> Zlength (firstn n l) = Z.of_nat n. -Proof. intros. rewrite Zlength_correct, firstn_length, Nat.min_l; trivial. Qed. +Proof. intros. rewrite Zlength_correct, length_firstn, Nat.min_l; trivial. Qed. Lemma skipn_Zlength {A} (l:list A) n: (n <= length l)%nat -> Zlength (skipn n l) = Zlength l - (Z.of_nat n). Proof. intros. - rewrite Zlength_correct, skipn_length. + rewrite Zlength_correct, length_skipn. rewrite Zlength_correct, Nat2Z.inj_sub; trivial. Qed. diff --git a/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v b/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v index a87a258a7..87b6b3fda 100644 --- a/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v +++ b/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v @@ -170,7 +170,7 @@ Intros snuff. rename H into Snuff. destruct (QuadChunks2ValList_bytes (map littleendian_invert snuff)) as [sr_bytes [SRBL SNR]]. assert (SRL: Zlength sr_bytes = 64). { - rewrite map_length, (Snuffle20_length _ _ Snuff) in SRBL. + rewrite length_map, (Snuffle20_length _ _ Snuff) in SRBL. rewrite Zlength_correct, SRBL. reflexivity. apply prepare_data_length. } @@ -322,7 +322,7 @@ forward_if (IfPost v_z v_x bInit (N0, N1, N2, N3) K mCont (Int64.unsigned bInit) Intros snuff. rename H into Snuff. destruct (QuadChunks2ValList_bytes (map littleendian_invert snuff)) as [sr_bytes [SRBL SNR]]. assert (Zlength sr_bytes = 64). - rewrite map_length, (Snuffle20_length _ _ Snuff) in SRBL. + rewrite length_map, (Snuffle20_length _ _ Snuff) in SRBL. rewrite Zlength_correct, SRBL. reflexivity. apply prepare_data_length. rename H into SRL. diff --git a/tweetnacl20140427/verif_salsa_base.v b/tweetnacl20140427/verif_salsa_base.v index 8f211e64d..34950fcf9 100644 --- a/tweetnacl20140427/verif_salsa_base.v +++ b/tweetnacl20140427/verif_salsa_base.v @@ -185,7 +185,7 @@ Definition littleendian_of_SixteenByte (x:SixteenByte): QuadWord := rewrite Zlength_correct, QuadWR_length. trivial. Qed. Lemma SixteenWR_length s: length (SixteenWordRep s) = 16%nat. destruct s as [[[? ?] ?] ?]. simpl. - repeat rewrite app_length. repeat rewrite QuadWR_length. reflexivity. Qed. + repeat rewrite length_app. repeat rewrite QuadWR_length. reflexivity. Qed. Lemma SixteenWR_zlength s: Zlength (SixteenWordRep s) = 16. rewrite Zlength_correct, SixteenWR_length. trivial. Qed. @@ -265,7 +265,7 @@ Qed. Proof. destruct s as [[[q0 q1] q2] q3]. reflexivity. Qed. Lemma SixteenWordRepI_length s: length (SixteenWordRepI s) = 16%nat. Proof. destruct s as [[[q0 q1] q2] q3]. simpl. - repeat rewrite app_length. repeat rewrite QuadWordRepI_length. reflexivity. + repeat rewrite length_app. repeat rewrite QuadWordRepI_length. reflexivity. Qed. Lemma QuadByte2ValList_bytes q: exists bytes, length bytes = 4%nat /\ @@ -282,7 +282,7 @@ Proof. destruct N as [[[q0 q1] q2] q3]. rewrite SixteenByte2ValList_char. destruct (QuadByte2ValList_bytes q2) as [bytes2 [L2 Q2]]; rewrite Q2. destruct (QuadByte2ValList_bytes q3) as [bytes3 [L3 Q3]]; rewrite Q3. exists (bytes0 ++ bytes1 ++ bytes2 ++ bytes3). - repeat rewrite map_app. repeat rewrite app_length. rewrite L0, L1, L2, L3. + repeat rewrite map_app. repeat rewrite length_app. rewrite L0, L1, L2, L3. split; trivial. Qed. @@ -302,7 +302,7 @@ Proof. destruct N as [[[q0 q1] q2] q3]. rewrite SixteenByte2ValList_char. destruct (QuadByte2ValList_ints q2) as [ints2 [L2 Q2]]; rewrite Q2. destruct (QuadByte2ValList_ints q3) as [ints3 [L3 Q3]]; rewrite Q3. exists (ints0 ++ ints1 ++ ints2 ++ ints3). - repeat rewrite map_app. repeat rewrite app_length. rewrite L0, L1, L2, L3. + repeat rewrite map_app. repeat rewrite length_app. rewrite L0, L1, L2, L3. split; trivial. Qed. @@ -314,7 +314,7 @@ Lemma QuadChunks2ValList_bytes: forall l, destruct IHl as [? [X1 X2]]; rewrite X2; clear X2. destruct (QuadByte2ValList_bytes a) as [? [Y1 Y2]]; rewrite Y2; clear Y2. repeat rewrite <- map_app. exists (x0 ++ x); split; trivial. - rewrite app_length, X1, Y1. lia. + rewrite length_app, X1, Y1. lia. Qed. Fixpoint upd_upto (x: SixteenByte * SixteenByte * (SixteenByte * SixteenByte)) i (l:list val):list val := diff --git a/veric/Clight_initial_world.v b/veric/Clight_initial_world.v index cefa8e293..7a5c8e699 100644 --- a/veric/Clight_initial_world.v +++ b/veric/Clight_initial_world.v @@ -139,13 +139,13 @@ change (AST.prog_defs prog) with (prog_defs prog) in Hm. forget (prog_defs prog) as dl. rewrite <- (rev_involutive dl) in H1,Hm. rewrite nth_error_rev in H1. -2 : { rewrite rev_length. clear - RANGE. +2 : { rewrite length_rev. clear - RANGE. destruct RANGE. apply inj_lt_iff. rewrite Z2Nat.id by lia. lia. } rename H1 into H5. replace (length (rev dl) - Z.to_nat (Z.pos b - 1) - 1)%nat with (length (rev dl) - Z.to_nat (Z.pos b))%nat in H5. -2 : { rewrite rev_length. +2 : { rewrite length_rev. clear - RANGE. replace (Z.to_nat (Z.pos b-1)) with (Z.to_nat (Z.pos b) - 1)%nat. assert (Z.to_nat (Z.pos b) <= length dl)%nat. @@ -162,7 +162,7 @@ assert (0 < Z.to_nat (Z.pos b) <= length dl)%nat. { clear - RANGE. lia. } clear RANGE; rename H0 into RANGE. rewrite Z2Nat.inj_pos in *. -rewrite <- rev_length in RANGE. +rewrite <- length_rev in RANGE. forget (rev dl) as dl'; clear dl; rename dl' into dl. destruct RANGE. rewrite alloc_globals_rev_eq in Hm. @@ -320,13 +320,13 @@ forget (prog_defs prog) as dl. rewrite <- (rev_involutive dl) in H1,Hm. rewrite nth_error_rev in H1. 2 : { - rewrite rev_length. clear - RANGE. + rewrite length_rev. clear - RANGE. destruct RANGE. apply inj_lt_iff. rewrite Z2Nat.id by lia. lia. } rename H1 into H5. replace (length (rev dl) - Z.to_nat (Z.pos b - 1) - 1)%nat with (length (rev dl) - Z.to_nat (Z.pos b))%nat in H5. -2 : { rewrite rev_length. +2 : { rewrite length_rev. clear - RANGE. replace (Z.to_nat (Z.pos b-1)) with (Z.to_nat (Z.pos b) - 1)%nat. assert (Z.to_nat (Z.pos b) <= length dl)%nat. @@ -343,7 +343,7 @@ assert (0 < Z.to_nat (Z.pos b) <= length dl)%nat. { clear - RANGE. lia. } clear RANGE; rename H0 into RANGE. rewrite Z2Nat.inj_pos in *. -rewrite <- rev_length in RANGE. +rewrite <- length_rev in RANGE. forget (rev dl) as dl'; clear dl; rename dl' into dl. destruct RANGE. rewrite alloc_globals_rev_eq in Hm. diff --git a/veric/initial_world.v b/veric/initial_world.v index 8a64b19d5..abdaf846a 100644 --- a/veric/initial_world.v +++ b/veric/initial_world.v @@ -701,13 +701,13 @@ Proof. induction vl; simpl; intros. apply nth_error_nil. destruct (eq_dec n (length vl)). subst. - pattern (length vl) at 1; rewrite <- rev_length. + pattern (length vl) at 1; rewrite <- length_rev. rewrite <- (Nat.add_0_r (length (rev vl))). rewrite nth_error_app. case_eq (length vl); intros. simpl. auto. replace (S n - n - 1)%nat with O by lia. simpl; auto. - rewrite nth_error_app1 by (rewrite rev_length; lia). + rewrite nth_error_app1 by (rewrite length_rev; lia). rewrite IHvl by lia. clear IHvl. destruct n; destruct (length vl). congruence. simpl. replace (n-0)%nat with n by lia; auto. @@ -786,9 +786,9 @@ Proof. intros. subst. rewrite map_rev; rewrite nth_error_rev. replace (length (map fst vl) - Z.to_nat (Zpos b - 1) - 1)%nat with (length vl - Pos.to_nat b)%nat ; [intuition | ]. - rewrite map_length. + rewrite length_map. transitivity (length vl - (Z.to_nat (Z.pos b-1)+1))%nat; try lia. - rewrite map_length. + rewrite length_map. rewrite Zlength_correct in H1. forget (Z.pos b-1) as i; forget (length vl) as n; clear - H1. apply inj_lt_rev. rewrite Z_to_nat_max; auto. @@ -807,9 +807,9 @@ Proof. intros. subst. by (rewrite <- e; replace (1 + (Z.pos b - 1)) with (Z.pos b) by lia; apply Pos2Z.id). clear e b. - rewrite <- Zlength_rev. rewrite <- rev_length. + rewrite <- Zlength_rev. rewrite <- length_rev. replace (length (rev vl)) with (length (rev vl) + 0)%nat by lia. - rewrite map_app. rewrite <- map_length with (f:=@fst ident (globdef (fundef F) type)). + rewrite map_app. rewrite <- length_map with (f:=@fst ident (globdef (fundef F) type)). rewrite nth_error_app. apply iff_trans with (i=id); [ | simpl; split; intro; subst; auto; inv H; auto]. rewrite In_rev in H2. rewrite <- map_rev in H2. @@ -852,7 +852,7 @@ Proof. intros. subst. f_equal. clear - H H2. forget (Z.to_nat (Z.pos b-1)) as j. replace (length vl) with (length (map fst (rev vl))) - by (rewrite map_length; rewrite rev_length; auto). + by (rewrite length_map; rewrite length_rev; auto). forget (map fst (rev vl)) as al. revert al H2 H; clear; induction j; destruct al; simpl; intros; auto. inv H; intuition. exfalso; clear - H; induction j; inv H; auto. @@ -862,21 +862,21 @@ Proof. intros. subst. destruct IHvl. split; intro. - apply H in H1. rewrite nth_error_app1; auto. - clear - n Hb. rewrite map_length. rewrite rev_length. rewrite Zlength_correct in Hb,n. + clear - n Hb. rewrite length_map. rewrite length_rev. rewrite Zlength_correct in Hb,n. assert (Z.pos b-1>=0) by lia. pose proof (Z2Nat.id _ (Z.ge_le _ _ H)). forget (Z.to_nat(Z.pos b-1)) as j. rewrite <- H0 in *. destruct Hb. clear - H2 n. lia. - assert (Z.to_nat (Z.pos b-1) < length (map (@fst _ _) (rev vl)))%nat. { clear - Hb n H1. - rewrite Zlength_correct in n. rewrite map_length; rewrite rev_length. + rewrite Zlength_correct in n. rewrite length_map; rewrite length_rev. assert (Z.to_nat (Z.pos b-1) <> length vl). { contradict n. rewrite <- n. rewrite Z2Nat.id; auto. lia. } forget (Z.to_nat (Z.pos b-1)) as j. clear - H1 H. assert (S (length vl) = length (map fst (rev vl) ++ map fst ((i, g) :: nil))). - { simpl. rewrite app_length; rewrite map_length; rewrite rev_length; simpl; lia. } + { simpl. rewrite length_app; rewrite length_map; rewrite length_rev; simpl; lia. } assert (j < S (length vl))%nat; [ | lia]. rewrite H0. forget (map fst (rev vl) ++ map fst ((i, g) :: nil)) as al. clear - H1. revert al H1; induction j; destruct al; simpl in *; intros; inv H1; auto; try lia. @@ -928,7 +928,7 @@ assert (RANGE: 0 <= Z.pos b - 1 < Zlength (rev (prog_defs prog))). { } split. rewrite Zlength_correct in RANGE. - rewrite rev_length in RANGE. lia. + rewrite length_rev in RANGE. lia. rewrite <- list_norepet_rev in H. unfold prog_defs_names in H. change (AST.prog_defs prog) with (prog_defs prog) in H. @@ -943,7 +943,7 @@ assert (RANGE: 0 <= Z.pos b - 1 < Zlength (rev (prog_defs prog))). { destruct p; simpl in H1. inv H1. exists g. rewrite <- H0. f_equal. - rewrite rev_length. rewrite map_length. + rewrite length_rev. rewrite length_map. clear - RANGE. rewrite Zlength_rev in RANGE. rewrite Zlength_correct in RANGE. rewrite <- (Z2Nat.id (Z.pos b)) in * by lia. @@ -953,9 +953,9 @@ assert (RANGE: 0 <= Z.pos b - 1 < Zlength (rev (prog_defs prog))). { rewrite Nat2Z.id. lia. inv H1. - rewrite rev_length. rewrite map_length. + rewrite length_rev. rewrite length_map. clear - RANGE. rewrite Zlength_correct in RANGE. - rewrite rev_length in RANGE. + rewrite length_rev in RANGE. forget (length (prog_defs prog)) as N. assert (Z_of_nat N > 0) by lia. destruct N; inv H. diff --git a/veric/invariants.v b/veric/invariants.v index 314eeb5de..559023741 100644 --- a/veric/invariants.v +++ b/veric/invariants.v @@ -231,7 +231,7 @@ Qed. Lemma singleton_length : forall {A} n (a : A), length (list_singleton n a) = S n. Proof. intros; unfold list_singleton. - erewrite app_length, repeat_length; simpl; lia. + erewrite length_app, repeat_length; simpl; lia. Qed. Lemma list_join_singleton : forall {P : Ghost} n a c l @@ -239,7 +239,7 @@ Lemma list_join_singleton : forall {P : Ghost} n a c l list_join (list_singleton n a) l (replace_nth n l (Some c)). Proof. induction l using rev_ind; simpl; intros; try lia. - rewrite app_length in Hn; simpl in Hn. + rewrite length_app in Hn; simpl in Hn. destruct (eq_dec n (length l)). - subst. erewrite app_nth2, Nat.sub_diag in Hjoin by lia; simpl in Hjoin. @@ -410,13 +410,13 @@ Proof. change [] with (core b); apply core_unit. + assert (a <> []) by (intro; subst; discriminate). erewrite (app_removelast_last None) in H, Heqn by auto. - erewrite app_length in Heqn; simpl in Heqn. + erewrite length_app in Heqn; simpl in Heqn. erewrite Nat.add_1_r in Heqn; inv Heqn. specialize (IHn _ eq_refl). destruct (IHn b c) as (c' & ? & ?); auto. { destruct H as [Hlen H]. split. - { rewrite app_length in Hlen; simpl in *; lia. } + { rewrite length_app in Hlen; simpl in *; lia. } intros ?? Hnth. specialize (H n a0). rewrite app_nth in H. @@ -432,7 +432,7 @@ Proof. apply join_comm in H2; auto. -- split. { destruct H. - erewrite app_length in *; simpl in *; lia. } + erewrite length_app in *; simpl in *; lia. } intros ?? Hnth. rewrite app_nth in Hnth. if_tac in Hnth; [apply H3; auto|]. @@ -870,13 +870,13 @@ Proof. exists (x ++ [Some (Some tt)]); split; simpl; auto. erewrite !map_app, own.map_repeat; simpl. pose proof (list_join_length _ _ _ H1) as Hlen. - rewrite map_length in Hlen. + rewrite length_map in Hlen. apply join_comm in H1. pose proof (list_join_length _ _ _ H1) as Hlen'. apply (join_comm(Perm_alg := list_Perm)), (list_join_over c). - { erewrite app_length, map_length, repeat_length, Nat.add_comm, Nat.sub_add; auto. } + { erewrite length_app, length_map, repeat_length, Nat.add_comm, Nat.sub_add; auto. } apply (join_comm(Perm_alg := list_Perm)), (list_join_filler(P := token_PCM)); - [|rewrite map_length; auto]. + [|rewrite length_map; auto]. apply join_comm in H1; auto. } rewrite exp_sepcon1; apply exp_left; intro. rewrite !sepcon_andp_prop1; apply prop_andp_left; intros [i ?]; subst. @@ -895,12 +895,12 @@ Proof. | Some _ => Some (Znth j ((lg ++ repeat O i) ++ [g])) | None => None end) (upto (length ((l ++ repeat emp i) ++ [P']))))). - { rewrite <- !app_assoc, app_length, upto_app, map_app. + { rewrite <- !app_assoc, length_app, upto_app, map_app. split. - { erewrite app_length, !map_length; lia. } + { erewrite length_app, !length_map; lia. } intros ?? Hn. - erewrite app_nth, map_length. - if_tac; [|erewrite nth_overflow in Hn by (rewrite map_length; lia); discriminate]. + erewrite app_nth, length_map. + if_tac; [|erewrite nth_overflow in Hn by (rewrite length_map; lia); discriminate]. erewrite nth_map' with (d' := 0) in * by auto. erewrite upto_length in *. assert (Z.of_nat n < Zlength l). @@ -911,7 +911,7 @@ Proof. rewrite !sepcon_assoc. view_shift (ghost_snap_forget(ORD := list_order _) (list_singleton (length lg + i) g)). { apply list_incl_singleton. - erewrite app_length, upto_app, map_app, app_nth2; erewrite map_length, upto_length, app_length, + erewrite length_app, upto_app, map_app, app_nth2; erewrite length_map, upto_length, length_app, repeat_length; try lia. replace (_ - _)%nat with O by lia; simpl. rewrite Nat2Z.inj_add, Z.add_0_r. @@ -921,8 +921,8 @@ Proof. apply exp_right with ((l ++ repeat emp i) ++ [P']). rewrite exp_sepcon1; apply exp_right with ((lg ++ repeat O i) ++ [g]). rewrite exp_sepcon1; apply exp_right with ((lb ++ repeat None i) ++ [Some true]). - erewrite !(app_length (_ ++ _)); simpl. - erewrite prop_true_andp by (erewrite !app_length, !repeat_length; lia). + erewrite !(length_app (_ ++ _)); simpl. + erewrite prop_true_andp by (erewrite !length_app, !repeat_length; lia). erewrite upto_app, iter_sepcon_app; simpl. erewrite Z.add_0_r, <- Zlength_correct, !app_Znth2; erewrite !Zlength_app, !coqlib4.Zlength_repeat; try lia. erewrite Hlg, Hlb, Zminus_diag, !Znth_0_cons. @@ -935,11 +935,11 @@ Proof. repeat destruct (lt_dec _ _); auto; try discriminate. destruct (x - _)%nat; [|destruct n0]; inv X. - destruct (lt_dec x (length lb)). - rewrite !app_nth, app_length. + rewrite !app_nth, length_app. destruct (lt_dec _ _); [|lia]. destruct (lt_dec _ _); [auto | lia]. { rewrite nth_overflow in X by lia; discriminate. } } - erewrite app_length, upto_app, iter_sepcon_app. + erewrite length_app, upto_app, iter_sepcon_app. rewrite sepcon_assoc; apply sepcon_derives. - eapply derives_trans with (_ * emp)%pred; [rewrite sepcon_emp; apply derives_refl|]. apply sepcon_derives. @@ -990,7 +990,7 @@ Proof. exists (map (fun o => match o with Some true => Some (Some tt) | _ => None end) ((lb ++ repeat None (i - length lb)) ++ [Some true])). pose proof (list_join_length _ _ _ H1) as Hlen. - rewrite map_length in Hlen. + rewrite length_map in Hlen. split. { exists (i - length lg)%nat; rewrite H, H0; split; auto. rewrite Nat.add_comm, Nat.sub_add; auto; lia. } @@ -999,13 +999,13 @@ Proof. apply join_comm in H1. rewrite app_assoc; apply (join_comm(Perm_alg := list_Perm)), (list_join_over c). { apply list_join_length in H1. - rewrite app_length, map_length, repeat_length, Nat.add_comm, Nat.sub_add; auto; lia. } + rewrite length_app, length_map, repeat_length, Nat.add_comm, Nat.sub_add; auto; lia. } replace (i - length lb)%nat with ((length x - length lb) + (i - length x))%nat by lia. rewrite repeat_app, app_assoc; apply (list_join_over c). { apply list_join_length in H1. - rewrite app_length, map_length, repeat_length; lia. } + rewrite length_app, length_map, repeat_length; lia. } apply (join_comm(Perm_alg := list_Perm)), (list_join_filler(P := token_PCM)); - [|rewrite map_length; auto]. + [|rewrite length_map; auto]. apply join_comm in H1; auto. } rewrite exp_sepcon1; apply exp_left; intro. rewrite !sepcon_andp_prop1; apply prop_andp_left; intros [i []]; subst. @@ -1023,12 +1023,12 @@ Proof. | Some _ => Some (Znth j ((lg ++ repeat O i) ++ [g])) | None => None end) (upto (length ((l ++ repeat emp i) ++ [P]))))). - { rewrite <- !app_assoc, app_length, upto_app, map_app. + { rewrite <- !app_assoc, length_app, upto_app, map_app. split. - { erewrite app_length, !map_length; lia. } + { erewrite length_app, !length_map; lia. } intros ?? Hn. - erewrite app_nth, map_length. - if_tac; [|erewrite nth_overflow in Hn by (rewrite map_length; lia); discriminate]. + erewrite app_nth, length_map. + if_tac; [|erewrite nth_overflow in Hn by (rewrite length_map; lia); discriminate]. erewrite nth_map' with (d' := 0) in * by auto. erewrite upto_length in *. assert (Z.of_nat n < Zlength l). @@ -1039,7 +1039,7 @@ Proof. rewrite !sepcon_assoc. view_shift (ghost_snap_forget(ORD := list_order _) (list_singleton (length lg + i) g)). { apply list_incl_singleton. - erewrite app_length, upto_app, map_app, app_nth2; erewrite map_length, upto_length, app_length, + erewrite length_app, upto_app, map_app, app_nth2; erewrite length_map, upto_length, length_app, repeat_length; try lia. replace (_ - _)%nat with O by lia; simpl. rewrite Nat2Z.inj_add, Z.add_0_r. @@ -1049,8 +1049,8 @@ Proof. apply exp_right with ((l ++ repeat emp i) ++ [P]). rewrite exp_sepcon1; apply exp_right with ((lg ++ repeat O i) ++ [g]). rewrite exp_sepcon1; apply exp_right with ((lb ++ repeat None i) ++ [Some true]). - erewrite !(app_length (_ ++ _)); simpl. - erewrite prop_true_andp by (erewrite !app_length, !repeat_length; lia). + erewrite !(length_app (_ ++ _)); simpl. + erewrite prop_true_andp by (erewrite !length_app, !repeat_length; lia). erewrite upto_app, iter_sepcon_app; simpl. erewrite Z.add_0_r, <- Zlength_correct, !app_Znth2; erewrite !Zlength_app, !coqlib4.Zlength_repeat; try lia. erewrite Hlg, Hlb, Zminus_diag, !Znth_0_cons. @@ -1063,11 +1063,11 @@ Proof. repeat destruct (lt_dec _ _); auto; try discriminate. destruct (x - _)%nat; [|destruct n0]; inv X. - destruct (lt_dec x (length lb)). - rewrite !app_nth, app_length. + rewrite !app_nth, length_app. destruct (lt_dec _ _); [|lia]. destruct (lt_dec _ _); [auto | lia]. { rewrite nth_overflow in X by lia; discriminate. } } - erewrite app_length, upto_app, iter_sepcon_app. + erewrite length_app, upto_app, iter_sepcon_app. rewrite sepcon_assoc; apply sepcon_derives. - eapply derives_trans with (_ * emp)%pred; [rewrite sepcon_emp; apply derives_refl|]. apply sepcon_derives. @@ -1128,7 +1128,7 @@ Proof. apply prop_derives; intros Hincl. apply list_incl_singleton in Hincl. destruct (lt_dec i (length lg)); - [|rewrite nth_overflow in Hincl by (rewrite map_length, upto_length; lia); discriminate]. + [|rewrite nth_overflow in Hincl by (rewrite length_map, upto_length; lia); discriminate]. rewrite nth_map' with (d' := 0) in Hincl by (rewrite upto_length; lia). rewrite nth_upto in Hincl by lia. destruct (Znth (Z.of_nat i) lb); inversion Hincl; eauto. } @@ -1215,7 +1215,7 @@ Proof. apply prop_derives; intros Hincl. apply list_incl_singleton in Hincl. destruct (lt_dec i (length lg)); - [|rewrite nth_overflow in Hincl by (rewrite map_length, upto_length; lia); discriminate]. + [|rewrite nth_overflow in Hincl by (rewrite length_map, upto_length; lia); discriminate]. rewrite nth_map' with (d' := 0) in Hincl by (rewrite upto_length; lia). rewrite nth_upto in Hincl by lia. destruct (Znth (Z.of_nat i) lb); inversion Hincl; eauto. } @@ -1279,7 +1279,7 @@ Proof. { unfold ghost_list. erewrite <- ghost_op; [apply derives_refl|]. rewrite map_replace_nth. apply (list_join_singleton(P := token_PCM)). - { rewrite map_length; lia. } + { rewrite length_map; lia. } rewrite nth_map' with (d' := None) by lia. rewrite Hi'; constructor. } Qed. diff --git a/veric/own.v b/veric/own.v index 2aebae2cc..68235e63a 100644 --- a/veric/own.v +++ b/veric/own.v @@ -678,18 +678,18 @@ Lemma list_set_set : forall {A} n l (a b : A), (n <= length l)%nat -> Proof. intros; unfold list_set. rewrite (proj2 (Nat.sub_0_le _ _) H). - rewrite !app_length, !skipn_app, firstn_app, firstn_length, min_l, Nat.sub_diag, app_nil_r, repeat_length by auto. + rewrite !length_app, !skipn_app, firstn_app, length_firstn, min_l, Nat.sub_diag, app_nil_r, repeat_length by auto. rewrite firstn_firstn, min_l by auto; f_equal. - unfold length; setoid_rewrite skipn_length; f_equal. + unfold length; setoid_rewrite length_skipn; f_equal. - f_equal. lia. - - rewrite skipn_all2, skipn_nil, Nat.sub_0_r; [|rewrite firstn_length; lia]. + - rewrite skipn_all2, skipn_nil, Nat.sub_0_r; [|rewrite length_firstn; lia]. rewrite (Nat.add_sub 1); auto. Qed. Lemma nth_list_set : forall {A} n l (a : A) d, nth n (list_set l n a) d = Some a. Proof. intros; unfold list_set. - rewrite 2app_nth2; rewrite ?repeat_length, ?firstn_length; try lia. + rewrite 2app_nth2; rewrite ?repeat_length, ?length_firstn; try lia. match goal with |- nth ?n _ _ = _ => replace n with O by lia end; auto. Qed. @@ -708,7 +708,7 @@ Proof. unfold list_set; rewrite !map_app, map_firstn, map_repeat. unfold map at 2; setoid_rewrite map_skipn. rewrite ghost_fmap_singleton; simpl Datatypes.option_map. - erewrite <- map_length. + erewrite <- length_map. rewrite level_core. inv J. + inj_pair_tac. @@ -728,7 +728,7 @@ Proof. constructor. rewrite H; eauto. Unshelve. * inv H0; auto. - * rewrite map_length. + * rewrite length_map. destruct (le_dec (length x) g); [|lia]. rewrite nth_overflow in H1 by auto; discriminate. * apply join_comm, join_valid in H2; auto. diff --git a/veric/semax_call.v b/veric/semax_call.v index 5905e6b47..9828b1834 100644 --- a/veric/semax_call.v +++ b/veric/semax_call.v @@ -2790,7 +2790,7 @@ Proof. destruct (build_call_temp_env f args) as [te' H21]; auto. { clear - H16' Hargs. simpl in H16'. unfold type_of_function in H16'. inv H16'. rewrite <- Hargs. - unfold type_of_params. rewrite map_length. auto. } + unfold type_of_params. rewrite length_map. auto. } pose proof (age_twin' _ _ _ H20' H13) as [jm''' [_ H20x]]. apply @jsafeN_step with (c' := State f (f.(fn_body)) ctl ve' te') (m' := jm'''); auto. diff --git a/veric/semax_prog.v b/veric/semax_prog.v index e1fa15059..69c808283 100644 --- a/veric/semax_prog.v +++ b/veric/semax_prog.v @@ -1857,7 +1857,7 @@ as [te' H21]; auto. destruct f; simpl in *. assert (Datatypes.length (map snd fn_params) = Datatypes.length params). assert (params = map snd fn_params) by apply H10. subst; trivial. - rewrite !map_length in H. rewrite H. + rewrite !length_map in H. rewrite H. clear - arg_p. apply tc_vals_length; trivial. } diff --git a/veric/superprecise.v b/veric/superprecise.v index 839fe564f..cf90cfb8b 100644 --- a/veric/superprecise.v +++ b/veric/superprecise.v @@ -48,7 +48,7 @@ Proof. intros. rewrite <- (rev_involutive i). rewrite <- (rev_involutive j). f_equal. assert (length (rev i) = length (rev j)). - repeat rewrite rev_length; auto. + repeat rewrite length_rev; auto. eapply int_of_bytes_uniq; eauto. apply int_of_bytes_uniq. Qed. diff --git a/veristar/clause_universe.v b/veristar/clause_universe.v index 4f97a4301..26e40381f 100644 --- a/veristar/clause_universe.v +++ b/veristar/clause_universe.v @@ -513,7 +513,7 @@ intros. unfold In. destruct x as [l' ?]. simpl in *. - replace (length (proj1_sig x')) with (length l') by (rewrite <- H2; apply map_length). + replace (length (proj1_sig x')) with (length l') by (rewrite <- H2; apply length_map). clear - n0 H1 H0. rename l' into l. revert F n n0 H0 H1; induction l; simpl; intros. diff --git a/veristar/redblack.v b/veristar/redblack.v index 66c3b75e5..f727844ef 100644 --- a/veristar/redblack.v +++ b/veristar/redblack.v @@ -4050,7 +4050,7 @@ Proof. unfold cardinal. intros; rewrite fold_spec. rewrite <- List.fold_left_rev_right. - rewrite <- List.rev_length. + rewrite <- List.length_rev. unfold elt. remember (@rev K.t (elements s)) as l; clear. clear; induction l; simpl; auto. diff --git a/zlist/sublist.v b/zlist/sublist.v index 505f65077..475402103 100644 --- a/zlist/sublist.v +++ b/zlist/sublist.v @@ -209,7 +209,7 @@ Proof. reflexivity. Qed. -Lemma skipn_length: forall {A} (contents: list A) n, +Lemma length_skipn: forall {A} (contents: list A) n, length (skipn n contents) = (length contents - n)%nat. Proof. intros. @@ -236,7 +236,7 @@ Proof. - simpl. apply IHcontents. lia. Qed. -Lemma skipn_length_short: +Lemma length_skipn_short: forall {A} n (al: list A), (length al <= n)%nat -> (length (skipn n al) = 0)%nat. @@ -250,7 +250,7 @@ Lemma skipn_short: forall {A} n (al: list A), (n >= length al)%nat -> skipn n al = nil. Proof. intros. -pose proof (skipn_length_short n al). +pose proof (length_skipn_short n al). assert (length al <= n)%nat by auto. specialize (H0 H1). destruct (skipn n al); inv H0; auto. @@ -337,13 +337,13 @@ Proof. induction n; intros. simpl. rewrite Nat.sub_0_r. rewrite firstn_exact_length. auto. destruct (rev vl) eqn:?. -pose proof (rev_length vl). rewrite Heql in H. +pose proof (length_rev vl). rewrite Heql in H. destruct vl; inv H. reflexivity. simpl. assert (vl = rev l ++ rev [a]). rewrite <- rev_app_distr. simpl app. rewrite <- Heql; rewrite rev_involutive; auto. rewrite H. -rewrite app_length. +rewrite length_app. simpl length. rewrite <- (rev_involutive l) at 1. rewrite IHn. @@ -386,14 +386,14 @@ Lemma rev_skipn: Proof. induction n; intros. simpl. rewrite Nat.sub_0_r. -rewrite <- rev_length. +rewrite <- length_rev. rewrite firstn_exact_length. auto. destruct vl. simpl. auto. simpl. rewrite IHn. -rewrite firstn_app1 by (rewrite rev_length; lia). +rewrite firstn_app1 by (rewrite length_rev; lia). auto. Qed. @@ -409,7 +409,7 @@ assert (n = (length vl - lo) - (length vl - (lo+n)))%nat by lia. rewrite H0 at 2. rewrite <- skipn_firstn. rewrite rev_skipn. -rewrite firstn_length. rewrite min_l by lia. +rewrite length_firstn. rewrite min_l by lia. f_equal. auto. Qed. @@ -672,7 +672,7 @@ Lemma Zlength_firstn: forall {A} n (v: list A), Zlength (firstn (Z.to_nat n) v) = Z.min (Z.max 0 n) (Zlength v). Proof. intros. rewrite !Zlength_correct. -rewrite firstn_length. +rewrite length_firstn. (* solve by SMT *) rewrite Zmin_spec, Zmax_spec. if_tac; [rewrite min_l | rewrite min_r]. @@ -694,7 +694,7 @@ Proof. intros. (* solve by SMT *) rewrite !Zlength_correct. -rewrite skipn_length. rewrite !Zmax_spec. +rewrite length_skipn. rewrite !Zmax_spec. if_tac. if_tac in H. lia. @@ -1243,7 +1243,7 @@ Lemma sublist_nil': forall (A : Type) (lo lo': Z) (al : list A), lo=lo' -> subli Proof. intros. subst. apply sublist_nil. Qed. Lemma sublist_skip {A} (l:list A) i : 0<=i -> sublist i (Zlength l) l = skipn (Z.to_nat i) l. -Proof. intros; unfold_sublist_old. apply firstn_same. rewrite skipn_length. +Proof. intros; unfold_sublist_old. apply firstn_same. rewrite length_skipn. rewrite Z2Nat.inj_sub, Zlength_correct, Nat2Z.id. lia. trivial. Qed. @@ -1255,7 +1255,7 @@ Lemma sublist_app1: 0 <= k <= i -> i <= Zlength al -> sublist k i (al ++ bl) = sublist k i al. Proof. intros. unfold_sublist_old. rewrite skipn_app1. rewrite firstn_app1. trivial. - rewrite skipn_length, Z2Nat.inj_sub. apply Nat2Z.inj_le. + rewrite length_skipn, Z2Nat.inj_sub. apply Nat2Z.inj_le. repeat rewrite Nat2Z.inj_sub. rewrite Z2Nat.id, <- Zlength_correct. lia. lia. rewrite <- ZtoNat_Zlength. apply Z2Nat.inj_le; lia. apply Z2Nat.inj_le; lia. lia. rewrite <- ZtoNat_Zlength. apply Z2Nat.inj_le; lia. @@ -1848,7 +1848,7 @@ Qed. Lemma Zlength_combine : forall {A B} (l : list A) (l' : list B), Zlength (combine l l') = Z.min (Zlength l) (Zlength l'). Proof. - intros; rewrite !Zlength_correct, combine_length, Nat2Z.inj_min; auto. + intros; rewrite !Zlength_correct, length_combine, Nat2Z.inj_min; auto. Qed. Lemma upd_Znth_cons : forall {A} i a l (x : A), i > 0 -> @@ -1922,14 +1922,14 @@ Qed. Lemma length_concat : forall {A} (l : list (list A)), length (concat l) = fold_right plus O (map (@length A) l). Proof. induction l; auto; simpl. - rewrite app_length, IHl; auto. + rewrite length_app, IHl; auto. Qed. Lemma length_concat_min : forall {A}{d: Inhabitant A} (l : list (list A)) i (Hi : 0 <= i < Zlength l), (length (Znth i l) <= length (concat l))%nat. Proof. induction l; simpl; intros; [rewrite Zlength_nil in *; lia|]. - rewrite app_length; destruct (Z.eq_dec i 0). + rewrite length_app; destruct (Z.eq_dec i 0). - subst; rewrite Znth_0_cons; lia. - rewrite Znth_pos_cons by lia. rewrite Zlength_cons in *; etransitivity; [apply IHl|]; lia. @@ -1940,10 +1940,10 @@ Lemma length_concat_upd : forall {A} {d: Inhabitant A} l i (l' : list A) (Hi : 0 Proof. induction l; intros; [rewrite Zlength_nil in *; lia|]. destruct (Z.eq_dec i 0). - - subst; rewrite upd_Znth0, Znth_0_cons. simpl. rewrite !app_length. lia. + - subst; rewrite upd_Znth0, Znth_0_cons. simpl. rewrite !length_app. lia. - rewrite upd_Znth_cons, Znth_pos_cons by lia; simpl. rewrite Zlength_cons in *. - rewrite !app_length, IHl by lia. + rewrite !length_app, IHl by lia. cut (length (Znth (i - 1) l) <= length (concat l))%nat. lia. apply length_concat_min. lia. Qed. @@ -2341,7 +2341,7 @@ Qed. Lemma upto_length : forall n, length (upto n) = n. Proof. induction n; auto; simpl. - rewrite map_length, IHn; auto. + rewrite length_map, IHn; auto. Qed. Corollary Zlength_upto : forall n, Zlength (upto n) = Z.of_nat n. @@ -2631,7 +2631,7 @@ Lemma rev_combine : forall {A B} (l1 : list A) (l2 : list B), length l1 = length rev (combine l1 l2) = combine (rev l1) (rev l2). Proof. induction l1; destruct l2; try discriminate; auto; simpl; intros. - inv H; rewrite combine_app; [|rewrite !rev_length; auto]. + inv H; rewrite combine_app; [|rewrite !length_rev; auto]. rewrite IHl1; auto. Qed. @@ -2919,7 +2919,7 @@ Lemma rotate_inj : forall {A} (l1 l2 : list A) n m, rotate l1 n m = rotate l2 n Proof. unfold rotate; intros. destruct (app_eq_len_eq H) as (Hskip & Hfirst). - { unfold sublist; repeat rewrite skipn_length, firstn_length. + { unfold sublist; repeat rewrite length_skipn, length_firstn. repeat rewrite Zlength_correct; rewrite H0; lia. } erewrite <- sublist_same with (al := l1), <- sublist_rejoin with (mid := m - n); auto; try lia. rewrite Hfirst, Hskip, sublist_rejoin, sublist_same; auto; try lia. @@ -3082,7 +3082,7 @@ Lemma list_Znth_eq : forall {A}{d: Inhabitant A} (l : list A), l = map (fun j => Znth j l) (upto (length l)). Proof. induction l; simpl; intros; auto. - rewrite Znth_0_cons, IHl, map_map, map_length, upto_length. + rewrite Znth_0_cons, IHl, map_map, length_map, upto_length. f_equal; apply map_ext_in; intros. rewrite Znth_pos_cons, <- IHl. unfold Z.succ; rewrite Z.add_simpl_r; auto.