Stronger simplification of adc too add when we can prove the carry is 0

1 files changed, 4 insertions, 59 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index b61e51937..712ba10bc 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -157,66 +157,11 @@ Proof.
                           | [ H : (0 <= FixedWordSizes.wordToZ_gen x < _)%Z |- _ ] => fail
                           | _ => pose proof (FixedWordSizesEquality.wordToZ_gen_range x)
                           end
-                     | [ |- context[Z.max ?x ?y] ]
-                       => first [ rewrite (Z.max_r x y) by omega
-                                | rewrite (Z.max_l x y) by omega ]
-                     | [ H : 0 < ?e |- context[(_ mod (2^Z.of_nat (2^?e)))%Z] ]
+                     | [ |- context[FixedWordSizes.wordToZ ?e] ]
                        => lazymatch goal with
-                          | [ H : (_ <= 2^Z.of_nat (2^e))%Z |- _ ] => fail
-                          | _ => assert (2^Z.of_nat (2^1) <= 2^Z.of_nat (2^e))%Z
-                              by (rewrite !Z.pow_Zpow; simpl Z.of_nat; auto with zarith)
-                          end
-                     | [ H : (1 < ?e)%Z |- context[(_ mod (2^?e))%Z] ]
-                       => lazymatch goal with
-                          | [ H : (_ <= 2^e)%Z |- _ ] => fail
-                          | _ => assert (2^2 <= 2^e)%Z
-                              by auto with zarith
-                          end
-                     | [ |- context[Z.max 0 (?x mod ?y)] ]
-                       => rewrite (Z.max_r 0 (x mod y))
-                         by Z.zero_bounds
-                     | [ |- context[Z.max 0 ((?x mod ?y) * (?z mod ?w))] ]
-                       => rewrite (Z.max_r 0 ((x mod y) * (z mod w)))
-                         by Z.zero_bounds
-                     end
-                   | rewrite !FixedWordSizesEquality.wordToZ_ZToWord_mod_full
-                   | progress Z.rewrite_mod_small
-                   | rewrite Z.div_small by omega
-                   | rewrite <- FixedWordSizesEquality.eq_ZToWord ].
-  all:repeat first [ reflexivity
-                   | omega
-                   | discriminate
-                   | progress cbv [LetIn.Let_In Z.zselect IdfunWithAlt.id_with_alt]
-                   | progress subst
-                   | progress simpl in *
-                   | progress Bool.split_andb
-                   | progress Z.ltb_to_lt
-                   | break_innermost_match_step
-                   | rewrite FixedWordSizesEquality.ZToWord_wordToZ
-                   | rewrite FixedWordSizesEquality.ZToWord_wordToZ_ZToWord by reflexivity
-                   | rewrite FixedWordSizesEquality.wordToZ_ZToWord_0
-                   | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r
-                   | rewrite !Z.sub_with_borrow_to_add_get_carry
-                   | progress autorewrite with zsimplify_fast
-                   | progress cbv [cast_const ZToInterp interpToZ]
-                   | progress change (Z.pow_pos 2 1) with 2%Z in *
-                   | progress change (Z.pow_pos 2 2) with 4%Z in *
-                   | nia
-                   | progress cbv [Z.add_with_carry]
-                   | match goal with
-                     | [ |- context[(?x mod ?m)%Z] ]
-                       => rewrite (Z.mod_small x m) by solve_word_small ()
-                     | [ |- context[(?x / ?m)%Z] ]
-                       => rewrite (Z.div_small x m) by solve_word_small ()
-                     | [ H : ?x = 0%Z |- context[?x] ] => rewrite H
-                     | [ H : ?x = 1%Z |- context[?x] ] => rewrite H
-                     | [ H : (_ =? _)%nat = true |- _ ] => apply beq_nat_true in H
-                     | [ H : (_ <? _)%nat = true |- _ ] => apply NPeano.Nat.ltb_lt in H
-                     | [ |- context[FixedWordSizes.wordToZ_gen ?x] ]
-                       => lazymatch goal with
-                          | [ H : (0 <= FixedWordSizes.wordToZ_gen x)%Z |- _ ] => fail
-                          | [ H : (0 <= FixedWordSizes.wordToZ_gen x < _)%Z |- _ ] => fail
-                          | _ => pose proof (FixedWordSizesEquality.wordToZ_gen_range x)
+                          | [ H : (0 <= FixedWordSizes.wordToZ e)%Z |- _ ] => fail
+                          | [ H : (0 <= FixedWordSizes.wordToZ e < _)%Z |- _ ] => fail
+                          | _ => pose proof (FixedWordSizesEquality.wordToZ_range e)
                           end
                      | [ |- context[Z.max ?x ?y] ]
                        => first [ rewrite (Z.max_r x y) by omega