diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Bounds/Relax.v | 26 |
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. |