Reify most rewrite rules

Currently we don't handle rules that require "concrete list of cons
cells" nor rules that require "concrete nat literal to do recursion on";
both of these require special treatment, to be implemented in an
upcoming commit.

The reifier is kind-of slow, alas.

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
21m52.72s | Total                                        | 21m20.90s || +0m31.82s | +2.48%
--------------------------------------------------------------------------------------------
1m12.22s  | Rewriter.vo                                  | 0m47.38s  || +0m24.83s | +52.42%
3m14.35s  | p384_32.c                                    | 3m19.59s  || -0m05.24s | -2.62%
1m45.12s  | RewriterRulesGood.vo                         | 1m39.44s  || +0m05.68s | +5.71%
0m40.82s  | ExtractionHaskell/unsaturated_solinas        | 0m37.58s  || +0m03.24s | +8.62%
1m35.04s  | RewriterRulesInterpGood.vo                   | 1m32.48s  || +0m02.56s | +2.76%
0m59.49s  | ExtractionHaskell/word_by_word_montgomery    | 0m56.71s  || +0m02.78s | +4.90%
1m45.10s  | Fancy/Barrett256.vo                          | 1m47.00s  || -0m01.90s | -1.77%
0m40.21s  | p521_64.c                                    | 0m38.97s  || +0m01.24s | +3.18%
0m24.42s  | SlowPrimeSynthesisExamples.vo                | 0m25.67s  || -0m01.25s | -4.86%
0m20.48s  | secp256k1_32.c                               | 0m19.27s  || +0m01.21s | +6.27%
1m47.10s  | RewriterWf2.vo                               | 1m47.22s  || -0m00.12s | -0.11%
0m47.85s  | p521_32.c                                    | 0m47.47s  || +0m00.38s | +0.80%
0m45.66s  | RewriterInterpProofs1.vo                     | 0m45.74s  || -0m00.08s | -0.17%
0m37.18s  | Fancy/Montgomery256.vo                       | 0m37.14s  || +0m00.03s | +0.10%
0m36.26s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m36.14s  || +0m00.11s | +0.33%
0m28.38s  | ExtractionHaskell/saturated_solinas          | 0m28.04s  || +0m00.33s | +1.21%
0m26.80s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m26.83s  || -0m00.02s | -0.11%
0m24.00s  | RewriterWf1.vo                               | 0m23.96s  || +0m00.03s | +0.16%
0m19.82s  | ExtractionOCaml/word_by_word_montgomery      | 0m20.34s  || -0m00.51s | -2.55%
0m19.65s  | p256_32.c                                    | 0m19.24s  || +0m00.41s | +2.13%
0m18.54s  | p448_solinas_64.c                            | 0m19.24s  || -0m00.69s | -3.63%
0m16.18s  | p434_64.c                                    | 0m16.49s  || -0m00.30s | -1.87%
0m13.67s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m14.47s  || -0m00.80s | -5.52%
0m13.22s  | ExtractionOCaml/unsaturated_solinas          | 0m13.72s  || -0m00.50s | -3.64%
0m09.91s  | p224_32.c                                    | 0m09.89s  || +0m00.01s | +0.20%
0m09.85s  | ExtractionOCaml/saturated_solinas            | 0m09.83s  || +0m00.01s | +0.20%
0m08.66s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.86s  || +0m00.79s | +10.17%
0m08.36s  | p384_64.c                                    | 0m08.46s  || -0m00.10s | -1.18%
0m07.72s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m08.29s  || -0m00.56s | -6.87%
0m06.66s  | BoundsPipeline.vo                            | 0m06.73s  || -0m00.07s | -1.04%
0m06.50s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m06.56s  || -0m00.05s | -0.91%
0m06.22s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.69s  || +0m00.52s | +9.31%
0m05.50s  | ExtractionHaskell/saturated_solinas.hs       | 0m05.88s  || -0m00.37s | -6.46%
0m03.51s  | PushButtonSynthesis/Primitives.vo            | 0m03.48s  || +0m00.02s | +0.86%
0m03.34s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.32s  || +0m00.02s | +0.60%
0m03.31s  | curve25519_32.c                              | 0m03.13s  || +0m00.18s | +5.75%
0m03.15s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m03.12s  || +0m00.02s | +0.96%
0m03.11s  | PushButtonSynthesis/BarrettReduction.vo      | 0m03.08s  || +0m00.02s | +0.97%
0m02.80s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m02.86s  || -0m00.06s | -2.09%
0m02.13s  | curve25519_64.c                              | 0m02.02s  || +0m00.10s | +5.44%
0m01.58s  | p256_64.c                                    | 0m01.66s  || -0m00.07s | -4.81%
0m01.53s  | p224_64.c                                    | 0m01.60s  || -0m00.07s | -4.37%
0m01.49s  | secp256k1_64.c                               | 0m01.72s  || -0m00.23s | -13.37%
0m01.34s  | CLI.vo                                       | 0m01.23s  || +0m00.11s | +8.94%
0m01.16s  | RewriterProofs.vo                            | 0m01.10s  || +0m00.05s | +5.45%
0m01.16s  | StandaloneOCamlMain.vo                       | 0m01.13s  || +0m00.03s | +2.65%
0m01.10s  | CompilersTestCases.vo                        | 0m01.09s  || +0m00.01s | +0.91%
0m01.07s  | StandaloneHaskellMain.vo                     | 0m01.04s  || +0m00.03s | +2.88%

1 files changed, 5 insertions, 0 deletions

diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v
index a2aa56a36..954340fa4 100644
--- a/src/RewriterRulesInterpGood.v
+++ b/src/RewriterRulesInterpGood.v
@@ -475,7 +475,10 @@ Module Compilers.
                 | [ |- ?x = ?x ] => reflexivity
                 | [ |- True ] => exact I
                 | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence
+                | [ H : true = false |- _ ]=> exfalso; clear -H; congruence
+                | [ H : false = true |- _ ]=> exfalso; clear -H; congruence
                 end
+              | progress cbv [option_beq] in *
               | match goal with
                 | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ]
                   => rewrite ZRange.normalize_idempotent in H
@@ -689,6 +692,8 @@ Module Compilers.
                    |- context[?v mod ?m] ]
                  => unique assert (is_bounded_by_bool v r[0~>x-1] = true)
                    by (eapply ZRange.is_bounded_by_of_is_tighter_than; eassumption)
+               | _ => progress Z.ltb_to_lt
+               | _ => progress subst
                end.
 
       Local Ltac unfold_cast_lemmas :=