mit-plv · andres-erbsen · Mar 1, 2024 · Feb 29, 2024
diff --git a/rupicola b/rupicola
diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v
@@ -314,7 +314,7 @@ Module Fancy.
       Proof.
         intros. subst a b. autorewrite with push_Zmul.
         ring_simplify_subterms. rewrite Z.pow_2_r.
-        rewrite Z.div_add_exact by (push_Zmod; autorewrite with zsimplify; lia).
+        rewrite Z.div_add_exact by (push_Zmod; rewrite ?Zmod_0_l; lia).
         repeat match goal with
                | |- context [d * ?a * ?b * ?c] =>
                  replace (d * a * b * c) with (a * b * c * d) by ring

diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v
@@ -61,6 +61,7 @@ Section barrett.
 
     Lemma r_mod_3m_eq_orig : r_mod_3m = r_mod_3m_orig.
     Proof using base_pos k_big_enough m_pos m_small offset_nonneg r1 r2.
+      clear μ_good x_nonneg.
       assert (0 <= r1 < b^(k+offset)) by (subst r1; auto with zarith).
       assert (0 <= r2 < b^(k+offset)) by (subst r2; auto with zarith).
       subst r_mod_3m r_mod_3m_orig; cbv zeta.

diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
@@ -1106,7 +1106,7 @@ Module Positional.
     Lemma length_sub a b
       : length a = n -> length b = n ->
         length (sub a b) = n.
-    Proof using length_balance. intros; cbv [sub scmul negate_snd]; repeat distr_length. Qed.
+    Proof using length_balance. clear dependent s. intros; cbv [sub scmul negate_snd]; repeat distr_length. Qed.
     Hint Rewrite length_sub : distr_length.
     Definition opp (a:list Z) : list Z
       := sub (zeros n) a.
@@ -1119,7 +1119,7 @@ Module Positional.
     Proof using m_nz s_nz weight_0 weight_nz eval_balance length_balance. intros; cbv [opp]; push; distr_length; auto.       Qed.
     Lemma length_opp a
       : length a = n -> length (opp a) = n.
-    Proof using length_balance. cbv [opp]; intros; repeat distr_length.            Qed.
+    Proof using length_balance. clear dependent s. cbv [opp]; intros; repeat distr_length.            Qed.
   End sub.
   Hint Rewrite @eval_scmul @eval_opp @eval_sub : push_eval.
   Hint Rewrite @length_scmul @length_sub @length_opp : distr_length.

diff --git a/src/Arithmetic/SolinasReduction.v b/src/Arithmetic/SolinasReduction.v
@@ -1215,6 +1215,7 @@ Module SolinasReduction.
           eval weight (2 * n) (mul_no_reduce base n p q) =
             eval weight n p * Positional.eval weight n q.
       Proof using base_nz n_gt_1 wprops.
+        clear dependent s.
         intros p q.
         cbv [mul_no_reduce].
         break_match.
@@ -1260,6 +1261,7 @@ Module SolinasReduction.
       Theorem length_mul_no_reduce : forall p q,
           length (mul_no_reduce base n p q) = (2 * n)%nat.
       Proof using base_nz n_gt_1 wprops.
+        clear dependent s.
         intros; unfold mul_no_reduce; break_match; push.
       Qed.
       Hint Rewrite length_mul_no_reduce : push_length.
@@ -1322,6 +1324,7 @@ Module SolinasReduction.
             (combine (map weight (seq 0 n)) (firstn n p),
               (combine (map weight (seq 0 (m1 - n))) (skipn n p))).
       Proof using n_gt_1 wprops.
+        clear dependent s.
         intros m1 p ? ?.
         replace m1 with (n + (m1 - n))%nat at 1 by lia.
         rewrite <-(firstn_skipn n p) at 1.
@@ -2432,13 +2435,13 @@ Module SolinasReduction.
       Lemma sat_mul_comm (p q : list (Z * Z)) :
         Associational.eval (Associational.sat_mul base p q) =
           Associational.eval (Associational.sat_mul base q p).
-      Proof using base_nz n_gt_1. push; lia. Qed.
+      Proof using base_nz n_gt_1. clear dependent s. push; lia. Qed.
 
       Lemma sat_mul_distr (p q1 q2 : list (Z * Z)) :
         Associational.eval (Associational.sat_mul base p (q1 ++ q2)) =
           Associational.eval (Associational.sat_mul base p q1) +
             Associational.eval (Associational.sat_mul base p q2).
-      Proof using base_nz n_gt_1. push; lia. Qed.
+      Proof using base_nz n_gt_1. clear dependent s. push; lia. Qed.
 
       Lemma cons_to_app {A} a (p : list A) :
         a :: p = [a] ++ p.
@@ -2451,6 +2454,7 @@ Module SolinasReduction.
         eval weight m (fst (Rows.flatten' weight state inp)) =
           (Rows.eval weight m inp + eval weight m (fst state) + weight m * snd state) mod weight m.
       Proof using n_gt_1 wprops.
+        clear dependent s.
         intros.
         rewrite Rows.flatten'_correct with (n:=m) by auto.
         push.
@@ -2463,13 +2467,14 @@ Module SolinasReduction.
 
       Lemma sum_one x :
         sum [x] = x.
-      Proof. cbn; lia. Qed.
+      Proof. clear dependent s; cbn; lia. Qed.
 
       Lemma square_indiv_cons (p : list (Z * Z)) (a : Z * Z) :
         Associational.eval (sqr_indiv base (a :: p)) =
           Associational.eval (sqr_indiv base [a]) +
             Associational.eval (sqr_indiv base p).
       Proof using base_nz n_gt_1.
+        clear dependent s.
         cbv [sqr_indiv sqr_indiv'].
         cbn [fold_right].
         push.
@@ -2480,6 +2485,7 @@ Module SolinasReduction.
         Associational.eval (sqr_indiv base (p ++ q)) =
           Associational.eval (sqr_indiv base p) + Associational.eval (sqr_indiv base q).
       Proof using base_nz n_gt_1.
+        clear dependent s.
         generalize dependent q.
         induction p as [| a p IHp] using rev_ind; intros q.
         push.
@@ -2497,6 +2503,7 @@ Module SolinasReduction.
                                                                                   (Associational.eval (sat_mul base [(weight 2, x1)] [(weight 2, x1)]) +
                                                                                      Associational.eval (sat_mul base [(weight 3, x2)] [(weight 3, x2)])))).
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         intros x x0 x1 x2 q H.
         rewrite H.
         cbv [to_associational].
@@ -2519,6 +2526,7 @@ Module SolinasReduction.
         p = x :: x0 :: x1 :: x2 :: q ->
         length (square1 base (to_associational weight 4 p)) = 8%nat.
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         intros x x0 x1 x2 q H.
         cbv [square1].
         push.
@@ -2547,6 +2555,7 @@ Module SolinasReduction.
                  (Associational.eval (sat_mul base [(weight 3, x2)] [(weight 1, x0)]) +
                     Associational.eval (sat_mul base [(weight 3, x2)] [(weight 2, x1)]))).
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         intros x x0 x1 x2 q bound H H1.
         rewrite H1.
         cbv [to_associational].
@@ -2612,6 +2621,7 @@ Module SolinasReduction.
         p = x :: x0 :: x1 :: x2 :: q ->
         0 <= eval weight 8 (square1 base (to_associational weight 4 p)) < weight 7.
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         intros x x0 x1 x2 q bound H H0.
         erewrite eval_square1; [| eauto | eauto].
         rewrite H0 in H.
@@ -2635,6 +2645,7 @@ Module SolinasReduction.
       Theorem eval_square_no_reduce (p : list Z) :
         eval weight (2 * n) (square_no_reduce base n p) = (eval weight n p) * (eval weight n p).
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         rewrite <-eval_mul_no_reduce with (base:=base) by lia.
         cbv [square_no_reduce].
         break_match.
@@ -2729,6 +2740,7 @@ Module SolinasReduction.
       Theorem length_square_no_reduce (p : list Z):
         length (square_no_reduce base n p) = (2 * n)%nat.
       Proof using base_nz wprops n_gt_1.
+        clear dependent s.
         cbv [square_no_reduce].
         break_match.
         rewrite Nat.eqb_eq in Heqb.

diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v
@@ -1020,11 +1020,12 @@ Module WordByWordMontgomery.
       Qed.
       Lemma sub_bound : 0 <= eval (sub Av Bv) < eval N.
       Proof using small_Bv small_Av R_numlimbs_nz Bv_bound Av_bound small_N r_big' partition_Proper lgr_big N_nz N_lt_R.
+        clear dependent ri; clear dependent k.
         generalize eval_sub; break_innermost_match; Z.ltb_to_lt; lia.
       Qed.
       Lemma opp_bound : 0 <= eval (opp Av) < eval N.
       Proof using small_Av R_numlimbs_nz Av_bound small_N r_big' partition_Proper lgr_big N_nz N_lt_R.
-        clear Bv small_Bv Bv_bound.
+        clear Bv small_Bv Bv_bound k k_correct ri ri_correct.
         generalize eval_opp; break_innermost_match; Z.ltb_to_lt; lia.
       Qed.
     End add_sub.

diff --git a/src/Curves/TableMult/TableMult.v b/src/Curves/TableMult/TableMult.v
@@ -1243,7 +1243,7 @@ Section TableMult.
       intros.
       unfold positify.
       pose proof oddify_bounds e.
-      intuition.
+      intuition auto with core.
       - apply Z.div_pos; lia.
       - apply Z.div_lt_upper_bound; lia.
     Qed.

diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
@@ -58,6 +58,7 @@ Lemma x_nonneg: 0 <= x. Proof using prime_p x_id. clear -prime_p x_id. Z.prime_b
 
 Lemma x_id_inv : x = (p - 1) / 2.
 Proof using x_id.
+  clear neq_p_2.
   intros; apply Zeq_plus_swap in x_id.
   replace (p - 1) with (2 * ((p - 1) / 2)) in x_id by
     (symmetry; apply Z_div_exact_2; [lia | rewrite <- x_id; apply Z_mod_mult]).

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
@@ -1,17 +1,15 @@
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.SideConditions.CorePackages.
-Require Import Crypto.Util.SideConditions.ModInvPackage.
 Require Import Crypto.Util.SideConditions.ReductionPackages.
 Require Import Crypto.Util.SideConditions.RingPackage.
 
 Ltac autosolve_gen autosolve_tac ring_intros_tac else_tac :=
   CorePackages.preautosolve ();
   CorePackages.Internal.autosolve ltac:(fun _ =>
-  ModInvPackage.autosolve ltac:(fun _ =>
   ReductionPackages.autosolve autosolve_tac ltac:(fun _ =>
   RingPackage.autosolve_gen_intros ring_intros_tac ltac:(fun _ =>
   CorePackages.autosolve else_tac
-                                       )))).
+                                       ))).
 
 Ltac autosolve_gen_intros ring_intros_tac else_tac :=
   autosolve_gen ltac:(autosolve_gen_intros ring_intros_tac) ring_intros_tac else_tac.

diff --git a/src/Util/SideConditions/ModInvPackage.v b/src/Util/SideConditions/ModInvPackage.v
diff --git a/src/Util/ZUtil/ModInv.v b/src/Util/ZUtil/ModInv.v
diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v
 (** * Global Settings across the project *)

 (** Compatibility with 8.4 so we can write, e.g., [match p with
    ex_intro x y => _ end], rather than [match p with ex_intro _ x y
diff --git a/src/Util/IffT.v b/src/Util/IffT.v
 Require Import Coq.Classes.RelationClasses.
 Notation iffT A B := (((A -> B) * (B -> A)))%type.
 Notation iffTp := (fun A B => inhabited (iffT A B)).
	(** * Global Settings across the project *)
Check failure on line 1 in src/Util/GlobalSettings.v GitHub Actions / macos `src/Util/GlobalSettings.v`

	(** Compatibility with 8.4 so we can write, e.g., [match p with
	ex_intro x y => _ end], rather than [match p with ex_intro _ x y
	Require Import Coq.Classes.RelationClasses.
Check failure on line 1 in src/Util/IffT.v GitHub Actions / macos `src/Util/IffT.v`
	Notation iffT A B := (((A -> B) * (B -> A)))%type.
	Notation iffTp := (fun A B => inhabited (iffT A B)).