Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool_union

3 files changed, 13 insertions, 3 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 72a94e54c..3391c741b 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -52,7 +52,7 @@ Module Compilers.
              end%bool.
         Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
           := match t with
-             | base.type.Z => fun r z => (lower r <=? z) && (z <=? upper r)
+             | base.type.Z => fun r z => ZRange.is_bounded_by_bool z r
              | base.type.nat => Nat.eqb
              | base.type.unit => fun _ _ => true
              | base.type.bool => bool_eq
@@ -208,7 +208,7 @@ Module Compilers.
                            | progress cbn in *
                            | progress destruct_head' option
                            | solve [ eauto with nocore ]
-                           | progress cbv [is_tighter_than_bool] in *
+                           | progress cbv [ZRange.is_bounded_by_bool is_tighter_than_bool] in *
                            | progress rewrite ?Bool.andb_true_iff in *
                            | discriminate
                            | apply conj
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 69d1985b2..3e4631de8 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -485,7 +485,7 @@ Module Compilers.
                      ident.gen_interp cast_outside_of_range idc v = v).
       Proof.
         cbv [annotate_ident Option.bind] in Hst; break_innermost_match_hyps; inversion_option; subst;
-          cbv [ident.gen_interp ident.cast abstraction_relation' ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by];
+          cbv [ident.gen_interp ident.cast abstraction_relation' ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by is_bounded_by_bool];
           intros; destruct_head'_prod; cbn [fst snd] in *;
             break_innermost_match; Bool.split_andb; try congruence; reflexivity.
       Qed.
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index e8565bcf3..8da5e69d7 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -87,4 +87,14 @@ Module ZRange.
     cbv [is_tighter_than_bool is_true]; cbn [lower upper]; repeat intro.
     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
+      -> 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.
+    all: lia.
+  Qed.
 End ZRange.