move lemmas from Lib/Core to coqutil

mit-plv · May 2, 2022 · c510bd8 · c510bd8
1 parent 03b890b
commit c510bd8
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 757 deletions.
diff --git a/bedrock2 b/bedrock2
diff --git a/src/Rupicola/Lib/ArrayCasts.v b/src/Rupicola/Lib/ArrayCasts.v
@@ -78,15 +78,15 @@ Section with_parameters.
       length (bs2zs n bs) = Nat.div_up (length bs) n.
     Proof.
       unfold bs2zs; intros.
-      rewrite map_length, length_chunk, div_up_eqn.
+      rewrite map_length, length_chunk, Nat.div_up_eqn.
       all: auto.
     Qed.
 
     Lemma div_up_mod_eq a b:
       b <> 0 ->
       a mod b = 0 ->
       Nat.div_up a b = a / b.
-    Proof. intros H0 Hm; rewrite div_up_eqn, Hm; auto. Qed.
+    Proof. intros H0 Hm; rewrite Nat.div_up_eqn, Hm; auto. Qed.
 
     Lemma bs2zs_length n bs :
       (n <> 0)%nat ->

diff --git a/src/Rupicola/Lib/Arrays.v b/src/Rupicola/Lib/Arrays.v
@@ -60,9 +60,9 @@ Section ListArray.
     Proof.
       unfold put; intros ? -> ;
         rewrite !replace_nth_eqn by (rewrite ?app_length; lia).
-      rewrite List_firstn_app_l by reflexivity.
+      rewrite List.firstn_app_l by reflexivity.
       change (S ?x) with (1 + x); rewrite <- List.skipn_skipn.
-      rewrite List_skipn_app_r by reflexivity.
+      rewrite List.skipn_app_r by reflexivity.
       reflexivity.
     Qed.
   End __.