From fc5799c2a683e6ead7eabf9594e50149727a68bb Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 4 Dec 2023 00:55:23 -0800
Subject: [PATCH] Add some more ZRangeProofs (#1766)

For https://github.com/mit-plv/fiat-crypto/pull/1761
---
 src/AbstractInterpretation/ZRangeProofs.v | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
index 0a6cca2ef62..5f04e08a176 100644
--- a/src/AbstractInterpretation/ZRangeProofs.v
+++ b/src/AbstractInterpretation/ZRangeProofs.v
@@ -65,11 +65,29 @@ Module Compilers.
           -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
         Proof. induction t; cbn in *; intuition congruence. Qed.
 
+        Lemma is_bounded_by_impl_related_hetero_and_Proper {skip_base} t
+              (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+        : ZRange.type.option.is_bounded_by x v = true
+          -> type.related_hetero_and_Proper (skip_base:=skip_base) (fun _ => eq) (fun _ => eq) (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
+        Proof. induction t; cbn in *; break_innermost_match; intuition congruence. Qed.
+
         Lemma is_bounded_by_impl_eqv_refl t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> x == x /\ v == v.
+        Proof. induction t; cbn; split; try reflexivity; try congruence. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl1 t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> x == x.
+        Proof. intros; eapply is_bounded_by_impl_eqv_refl; eassumption. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl2 t
           (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
           : ZRange.type.option.is_bounded_by x v = true
             -> v == v.
-        Proof. induction t; cbn; try reflexivity; try congruence. Qed.
+        Proof. intros; eapply is_bounded_by_impl_eqv_refl; eassumption. Qed.
 
         Lemma andb_bool_for_each_lhs_of_arrow_is_bounded_by_impl_and_for_each_lhs_of_arrow_eqv_refl t
           (x : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (v : type.for_each_lhs_of_arrow (type.interp base.interp) t)
@@ -79,7 +97,7 @@ Module Compilers.
           induction t; cbn; [ reflexivity | ].
           rewrite Bool.andb_true_iff.
           intros [H0 H1].
-          split; eauto using is_bounded_by_impl_eqv_refl.
+          split; eauto using is_bounded_by_impl_eqv_refl2.
         Qed.
       End option.
     End type.