Augment rewrite rule proving tactics for saturated arithmetic

For mit-plv#1609 and
mit-plv#1777

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 :=