From 0055c8c95e7f2da419b8fcfe8de6e117fc8352a6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Dec 2023 21:15:28 -0500 Subject: [PATCH] Augment rewrite rule proving tactics for saturated arithmetic For https://github.com/mit-plv/fiat-crypto/pull/1609 and https://github.com/mit-plv/fiat-crypto/pull/1777 --- src/Rewriter/RulesProofs.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v index 55c96c2888..1eb8f63004 100644 --- a/src/Rewriter/RulesProofs.v +++ b/src/Rewriter/RulesProofs.v @@ -263,6 +263,13 @@ Local Ltac interp_good_t_step_arith := => cbv [Z.ltz]; apply unfold_is_bounded_by_bool in Hx; apply unfold_is_bounded_by_bool in Hy + | [ H : is_bounded_by_bool _ (ZRange.normalize r[0 ~> 1]) = true |- _ ] + => change (ZRange.normalize r[0 ~> 1]) with r[0 ~> 1]%zrange in *; + cbv [is_bounded_by_bool] in H; cbn [upper lower] in H + | [ H : ?x <> ?a, H' : ?a <= ?x |- _ ] => assert (a < x) by lia; clear H H' + | [ H : 0 < ?x, H' : ?x <= 1 |- _ ] => assert (x = 1) by lia; clear H H' + | [ H : ?x <= 1, H' : 0 <= ?x |- _ ] => assert (x = 0 \/ x = 1) by lia; clear H H' + | [ H : ?x = Z.neg _ |- context[?x] ] => rewrite H | [ |- context[ident.cast r[0~>0] ?v] ] => rewrite (ident.platform_specific_cast_0_is_mod 0 v) by reflexivity | [ H : ?x = Z.ones _ |- context [Z.land _ ?x] ] => rewrite H @@ -288,6 +295,7 @@ Local Ltac interp_good_t_step_arith := | progress destruct_head'_and | progress Z.ltb_to_lt | progress split_andb + | progress change (0 - 1) with (-1) in * | match goal with | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia @@ -399,6 +407,9 @@ Local Ltac interp_good_t_step_arith := => tryif constr_eq x x' then fail else replace x with x' by lia | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast end + | match goal with + | [ |- context[(- _) mod _] ] => rewrite Z.mod_opp_small by lia + end | saturate_add_sub_bounds_step ]. Local Ltac remove_casts :=