From f22454c7a80b174a5c0cac1f3648727df054f9c9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 11 Oct 2018 14:23:35 -0400 Subject: Add some zrange lemmas --- src/Util/ZRange/BasicLemmas.v | 23 +++++++++++++++++++++++ src/Util/ZRange/Operations.v | 2 ++ 2 files changed, 25 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 4bdcb19ef..673a8ac8b 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -67,10 +67,17 @@ Module ZRange. | [ |- or _ (false = true) ] => left | [ |- or _ (?x = ?x) ] => right | [ H : true = false |- _ ] => exfalso; clear -H; discriminate + | [ H : Build_zrange _ _ = Build_zrange _ _ |- _ ] => inversion H; clear H end | progress specialize_by omega | progress destruct_head'_or ]. + Lemma goodb_normalize r : goodb (normalize r) = true. + Proof. repeat t2_step. Qed. + + Lemma normalize_id_iff_goodb {r} : goodb r = true <-> normalize r = r. + Proof. repeat t2_step. Qed. + Lemma is_tighter_than_bool_extend_land_lor_bounds r : is_tighter_than_bool r (extend_land_lor_bounds r) = true. Proof. repeat t2_step. Qed. @@ -95,6 +102,22 @@ Module ZRange. rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption. Qed. + Lemma is_bounded_by_normalize r + : forall v, is_bounded_by_bool v r = true -> is_bounded_by_bool v (normalize r) = true. + Proof. + apply <- is_bounded_by_iff_is_tighter_than; destruct (goodb r) eqn:?; [ left | right; reflexivity ]. + rewrite (proj1 normalize_id_iff_goodb) by assumption; change (is_true (is_tighter_than_bool r r)); reflexivity. + Qed. + + Lemma goodb_of_is_bounded_by_bool v r : is_bounded_by_bool v r = true -> goodb r = true. + Proof. repeat t2_step. Qed. + + Lemma is_tighter_than_bool_normalize_of_goodb r : goodb r = true -> is_tighter_than_bool r (normalize r) = true. + Proof. repeat t2_step. Qed. + + Lemma normalize_is_tighter_than_bool_of_goodb r : goodb r = true -> is_tighter_than_bool (normalize r) r = true. + Proof. repeat t2_step. Qed. + Lemma is_bounded_by_of_is_tighter_than r1 r2 (H : is_tighter_than_bool r1 r2 = true) : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true). Proof. apply is_bounded_by_iff_is_tighter_than; auto. Qed. diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index c6f209e16..32924e6dc 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -31,6 +31,8 @@ Module ZRange. Lemma normalize'_eq : normalize = normalize'. Proof. reflexivity. Defined. + Definition size (v : zrange) : Z := upper (normalize v) - lower (normalize v). + Definition abs (v : zrange) : zrange := let (l, u) := eta v in r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ]. -- cgit v1.2.3