Fix some bounds analysis

1 files changed, 10 insertions, 4 deletions

diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 6b5a430c4..1245bfe3f 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -89,16 +89,22 @@ 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_bool_Proper_if_sumbool_union {A B} (b : sumbool A B) x y rx ry
-    : is_bounded_by_bool x rx = true
-      -> is_bounded_by_bool y ry = true
+  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)
       -> is_bounded_by_bool (if b then x else y) (Operations.ZRange.union rx ry) = true.
   Proof.
     destruct b; cbv [Operations.ZRange.union is_bounded_by_bool];
-      intros; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max.
+      intros; specialize_by_assumption; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max.
     all: lia.
   Qed.
 
+  Lemma is_bounded_by_bool_Proper_if_sumbool_union {A B} (b : sumbool A B) x y rx ry
+    : is_bounded_by_bool x rx = true
+      -> is_bounded_by_bool y ry = true
+      -> is_bounded_by_bool (if b then x else y) (Operations.ZRange.union rx ry) = true.
+  Proof. intros; apply is_bounded_by_bool_Proper_if_sumbool_union_dep; auto. Qed.
+
   Lemma is_bounded_by_bool_opp x r : is_bounded_by_bool (Z.opp x) (ZRange.opp r) = is_bounded_by_bool x r.
   Proof.
     cbv [is_bounded_by_bool andb opp]; cbn [lower upper]; break_match; Z.ltb_to_lt; break_match; Z.ltb_to_lt;