Merge remote-tracking branch 'upstream/master' into bounded-interface

6 files changed, 23 insertions, 5 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index fd144a474..000f2599c 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -636,7 +636,8 @@ Global Instance Proper_fold_chain {T} {Teq} {Teq_Equivalence : Equivalence Teq}
               ==> Teq) fold_chain.
 Proof.
   do 9 intro.
-  subst; induction y1; repeat intro; rewrite !fold_chain_equation.
+  subst; induction y1; repeat intro;
+    unfold fold_chain; fold @fold_chain.
   + inversion H; assumption || reflexivity.
   + destruct a.
     apply IHy1.
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 0ce214bbd..7158dc22a 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -1230,7 +1230,6 @@ Section Conversion.
     /\ Z.of_nat i <= bitsIn limb_widthsA
     /\ forall n, Z.testbit (decodeB out) n = if Z_lt_dec n (Z.of_nat i) then Z.testbit (decodeA inp) n else false.
 
-  Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end.
   Ltac subst_lia := subst_let; subst; lia.
 
   Lemma convert'_bounded_step : forall inp i out,
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 1c39f22cb..2fd9befa0 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1340,6 +1340,7 @@ Proof.
 induction n; destruct l; boring.
 apply nth_error_nil_error.
 Qed.
+Hint Rewrite @nth_error_skipn : push_nth_error.
 
 Lemma nth_default_skipn : forall {A} (l : list A) d n m, nth_default d (skipn n l) m = nth_default d l (n + m).
 Proof.
@@ -1347,6 +1348,7 @@ cbv [nth_default]; intros.
 rewrite nth_error_skipn.
 reflexivity.
 Qed.
+Hint Rewrite @nth_default_skipn : push_nth_default.
 
 Lemma sum_firstn_skipn : forall l n m, sum_firstn l (n + m) = (sum_firstn l n + sum_firstn (skipn n l) m)%Z.
 Proof.
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 5daa2d4a9..686443829 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -25,6 +25,8 @@ Reserved Infix "&" (at level 50). (* N.B. This conflicts with [{ a : T & P}] for
 Reserved Infix "∣" (at level 50).
 Reserved Infix "~=" (at level 70).
 Reserved Infix "==" (at level 70, no associativity).
+Reserved Infix "=~>" (at level 70, no associativity).
+Reserved Infix "<~=" (at level 70, no associativity).
 Reserved Infix "≡" (at level 70, no associativity).
 Reserved Infix "≢" (at level 70, no associativity).
 Reserved Infix "≡_n" (at level 70, no associativity).
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index be777512c..cee2fc2a1 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -61,6 +61,8 @@ Ltac subst_evars :=
          | [ e := ?E |- _ ] => is_evar E; subst e
          end.
 
+Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end.
+
 (** destruct discriminees of [match]es in the goal *)
 (* Prioritize breaking apart things in the context, then things which
    don't need equations, then simple matches (which can be displayed
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index d06477d3c..1758f1496 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -19,7 +19,7 @@ Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
 Hint Extern 1 => omega : omega.
-Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound : zarith.
+Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos : zarith.
 Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
 
 Ltac zutil_arith := solve [ omega | lia | auto with nocore ].
@@ -324,15 +324,27 @@ Module Z.
 
   Hint Resolve elim_mod : zarith.
 
+  Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c.
+  Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add_full : zsimplify.
+
+  Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b.
+  Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add_l_full : zsimplify.
+
+  Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b.
+  Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a.
+  Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify.
+
   Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
   Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
-  Hint Rewrite mod_add_l using zutil_arith : zsimplify.
 
   Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b.
   Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
   Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a.
   Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
-  Hint Rewrite mod_add' mod_add_l' using zutil_arith : zsimplify.
 
   Lemma pos_pow_nat_pos : forall x n,
     Z.pos x ^ Z.of_nat n > 0.