From cd24907d7c46ddc52989a5cfa7a10c3c4568eee3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Aug 2018 17:05:30 -0400 Subject: Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool_union --- src/Experiments/NewPipeline/AbstractInterpretation.v | 4 ++-- src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 2 +- src/Util/ZRange/BasicLemmas.v | 10 ++++++++++ 3 files changed, 13 insertions(+), 3 deletions(-) (limited to 'src') 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. -- cgit v1.2.3