Alter relax_output_bounds statement

It needs to fit the actual statement of MapBounds correctness

1 files changed, 25 insertions, 1 deletions

diff --git a/src/Reflection/Z/Bounds/Relax.v b/src/Reflection/Z/Bounds/Relax.v
index 52978fabd..5269639e1 100644
--- a/src/Reflection/Z/Bounds/Relax.v
+++ b/src/Reflection/Z/Bounds/Relax.v
@@ -28,7 +28,7 @@ Local Arguments Z.pow : simpl never.
 Local Arguments Z.sub !_ !_.
 Local Arguments Z.add !_ !_.
 Local Arguments Z.mul !_ !_.
-Lemma relax_output_bounds
+Lemma relax_output_bounds'
       t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t)
       (Hv : SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds
             = SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) tight_output_bounds)
@@ -102,3 +102,27 @@ Proof.
                           let k := fresh in intro k; intros; subst k
                      end ]. }
 Qed.
+
+Lemma relax_output_bounds
+      t (tight_output_bounds relaxed_output_bounds : interp_flat_type Bounds.interp_base_type t)
+      (Hv : SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds
+            = SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) tight_output_bounds)
+      v k
+      (v' := eq_rect _ (interp_flat_type _) v _ Hv)
+      (Htighter : @Bounds.is_bounded_by t tight_output_bounds k
+                  /\ @cast_back_flat_const
+                       (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) tight_output_bounds
+                       v'
+                     = k)
+      (Hrelax : Bounds.is_tighter_thanb tight_output_bounds relaxed_output_bounds = true)
+  : @Bounds.is_bounded_by t relaxed_output_bounds k
+    /\ @cast_back_flat_const
+         (@Bounds.interp_base_type) t (fun _ => Bounds.bounds_to_base_type) relaxed_output_bounds
+         v
+       = k.
+Proof.
+  pose proof (fun pf => @relax_output_bounds' t tight_output_bounds relaxed_output_bounds Hv v k (conj pf (proj2 Htighter)) Hrelax) as H.
+  destruct H as [H1 H2]; [ | rewrite <- H2; tauto ].
+  subst v'.
+  destruct Htighter; subst k; assumption.
+Qed.