Add a couple of zrange lemmas

2 files changed, 61 insertions, 11 deletions

diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index c5dcaa3d4..b8f9c7c66 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -1,7 +1,11 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.omega.Omega.
+Require Import Coq.micromega.Lia.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.DestructHead.
 
@@ -11,17 +15,17 @@ Module ZRange.
 
   Local Notation eta v := r[ lower v ~> upper v ].
 
-  Local Ltac t :=
-    repeat first [ reflexivity
-                 | progress destruct_head' zrange
-                 | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt]
-                 | progress split_min_max
-                 | match goal with
-                   | [ |- _ = _ :> zrange ] => apply f_equal2
-                   end
-                 | omega
-                 | solve [ auto ] ].
-
+  Local Ltac t_step :=
+    first [ reflexivity
+          | progress destruct_head' zrange
+          | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt andb Z.leb Z.geb] in *
+          | progress split_min_max
+          | match goal with
+            | [ |- _ = _ :> zrange ] => apply f_equal2
+            end
+          | omega
+          | solve [ auto ] ].
+  Local Ltac t := repeat t_step.
 
   Lemma flip_flip v : flip (flip v) = v.
   Proof. destruct v; reflexivity. Qed.
@@ -34,4 +38,39 @@ Module ZRange.
 
   Definition normalize_or v : normalize v = v \/ normalize v = flip v.
   Proof. t. Qed.
+
+  Local Ltac t2_step :=
+    first [ t_step
+          | rewrite !Bool.andb_true_iff
+          | rewrite !Z.leb_le
+          | rewrite !Z.leb_gt
+          | rewrite Bool.andb_true_iff in *
+          | rewrite Z.leb_le in *
+          | rewrite Z.leb_gt in *
+          | progress intros
+          | match goal with
+            | [ H : context[andb _ _ = true] |- _ ] => setoid_rewrite Bool.andb_true_iff in H
+            | [ |- context[andb _ _ = true] ] => setoid_rewrite Bool.andb_true_iff
+            | [ H : context[Z.leb _ _ = true] |- _ ] => setoid_rewrite Z.leb_le in H
+            | [ |- context[Z.leb _ _ = true] ] => setoid_rewrite Z.leb_le
+            | [ H : context[Z.leb _ _ = false] |- _ ] => setoid_rewrite Z.leb_gt in H
+            | [ |- context[Z.leb _ _ = false] ] => setoid_rewrite Z.leb_gt
+            | [ |- and _ _ ] => apply conj
+            | [ |- or _ (true = false) ] => left
+            | [ |- or _ (false = true) ] => left
+            | [ |- or _ (?x = ?x) ] => right
+            | [ H : true = false |- _ ] => exfalso; clear -H; discriminate
+            end
+          | progress specialize_by omega
+          | progress destruct_head'_or ].
+
+  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).
+  Proof. repeat t2_step; specialize_all_ways; repeat t2_step. Qed.
+
+  Lemma is_bounded_by_iff_is_tighter_than_good r1 r2 (Hgood : goodb r1 = true)
+    : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true)
+      <-> (is_tighter_than_bool r1 r2 = true).
+  Proof. rewrite is_bounded_by_iff_is_tighter_than; intuition (congruence || auto). Qed.
 End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 881a28a31..d17785f77 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -78,6 +78,12 @@ Module ZRange.
           => let (lx, ux) := x in
              let (ly, uy) := y in
              {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}).
+  Definition lor_bounds : zrange -> zrange -> zrange
+    := extremization_bounds
+         (fun x y
+          => let (lx, ux) := x in
+             let (ly, uy) := y in
+             {| lower := Z.max lx ly ; upper := upper_lor_land_bounds ux uy |}).
 
   Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange :=
     if upper r <? split_at
@@ -87,4 +93,9 @@ Module ZRange.
                 {| lower := lower r / split_at; upper := (upper r / split_at) |} )
     else ( {| lower := 0; upper := split_at - 1 |},
            {| lower := lower r / split_at; upper := (upper r / split_at) |} ).
+
+  Definition good (r : zrange) : Prop
+    := lower r <= upper r.
+  Definition goodb (r : zrange) : bool
+    := (lower r <=? upper r)%Z.
 End ZRange.