aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject1
-rw-r--r--src/Util/ZRange/BasicLemmas.v7
-rw-r--r--src/Util/ZRange/LandLorBounds.v159
-rw-r--r--src/Util/ZRange/Operations.v12
-rw-r--r--src/Util/ZUtil/Definitions.v1
-rw-r--r--src/Util/ZUtil/LandLorBounds.v236
-rw-r--r--src/Util/ZUtil/LandLorShiftBounds.v41
-rw-r--r--src/Util/ZUtil/Modulo.v11
-rw-r--r--src/Util/ZUtil/Ones.v38
-rw-r--r--src/Util/ZUtil/Tactics/LinearSubstitute.v8
-rw-r--r--src/Util/ZUtil/ZSimplify/Core.v10
-rw-r--r--src/Util/ZUtil/ZSimplify/Simple.v3
12 files changed, 470 insertions, 57 deletions
diff --git a/_CoqProject b/_CoqProject
index 72b6eed1a..83cde8a3c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6604,6 +6604,7 @@ src/Util/Tactics/UniquePose.v
src/Util/Tactics/VM.v
src/Util/ZRange/BasicLemmas.v
src/Util/ZRange/CornersMonotoneBounds.v
+src/Util/ZRange/LandLorBounds.v
src/Util/ZRange/Operations.v
src/Util/ZRange/Show.v
src/Util/ZRange/SplitBounds.v
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 6cfdaaff8..4bdcb19ef 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -71,6 +71,9 @@ Module ZRange.
| progress specialize_by omega
| progress destruct_head'_or ].
+ Lemma is_tighter_than_bool_extend_land_lor_bounds r : is_tighter_than_bool r (extend_land_lor_bounds r) = true.
+ Proof. repeat t2_step. Qed.
+
Lemma is_bounded_by_iff_is_tighter_than r1 r2
: (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true)
<-> (is_tighter_than_bool r1 r2 = true \/ goodb r1 = false).
@@ -92,6 +95,10 @@ Module ZRange.
rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption.
Qed.
+ Lemma is_bounded_by_of_is_tighter_than r1 r2 (H : is_tighter_than_bool r1 r2 = true)
+ : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true).
+ Proof. apply is_bounded_by_iff_is_tighter_than; auto. Qed.
+
Lemma is_bounded_by_bool_Proper_if_sumbool_union_dep {A B} (b : sumbool A B) x y rx ry
: (A -> is_bounded_by_bool x rx = true)
-> (B -> is_bounded_by_bool y ry = true)
diff --git a/src/Util/ZRange/LandLorBounds.v b/src/Util/ZRange/LandLorBounds.v
new file mode 100644
index 000000000..dd538d967
--- /dev/null
+++ b/src/Util/ZRange/LandLorBounds.v
@@ -0,0 +1,159 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.LandLorBounds.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZRange.BasicLemmas.
+Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+Local Open Scope bool_scope.
+Local Open Scope Z_scope.
+
+Module ZRange.
+ Import Operations.ZRange.
+ Import CornersMonotoneBounds.ZRange.
+
+ Lemma is_bounded_by_bool_lor_land_bound_helper
+ f (Hf : f = Z.lor \/ f = Z.land)
+ x x_bs y y_bs
+ (Hboundedx : is_bounded_by_bool x x_bs = true)
+ (Hboundedy : is_bounded_by_bool y y_bs = true)
+ : is_tighter_than_bool
+ (constant (f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)))
+ (four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y)) x_bs y_bs)
+ = true.
+ Proof.
+ apply monotoneb_four_corners_and_zero_gen with (x:=x) (y:=y);
+ destruct_head'_or; subst f; eauto with typeclass_instances zarith core.
+ Qed.
+
+ Local Existing Instances Z.land_round_Proper_pos_r
+ Z.land_round_Proper_pos_l
+ Z.lor_round_Proper_pos_r
+ Z.lor_round_Proper_pos_l
+ Z.land_round_Proper_neg_r
+ Z.land_round_Proper_neg_l
+ Z.lor_round_Proper_neg_r
+ Z.lor_round_Proper_neg_l.
+
+ Lemma is_bounded_by_bool_land_lor_bounds_helper
+ f (Hf : f = Z.lor \/ f = Z.land)
+ x x_bs y y_bs
+ (Hboundedx : is_bounded_by_bool x x_bs = true)
+ (Hboundedy : is_bounded_by_bool y y_bs = true)
+ : is_bounded_by_bool (f x y) (land_lor_bounds f x_bs y_bs) = true.
+ Proof.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs)) as H.
+ pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as H0x.
+ pose proof (fun pf1 pf2 => is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) y (extend_land_lor_bounds y_bs) pf2 pf1) as Hm1x.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H0y.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf x (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1y.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as H00.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) 0 (extend_land_lor_bounds y_bs)) as Hm10.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf 0 (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as H0m1.
+ pose proof (is_bounded_by_bool_lor_land_bound_helper f Hf (-1) (extend_land_lor_bounds x_bs) (-1) (extend_land_lor_bounds y_bs)) as Hm1m1.
+ specialize_by (eapply ZRange.is_bounded_by_of_is_tighter_than; try eapply ZRange.is_tighter_than_bool_extend_land_lor_bounds; eassumption || reflexivity).
+ revert H H0x Hm1x H0y Hm1y H00 Hm1m1 H0m1 Hm10.
+ cbv [land_lor_bounds constant is_tighter_than_bool is_bounded_by_bool is_true] in *; cbn [lower upper] in *.
+ rewrite !Bool.andb_true_iff, !Z.leb_le in *.
+ cbv [extend_land_lor_bounds].
+ cbn [lower upper] in *.
+ destruct (Z.round_lor_land_bound_bounds x) as [Hx|Hx], (Z.round_lor_land_bound_bounds y) as [Hy|Hy].
+ all: repeat apply Z.min_case_strong; repeat apply Z.max_case_strong.
+ all: try (intros; exfalso; clear dependent f; lia).
+ all: destruct x as [|x|x], y as [|y|y]; try (intros; exfalso; clear dependent f; lia).
+ all: change (Z.round_lor_land_bound 0) with 0 in *.
+ all: change (Z.round_lor_land_bound (-1)) with (-1) in *.
+ all: intros.
+ all: repeat match goal with
+ | _ => assumption
+ | [ H : ?T, H' : ?T |- _ ] => clear H'
+ | [ H : 0 <= 0 <= 0 |- _ ] => clear H
+ | [ H : 0 <= -1 <= _ -> _ |- _ ] => clear H
+ | [ H : 0 <= -1 -> _ |- _ ] => clear H
+ | [ H : ?x <= ?x <= _ -> _ |- _ ] => specialize (fun pf => H (conj (@Z.le_refl x) pf))
+ | [ H : _ <= ?x <= ?x -> _ |- _ ] => specialize (fun pf => H (conj pf (@Z.le_refl x)))
+ | [ H : ?T, H' : ?T /\ _ -> _ |- _ ] => specialize (fun pf => H' (conj H pf))
+ | [ H : ?T, H' : _ /\ ?T -> _ |- _ ] => specialize (fun pf => H' (conj pf H))
+ | _ => progress specialize_by_assumption
+ | _ => progress specialize_by (destruct_head'_and; assumption)
+ | [ H : _ <= Z.pos _ <= ?x |- _ ] => unique assert (0 <= x) by (clear -H; lia)
+ | [ H : ?x <= Z.neg _ <= _ |- _ ] => unique assert (x <= -1) by (clear -H; lia)
+ | [ H : ?a <= _ <= ?c, H' : ?c <= ?d, H'' : ?a <= ?d -> _ |- _ ]
+ => unique assert (a <= d) by (clear -H H'; lia)
+ | [ H : ?a <= ?b -> ?c <= ?d <= ?e -> _ |- _ ] => specialize (fun pf1 pf2 => H pf2 pf1)
+ end.
+ all: destruct Hf; subst f.
+ all: split.
+ all: destruct_head'_and.
+ all: split_and.
+ all: repeat lazymatch goal with
+ | [ |- Z.land _ (Z.pos ?x) <= _ ]
+ => is_var x; etransitivity; [ apply Z.land_round_bound_pos_r' | ]
+ | [ |- Z.land (Z.pos ?x) _ <= _ ]
+ => is_var x; etransitivity; [ apply Z.land_round_bound_pos_l' | ]
+ | [ |- _ <= Z.land _ (Z.pos ?x) ]
+ => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_r ]
+ | [ |- _ <= Z.land (Z.pos ?x) _ ]
+ => is_var x; etransitivity; [ | apply Z.land_round_bound_pos_l ]
+ | [ |- Z.land _ (Z.neg ?x) <= _ ]
+ => is_var x; etransitivity; [ apply Z.land_round_bound_neg_r | ]
+ | [ |- Z.land (Z.neg ?x) _ <= _ ]
+ => is_var x; etransitivity; [ apply Z.land_round_bound_neg_l | ]
+ | [ |- _ <= Z.land _ (Z.neg ?x) ]
+ => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_r' ]
+ | [ |- _ <= Z.land (Z.neg ?x) _ ]
+ => is_var x; etransitivity; [ | apply Z.land_round_bound_neg_l' ]
+ | [ |- Z.lor _ (Z.pos ?x) <= _ ]
+ => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_r' | ]
+ | [ |- Z.lor (Z.pos ?x) _ <= _ ]
+ => is_var x; etransitivity; [ apply Z.lor_round_bound_pos_l' | ]
+ | [ |- _ <= Z.lor _ (Z.pos ?x) ]
+ => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_r ]
+ | [ |- _ <= Z.lor (Z.pos ?x) _ ]
+ => is_var x; etransitivity; [ | apply Z.lor_round_bound_pos_l ]
+ | [ |- Z.lor _ (Z.neg ?x) <= _ ]
+ => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_r | ]
+ | [ |- Z.lor (Z.neg ?x) _ <= _ ]
+ => is_var x; etransitivity; [ apply Z.lor_round_bound_neg_l | ]
+ | [ |- _ <= Z.lor _ (Z.neg ?x) ]
+ => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_r' ]
+ | [ |- _ <= Z.lor (Z.neg ?x) _ ]
+ => is_var x; etransitivity; [ | apply Z.lor_round_bound_neg_l' ]
+ | [ |- Z.pos ?x <= _ ]
+ => is_var x; etransitivity; [ eassumption | ]
+ | [ |- _ <= Z.neg ?x ]
+ => is_var x; etransitivity; [ | eassumption ]
+ | [ |- _ <= Z.pos ?x ]
+ => is_var x; transitivity 0; [ assumption | lia ]
+ | [ |- Z.neg ?x <= _ ]
+ => is_var x; transitivity (-1); [ lia | assumption ]
+ | _ => idtac
+ end.
+ all: try assumption.
+ all: try (rewrite ?Z.lor_0_l, ?Z.lor_0_r, ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_m1_l, ?Z.lor_m1_r, ?Z.land_m1_l, ?Z.land_m1_r in *; reflexivity || assumption).
+ Qed.
+
+ Lemma is_bounded_by_bool_land_bounds
+ x x_bs y y_bs
+ (Hboundedx : is_bounded_by_bool x x_bs = true)
+ (Hboundedy : is_bounded_by_bool y y_bs = true)
+ : is_bounded_by_bool (Z.land x y) (ZRange.land_bounds x_bs y_bs) = true.
+ Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed.
+
+ Lemma is_bounded_by_bool_lor_bounds
+ x x_bs y y_bs
+ (Hboundedx : is_bounded_by_bool x x_bs = true)
+ (Hboundedy : is_bounded_by_bool y y_bs = true)
+ : is_bounded_by_bool (Z.lor x y) (ZRange.lor_bounds x_bs y_bs) = true.
+ Proof. apply is_bounded_by_bool_land_lor_bounds_helper; auto. Qed.
+End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 130fdc0c4..c6f209e16 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -145,13 +145,13 @@ Module ZRange.
rewrite Z.max_comm; reflexivity.
Qed.
- (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
- Definition round_lor_land_bound (x : BinInt.Z) : BinInt.Z
- := if (0 <=? x)%Z
- then 2^(Z.log2_up (x+1))-1
- else -2^(Z.log2_up (-x)).
+ Definition extend_land_lor_bounds (v : zrange) : zrange
+ := let (l, u) := eta v in
+ r[ Z.min 0 l ~> Z.max (-1) u ].
+
Definition land_lor_bounds (f : BinInt.Z -> BinInt.Z -> BinInt.Z) (x y : zrange) : zrange
- := four_corners_and_zero (fun x y => f (round_lor_land_bound x) (round_lor_land_bound y)) x y.
+ := four_corners_and_zero (fun x y => f (Z.round_lor_land_bound x) (Z.round_lor_land_bound y))
+ (extend_land_lor_bounds x) (extend_land_lor_bounds y).
Definition land_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.land.
Definition lor_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.lor.
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 4ef6b5403..8fe5772f5 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -85,6 +85,7 @@ Module Z.
then mul_split_at_bitwidth (Z.log2 s) x y
else ((x * y) mod s, (x * y) / s).
+ (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
Definition round_lor_land_bound (x : Z) : Z
:= if (0 <=? x)%Z
then 2^(Z.log2_up (x+1))-1
diff --git a/src/Util/ZUtil/LandLorBounds.v b/src/Util/ZUtil/LandLorBounds.v
index 1b10ecf97..78866ec7f 100644
--- a/src/Util/ZUtil/LandLorBounds.v
+++ b/src/Util/ZUtil/LandLorBounds.v
@@ -3,8 +3,17 @@ Require Import Coq.ZArith.ZArith.
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Pow2.
+Require Import Crypto.Util.ZUtil.Log2.
Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Modulo.
Require Import Crypto.Util.ZUtil.Ones.
Require Import Crypto.Util.ZUtil.Lnot.
Require Import Crypto.Util.ZUtil.Land.
@@ -14,10 +23,34 @@ Require Import Crypto.Util.Tactics.BreakMatch.
Local Open Scope Z_scope.
Module Z.
+ Lemma round_lor_land_bound_bounds x
+ : (0 <= x <= Z.round_lor_land_bound x) \/ (Z.round_lor_land_bound x <= x <= -1).
+ Proof.
+ cbv [Z.round_lor_land_bound]; break_innermost_match; Z.ltb_to_lt.
+ all: constructor; split; try lia; [].
+ all: Z.replace_all_neg_with_pos.
+ all: match goal with |- context[2^Z.log2_up ?x] => pose proof (Z.log2_up_le_full x) end.
+ all: lia.
+ Qed.
+ Hint Resolve round_lor_land_bound_bounds : zarith.
+
+ Lemma round_lor_land_bound_bounds_pos x
+ : (0 <= Z.pos x <= Z.round_lor_land_bound (Z.pos x)).
+ Proof. generalize (round_lor_land_bound_bounds (Z.pos x)); lia. Qed.
+ Hint Resolve round_lor_land_bound_bounds_pos : zarith.
+
+ Lemma round_lor_land_bound_bounds_neg x
+ : Z.round_lor_land_bound (Z.neg x) <= Z.neg x <= -1.
+ Proof. generalize (round_lor_land_bound_bounds (Z.neg x)); lia. Qed.
+ Hint Resolve round_lor_land_bound_bounds_neg : zarith.
+
Local Ltac saturate :=
repeat first [ progress cbv [Z.round_lor_land_bound Proper respectful Basics.flip] in *
- | progress cbn in *
+ | progress Z.ltb_to_lt
| progress intros
+ | break_innermost_match_step
+ | lia
+ | rewrite !Pos2Z.opp_neg
| match goal with
| [ |- context[Z.log2_up ?x] ]
=> unique pose proof (Z.log2_up_nonneg x)
@@ -29,13 +62,18 @@ Module Z.
=> unique assert (Z.pos x <= Z.pos y) by lia
| [ H : Pos.le ?x ?y |- context[Z.pos (?x+1)] ]
=> unique assert (Z.pos (x+1) <= Z.pos (y+1)) by lia
+ | [ H : Z.le ?x ?y |- context[?x+1] ]
+ => unique assert (x+1 <= y+1) by lia
| [ H : Z.le ?x ?y |- context[2^Z.log2_up ?x] ]
=> unique assert (2^Z.log2_up x <= 2^Z.log2_up y) by (Z.peel_le; lia)
+ | [ H : ?a^?b <= ?a^?c |- _ ]
+ => unique assert (a^(c-b) = a^c/a^b) by auto with zarith;
+ unique assert (a^c mod a^b = 0) by auto with zarith
end ].
Local Ltac do_rewrites_step :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
- | [ |- context[Z.land (-2^_) (-2^_)] ]
+ (*| [ |- context[Z.land (-2^_) (-2^_)] ]
=> rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_lor, !Z.lor_ones_ones, !Z.lnot_ones_equiv
| [ |- context[Z.lor (-2^_) (-2^_)] ]
=> rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_land, !Z.land_ones_ones, !Z.lnot_ones_equiv
@@ -52,8 +90,45 @@ Module Z.
| [ |- context[Z.lor (-2^?x) (2^?y-1)] ]
=> rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive (2^y-1)), <- !Z.lnot_land, ?Z.lnot_ones_equiv, (Z.lnot_sub1 (2^y)), !Z.ones_equiv, ?Z.lnot_equiv, <- !Z.sub_1_r
| [ |- context[-?x mod ?y] ]
- => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod
- | [ H : ?x <= ?x |- _ ] => clear H
+ => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod*)
+ | [ |- context[Z.land (2^?y-1) ?x] ]
+ => is_var x; rewrite (Z.land_comm (2^y-1) x)
+ | [ |- context[Z.lor (2^?y-1) ?x] ]
+ => is_var x; rewrite (Z.lor_comm (2^y-1) x)
+ | [ |- context[Z.land (-2^?y) ?x] ]
+ => is_var x; rewrite (Z.land_comm (-2^y) x)
+ | [ |- context[Z.lor (-2^?y) ?x] ]
+ => is_var x; rewrite (Z.lor_comm (-2^y) x)
+ | [ |- context[Z.land _ (2^_-1)] ]
+ => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones by auto with zarith
+ | [ |- context[Z.land ?x (-2^?y)] ]
+ => is_var x;
+ rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_lor, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r;
+ let x' := fresh in
+ remember (-x-1) as x' eqn:?; Z.linear_substitute x;
+ rename x' into x
+ | [ |- context[Z.lor ?x (-2^?y)] ]
+ => is_var x;
+ rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive x), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r;
+ let x' := fresh in
+ remember (-x-1) as x' eqn:?; Z.linear_substitute x;
+ rename x' into x
+ | [ |- Z.lor ?x (?y-1) <= Z.lor ?x (?y'-1) ]
+ => rewrite (Z.div_mod'' (Z.lor x (y-1)) y), (Z.div_mod'' (Z.lor x (y'-1)) y') by auto with zarith
+ | [ |- Z.lor ?x (?y-1) = _ ]
+ => rewrite (Z.div_mod'' (Z.lor x (y-1)) y) by auto with zarith
+ | [ |- context[?m1 - 1 + (?x - ?x mod ?m1)] ]
+ => replace (m1 - 1 + (x - x mod m1)) with ((m1 - x mod m1) + (x - 1)) by lia
+ | _ => progress rewrite ?Z.lor_pow2_div_pow2_r, ?Z.lor_pow2_div_pow2_l, ?Z.lor_pow2_mod_pow2_r, ?Z.lor_pow2_mod_pow2_l by auto with zarith
+ | _ => rewrite !Z.mul_div_eq by lia
+ | _ => progress rewrite ?(Z.add_comm 1) in *
+ | [ |- context[?x mod 2^(Z.log2_up (?x + 1))] ]
+ => rewrite (Z.mod_small x (2^Z.log2_up (x+1))) by (rewrite <- Z.le_succ_l, <- Z.add_1_r, Z.log2_up_le_pow2 by lia; lia)
+ | [ H : ?a^?b <= ?a^?c |- context[?x mod ?a^?b] ]
+ => rewrite (@Z.mod_pow_r_split x a b c) by auto with zarith;
+ (Z.div_mod_to_quot_rem; nia)
+ | _ => progress Z.peel_le
+ (*| [ H : ?x <= ?x |- _ ] => clear H
| [ H : ?x < ?y, H' : ?y <= ?z |- _ ] => unique assert (x < z) by lia
| [ H : ?x < ?y, H' : ?a <= ?x |- _ ] => unique assert (a < y) by lia
| [ H : 2^?x < 2^?y |- context[2^?x mod 2^?y] ]
@@ -65,8 +140,15 @@ Module Z.
destruct (@Z.pow2_lt_or_divides x y ltac:(lia)) as [H|H];
[ repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia
| rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ]
- | rewrite H ]
- | _ => progress autorewrite with zsimplify_const
+ | rewrite H ]*)
+ | _ => progress autorewrite with zsimplify_fast in *
+ | [ |- context[-(-?x-1)] ] => replace (-(-x-1)) with (1+x) by lia
+ | [ H : 0 > -(1+?x) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H
+ | [ H : 0 > -(?x+1) |- _ ] => assert (0 <= x) by (clear -H; lia); clear H
+ | [ |- ?a - ?b = ?a' - ?b' ] => apply f_equal2; try reflexivity; []
+ | [ |- -?a = -?a' ] => apply f_equal
+ | _ => rewrite <- !Z.sub_1_r
+ | _ => lia
end.
Local Ltac do_rewrites := repeat do_rewrites_step.
Local Ltac fin_t :=
@@ -80,53 +162,129 @@ Module Z.
| lia
| progress Z.peel_le ].
Local Ltac t :=
- saturate; do_rewrites; fin_t.
+ saturate; do_rewrites.
Local Instance land_round_Proper_pos_r x
- : Proper (Pos.le ==> Z.le)
- (fun y =>
- Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))).
- Proof. destruct x; t. Qed.
+ : Proper (Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.pos y))).
+ Proof. t. Qed.
Local Instance land_round_Proper_pos_l y
- : Proper (Pos.le ==> Z.le)
- (fun x =>
- Z.land (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)).
- Proof. destruct y; t. Qed.
+ : Proper (Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.pos x)) y).
+ Proof. t. Qed.
Local Instance lor_round_Proper_pos_r x
- : Proper (Pos.le ==> Z.le)
- (fun y =>
- Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))).
- Proof. destruct x; t. Qed.
+ : Proper (Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.pos y))).
+ Proof. t. Qed.
Local Instance lor_round_Proper_pos_l y
- : Proper (Pos.le ==> Z.le)
- (fun x =>
- Z.lor (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)).
- Proof. destruct y; t. Qed.
+ : Proper (Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.pos x)) y).
+ Proof. t. Qed.
Local Instance land_round_Proper_neg_r x
- : Proper (Basics.flip Pos.le ==> Z.le)
- (fun y =>
- Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))).
- Proof. destruct x; t. Qed.
+ : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.land x (Z.round_lor_land_bound (Z.neg y))).
+ Proof. t. Qed.
Local Instance land_round_Proper_neg_l y
- : Proper (Basics.flip Pos.le ==> Z.le)
- (fun x =>
- Z.land (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)).
- Proof. destruct y; t. Qed.
+ : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.land (Z.round_lor_land_bound (Z.neg x)) y).
+ Proof. t. Qed.
Local Instance lor_round_Proper_neg_r x
- : Proper (Basics.flip Pos.le ==> Z.le)
- (fun y =>
- Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))).
- Proof. destruct x; t. Qed.
+ : Proper (Basics.flip Pos.le ==> Z.le) (fun y => Z.lor x (Z.round_lor_land_bound (Z.neg y))).
+ Proof. t. Qed.
Local Instance lor_round_Proper_neg_l y
- : Proper (Basics.flip Pos.le ==> Z.le)
- (fun x =>
- Z.lor (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)).
- Proof. destruct y; t. Qed.
+ : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.lor (Z.round_lor_land_bound (Z.neg x)) y).
+ Proof. t. Qed.
+
+ Lemma land_round_lor_land_bound_r x
+ : Z.land x (Z.round_lor_land_bound x) = if (0 <=? x) then x else Z.round_lor_land_bound x.
+ Proof. t. Qed.
+ Hint Rewrite land_round_lor_land_bound_r : zsimplify_fast zsimplify.
+ Lemma land_round_lor_land_bound_l x
+ : Z.land (Z.round_lor_land_bound x) x = if (0 <=? x) then x else Z.round_lor_land_bound x.
+ Proof. rewrite Z.land_comm, land_round_lor_land_bound_r; reflexivity. Qed.
+ Hint Rewrite land_round_lor_land_bound_l : zsimplify_fast zsimplify.
+
+ Lemma lor_round_lor_land_bound_r x
+ : Z.lor x (Z.round_lor_land_bound x) = if (0 <=? x) then Z.round_lor_land_bound x else x.
+ Proof. t. Qed.
+ Hint Rewrite lor_round_lor_land_bound_r : zsimplify_fast zsimplify.
+ Lemma lor_round_lor_land_bound_l x
+ : Z.lor (Z.round_lor_land_bound x) x = if (0 <=? x) then Z.round_lor_land_bound x else x.
+ Proof. rewrite Z.lor_comm, lor_round_lor_land_bound_r; reflexivity. Qed.
+ Hint Rewrite lor_round_lor_land_bound_l : zsimplify_fast zsimplify.
+
+ Lemma land_round_bound_pos_r v x
+ : 0 <= Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)).
+ Proof.
+ rewrite Z.land_nonneg; split; [ lia | ].
+ replace (Z.pos x) with (Z.land (Z.pos x) (Z.round_lor_land_bound (Z.pos x))) at 1
+ by now rewrite land_round_lor_land_bound_r.
+ rewrite (Z.land_comm (Z.pos x)), Z.land_assoc.
+ apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
+ Qed.
+ Hint Resolve land_round_bound_pos_r (fun v x => proj1 (land_round_bound_pos_r v x)) (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
+ Lemma land_round_bound_pos_l v x
+ : 0 <= Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v.
+ Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_pos_r. Qed.
+ Hint Resolve land_round_bound_pos_l (fun v x => proj1 (land_round_bound_pos_l v x)) (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.
+
+ Lemma land_round_bound_neg_r v x
+ : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x) <= v.
+ Proof.
+ assert (0 < 2 ^ Z.log2_up (Z.pos x)) by auto with zarith.
+ split; [ | apply Z.land_le; lia ].
+ replace (Z.round_lor_land_bound (Z.neg x)) with (Z.land (Z.neg x) (Z.round_lor_land_bound (Z.neg x)))
+ by now rewrite land_round_lor_land_bound_r.
+ rewrite !Z.land_assoc.
+ etransitivity; [ apply Z.land_le; cbn; lia | ]; lia.
+ Qed.
+ Hint Resolve land_round_bound_neg_r (fun v x => proj1 (land_round_bound_neg_r v x)) (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
+ Lemma land_round_bound_neg_l v x
+ : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v <= v.
+ Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_neg_r. Qed.
+ Hint Resolve land_round_bound_neg_l (fun v x => proj1 (land_round_bound_neg_l v x)) (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.
+
+ Lemma lor_round_bound_neg_r v x
+ : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x) <= -1.
+ Proof.
+ change (-1) with (Z.pred 0); rewrite <- Z.lt_le_pred.
+ rewrite Z.lor_neg; split; [ | lia ].
+ replace (Z.neg x) with (Z.lor (Z.neg x) (Z.round_lor_land_bound (Z.neg x))) at 2
+ by now rewrite lor_round_lor_land_bound_r.
+ rewrite (Z.lor_comm (Z.neg x)), Z.lor_assoc.
+ cbn; rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive v), <- (Z.lnot_involutive (Z.neg x)), <- !Z.lnot_land, !Z.ones_equiv, !Z.lnot_equiv, <- !Z.sub_1_r, !Pos2Z.opp_neg.
+ Z.peel_le.
+ apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
+ Qed.
+ Hint Resolve lor_round_bound_neg_r (fun v x => proj1 (lor_round_bound_neg_r v x)) (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
+ Lemma lor_round_bound_neg_l v x
+ : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v <= -1.
+ Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_neg_r. Qed.
+ Hint Resolve lor_round_bound_neg_l (fun v x => proj1 (lor_round_bound_neg_l v x)) (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.
+
+ Lemma lor_round_bound_pos_r v x
+ : v <= Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)).
+ Proof.
+ assert (0 < 2 ^ Z.log2_up (Z.pos (x + 1))) by auto with zarith.
+ split; [ apply Z.lor_lower; lia | ].
+ replace (Z.round_lor_land_bound (Z.pos x)) with (Z.lor (Z.pos x) (Z.round_lor_land_bound (Z.pos x)))
+ by now rewrite lor_round_lor_land_bound_r.
+ rewrite !Z.lor_assoc.
+ etransitivity; [ | apply Z.lor_lower; rewrite ?Z.lor_nonneg; cbn; lia ]; lia.
+ Qed.
+ Hint Resolve lor_round_bound_pos_r (fun v x => proj1 (lor_round_bound_pos_r v x)) (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
+ Lemma lor_round_bound_pos_l v x
+ : v <= Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v.
+ Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_pos_r. Qed.
+ Hint Resolve lor_round_bound_pos_l (fun v x => proj1 (lor_round_bound_pos_l v x)) (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.
+
+ Lemma land_round_bound_pos_r' v x : Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
+ Lemma land_round_bound_pos_l' v x : Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.
+ Lemma land_round_bound_neg_r' v x : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x). Proof. auto with zarith. Qed.
+ Lemma land_round_bound_neg_l' v x : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v. Proof. auto with zarith. Qed.
+ Lemma lor_round_bound_neg_r' v x : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x). Proof. auto with zarith. Qed.
+ Lemma lor_round_bound_neg_l' v x : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v. Proof. auto with zarith. Qed.
+ Lemma lor_round_bound_pos_r' v x : Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
+ Lemma lor_round_bound_pos_l' v x : Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.
End Z.
diff --git a/src/Util/ZUtil/LandLorShiftBounds.v b/src/Util/ZUtil/LandLorShiftBounds.v
index e978ab6b0..a8e0b2051 100644
--- a/src/Util/ZUtil/LandLorShiftBounds.v
+++ b/src/Util/ZUtil/LandLorShiftBounds.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.Testbit.
Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
Require Import Crypto.Util.NUtil.WithoutReferenceToZ.
Local Open Scope Z_scope.
@@ -70,7 +71,7 @@ Module Z.
Qed.
Section ZInequalities.
- Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
+ Lemma land_le' : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
Proof.
intros x y H; apply Z.ldiff_le; [assumption|].
rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc.
@@ -79,14 +80,38 @@ Module Z.
reflexivity.
Qed.
- Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z.
+ Lemma lor_lower : forall x y, (0 <= x -> 0 <= y)%Z -> (x <= Z.lor x y)%Z.
Proof.
- intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
- rewrite Z.ldiff_land.
- apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
- rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
- [|apply Z.ge_le; assumption].
- induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity.
+ intros x y H.
+ destruct (Z_lt_le_dec x 0).
+ { Z.replace_all_neg_with_pos.
+ replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia).
+ rewrite <- (Z.lnot_involutive y).
+ rewrite <- Z.lnot_land.
+ cbv [Z.lnot].
+ rewrite <- !Z.sub_1_r.
+ Z.peel_le.
+ apply land_le'; lia. }
+ { apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
+ rewrite Z.ldiff_land.
+ apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
+ rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
+ [|apply Z.ge_le; assumption].
+ induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. }
+ Qed.
+
+ Lemma land_le : forall x y, (0 <= y -> 0 <= x)%Z -> (Z.land x y <= x)%Z.
+ Proof.
+ intros x y H.
+ destruct (Z_lt_le_dec y 0), (Z_lt_le_dec x 0); auto using land_le' with lia.
+ Z.replace_all_neg_with_pos.
+ replace (-x) with (Z.lnot (x - 1)) by (cbv [Z.pred Z.lnot]; lia).
+ replace (-y) with (Z.lnot (y - 1)) by (cbv [Z.pred Z.lnot]; lia).
+ rewrite <- Z.lnot_lor.
+ cbv [Z.lnot].
+ rewrite <- !Z.sub_1_r.
+ Z.peel_le.
+ apply lor_lower; lia.
Qed.
Lemma lor_le : forall x y z,
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 567d106e3..9944c8124 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -297,6 +297,7 @@ Module Z.
apply Z_mod_mult.
Qed.
Hint Rewrite mod_same_pow using zutil_arith : zsimplify.
+ Hint Resolve mod_same_pow : zarith.
Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0.
Proof.
@@ -369,4 +370,14 @@ Module Z.
apply Z.mod_small.
omega.
Qed.
+
+ Lemma mod_pow_r_split x b e1 e2 : 0 <= b -> 0 <= e1 <= e2 -> x mod b^e2 = (x mod b^e1) + (b^e1) * ((x / b^e1) mod b^(e2-e1)).
+ Proof.
+ destruct (Z_zerop b).
+ { destruct (Z_zerop e1), (Z_zerop e2), (Z.eq_dec e1 e2); subst; intros; cbn; autorewrite with zsimplify_fast; lia. }
+ intros.
+ replace (b^e2) with (b^e1 * b^(e2 - e1)) by (autorewrite with pull_Zpow; f_equal; lia).
+ rewrite Z.rem_mul_r by auto with zarith.
+ reflexivity.
+ Qed.
End Z.
diff --git a/src/Util/ZUtil/Ones.v b/src/Util/ZUtil/Ones.v
index e856f23a0..37a0d184e 100644
--- a/src/Util/ZUtil/Ones.v
+++ b/src/Util/ZUtil/Ones.v
@@ -174,4 +174,42 @@ Module Z.
end ].
Qed.
Hint Rewrite lor_ones_ones : zsimplify.
+
+ Lemma lor_pow2_mod_pow2_r x e (He : 0 <= e) : Z.lor x (2^e-1) mod (2^e) = 2^e-1.
+ Proof.
+ destruct (Z_zerop e).
+ { subst; autorewrite with zsimplify_const; reflexivity. }
+ assert (0 <= x mod 2^e < 2^e) by auto with zarith.
+ assert (0 <= x mod 2^e <= 2^e-1) by lia.
+ assert (Z.log2 (x mod 2^e) <= Z.log2 (2^e-1)) by (apply Z.log2_le_mono; lia).
+ assert (Z.log2 (x mod 2^e) < e) by (rewrite Z.sub_1_r, Z.log2_pred_pow2 in * by lia; lia).
+ rewrite <- Z.land_ones, Z.land_lor_distr_l by assumption.
+ rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones_ones, Z.min_id, Z.max_id, Bool.if_const.
+ rewrite Z.land_ones by assumption.
+ rewrite Z.lor_ones_low; auto with zarith.
+ Qed.
+ Hint Rewrite lor_pow2_mod_pow2_r using zutil_arith : zsimplify.
+ Hint Rewrite lor_pow2_mod_pow2_r using assumption : zsimplify_fast.
+
+ Lemma lor_pow2_mod_pow2_l x e (He : 0 <= e) : Z.lor (2^e-1) x mod (2^e) = 2^e-1.
+ Proof. rewrite Z.lor_comm; apply lor_pow2_mod_pow2_r; assumption. Qed.
+ Hint Rewrite lor_pow2_mod_pow2_l using zutil_arith : zsimplify.
+ Hint Rewrite lor_pow2_mod_pow2_l using assumption : zsimplify_fast.
+
+ Lemma lor_pow2_div_pow2_r x e (He : 0 <= e) : (Z.lor x (2^e-1)) / (2^e) = x / 2^e.
+ Proof.
+ destruct (Z_zerop e).
+ { subst; autorewrite with zsimplify_const; reflexivity. }
+ assert (0 < 2^e) by auto with zarith.
+ rewrite <- Z.shiftr_div_pow2, Z.shiftr_lor, !Z.shiftr_div_pow2 by lia.
+ rewrite (Z.div_small (_-1) _), Z.lor_0_r by lia.
+ reflexivity.
+ Qed.
+ Hint Rewrite lor_pow2_div_pow2_r using zutil_arith : zsimplify.
+ Hint Rewrite lor_pow2_div_pow2_r using assumption : zsimplify_fast.
+
+ Lemma lor_pow2_div_pow2_l x e (He : 0 <= e) : (Z.lor (2^e-1) x) / (2^e) = x / 2^e.
+ Proof. rewrite Z.lor_comm; apply lor_pow2_div_pow2_r; assumption. Qed.
+ Hint Rewrite lor_pow2_div_pow2_l using zutil_arith : zsimplify.
+ Hint Rewrite lor_pow2_div_pow2_l using assumption : zsimplify_fast.
End Z.
diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v
index d03c9d196..960c06ce9 100644
--- a/src/Util/ZUtil/Tactics/LinearSubstitute.v
+++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v
@@ -12,6 +12,8 @@ Module Z.
Proof. omega. Qed.
Lemma move_R_Xm x y z : y - x = z -> x = y - z.
Proof. omega. Qed.
+ Lemma move_R_nX x y : -x = y -> x = -y.
+ Proof. omega. Qed.
Lemma move_L_pX x y z : z = x + y -> z - y = x.
Proof. omega. Qed.
Lemma move_L_mX x y z : z = x - y -> z + y = x.
@@ -20,6 +22,8 @@ Module Z.
Proof. omega. Qed.
Lemma move_L_Xm x y z : z = y - x -> y - z = x.
Proof. omega. Qed.
+ Lemma move_L_nX x y : y = -x -> -y = x.
+ Proof. omega. Qed.
(** [linear_substitute x] attempts to maipulate equations using only
addition and subtraction to put [x] on the left, and then
@@ -36,6 +40,8 @@ Module Z.
| ?a - ?b
=> first [ contains for_var b; apply move_L_mX in H
| contains for_var a; apply move_L_Xm in H ]
+ | -?a
+ => contains for_var a; apply move_L_nX in H
| for_var
=> progress symmetry in H
end
@@ -46,6 +52,8 @@ Module Z.
| ?a - ?b
=> first [ not contains for_var b; apply move_R_mX in H
| not contains for_var a; apply move_R_Xm in H ]
+ | -?a
+ => contains for_var a; apply move_R_nX in H
end ].
Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H.
Ltac linear_solve_for for_var :=
diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v
index c850ddef6..06bc648ff 100644
--- a/src/Util/ZUtil/ZSimplify/Core.v
+++ b/src/Util/ZUtil/ZSimplify/Core.v
@@ -1,14 +1,16 @@
Require Import Coq.ZArith.ZArith.
Require Export Crypto.Util.ZUtil.Hints.Core.
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_fast.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify_fast.
+Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_fast.
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify.
-Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l using zutil_arith : zsimplify.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l Z.pow_0_l using zutil_arith : zsimplify.
Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify.
Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify.
Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify.
-Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l : zsimplify_const.
+Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_1_r Z.shiftr_0_r Z.shiftr_0_l Z.shiftl_0_r Z.shiftl_0_l Z.sub_diag : zsimplify_const.
+Hint Rewrite Z.pow_0_l Z.pow_0_l' using assumption : zsimplify_const.
Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const.
diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v
index 94fa05e1a..b176c0b21 100644
--- a/src/Util/ZUtil/ZSimplify/Simple.v
+++ b/src/Util/ZUtil/ZSimplify/Simple.v
@@ -13,6 +13,9 @@ Module Z.
Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1.
Proof. apply Z.pow_1_l; lia. Qed.
Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify.
+ Lemma pow_0_l_Zpos a : 0^Zpos a = 0.
+ Proof. apply Z.pow_0_l; lia. Qed.
+ Hint Rewrite pow_0_l_Zpos : zsimplify_fast zsimplify_const zsimplify.
Lemma sub_same_minus (x y : Z) : x - (x - y) = y.
Proof. lia. Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 02:22:19 +0000