Replace deprecated lemmas

Barkhausen-Institut · Jun 28, 2024 · 34599d4 · 34599d4
1 parent 86d812e
commit 34599d4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/examples/pipeline_tutorial.v b/examples/pipeline_tutorial.v
@@ -404,7 +404,8 @@ The proof is a two-induction (captured by the ``Div2.ind_0_1_SS`` lemma); it tel
     Proof.
       intros r n.
       rewrite !iterate_S_acc, phi2_correct.
-      revert n; apply Div2.ind_0_1_SS; simpl. (* .unfold *)
+      revert n; apply Nat.pair_induction; simpl.
+      - Morphisms.solve_proper.
       - reflexivity.
       - unfold cycle; reflexivity.
       - intros n IH; simpl in IH; rewrite IH; reflexivity.

diff --git a/examples/rv/MultiplierCorrectness.v b/examples/rv/MultiplierCorrectness.v
@@ -35,9 +35,9 @@ Module MultiplierProofs.
     rewrite N.pow_succ_r'.
     rewrite (N.div_mod' a (2 ^ n)) at 1.
     rewrite N.testbit_spec'.
-    rewrite N.add_mod by (destruct n; cbn; lia).
+    rewrite N.Div0.add_mod by (destruct n; cbn; lia).
     rewrite (N.mul_comm 2 (2 ^ n)).
-    rewrite N.mul_mod_distr_l by (destruct n; cbn; lia).
+    rewrite N.Div0.mul_mod_distr_l by (destruct n; cbn; lia).
     rewrite (N.mod_small (a mod 2 ^ n)).
     - rewrite N.mod_small; [ ring | ].
       eapply N.le_lt_trans.