From f69b87e6400f84f3e5e9707bfd7d6e1aa460b632 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 00:53:11 -0400 Subject: Alter relax_output_bounds statement It needs to fit the actual statement of MapBounds correctness --- src/Reflection/Z/Bounds/Relax.v | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) (limited to 'src/Reflection') 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. -- cgit v1.2.3