From f02258707a08518df4ad9df0b100aea684f4df31 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Nov 2018 17:25:47 -0400 Subject: Add some zrange lemmas --- src/Util/ZRange/BasicLemmas.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 673a8ac8b..5f434c771 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -157,4 +157,24 @@ Module ZRange. try reflexivity; try lia. Qed. + + Lemma normalize_opp r : normalize (-r) = -(normalize r). + Proof. + cbv [normalize ZRange.opp]; cbn [lower upper]. + rewrite <- !Z.opp_min_distr, <- !Z.opp_max_distr. + reflexivity. + Qed. + + Lemma opp_involutive r : - - r = r. + Proof. + cbv [opp upper lower]; destruct r; rewrite !Z.opp_involutive; reflexivity. + Qed. + + Lemma is_bounded_by_bool_move_opp_normalize r v + : is_bounded_by_bool v (ZRange.normalize (-r)) + = is_bounded_by_bool (-v) (ZRange.normalize r). + Proof. + rewrite <- is_bounded_by_bool_opp at 1. + rewrite normalize_opp, opp_involutive; reflexivity. + Qed. End ZRange. -- cgit v1.2.3