Skip to content

Commit

Permalink
Augment rewrite rule proving tactics for saturated arithmetic (#1783)
Browse files Browse the repository at this point in the history
For #1609 and
#1777
  • Loading branch information
JasonGross authored Dec 10, 2023
1 parent 2964ff0 commit a407ad0
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions src/Rewriter/RulesProofs.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 :=
Expand Down

0 comments on commit a407ad0

Please sign in to comment.