Automate more of the rewriter reification, proof

Now we actually make use of the rewrite-rule-specific proofs, rather
than duplicating them inline.

We now support reifying `ident.gets_inlined` to
`SubstVarLike.is_var_fst_snd_pair_opp_cast`.

We also now fix a bug where we previously incorrectly substituted
context variables when reifying side conditions (needed for correct
reification of split-mul things, coming up soon).

Things are unfortunately a bit slow.

I'm not sure what's up with my proof of
`reflect_ident_iota_interp_related`; it seems more complicated than it
should be (maybe partly due to funext concerns).

Next up is to split out the rewrite rule generation bits into separate
files and have a single tactic that builds the entire package for us (in
prep for making the rewriter builder a vernacular).  After that I want
to more fully parameterize things over `ident`, and then also over the
non-container base-types (which will require some reworking of how we
handle special identifiers).  Additionally, I want to make the rewrite
rule definitions not depend on Language.v.

After     | File Name                                       | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------
20m50.18s | Total                                           | 23m01.24s || -2m11.06s | -9.48%
-----------------------------------------------------------------------------------------------
0m27.24s  | RewriterRulesGood.vo                            | 1m34.94s  || -1m07.70s | -71.30%
0m54.89s  | RewriterRulesInterpGood.vo                      | 1m57.72s  || -1m02.82s | -53.37%
1m37.88s  | RewriterWf2.vo                                  | 1m47.69s  || -0m09.81s | -9.10%
1m16.71s  | Rewriter.vo                                     | 1m12.61s  || +0m04.10s | +5.64%
0m37.14s  | ExtractionHaskell/unsaturated_solinas           | 0m40.06s  || -0m02.92s | -7.28%
0m36.10s  | RewriterWf1.vo                                  | 0m33.12s  || +0m02.98s | +8.99%
0m18.31s  | p256_32.c                                       | 0m20.70s  || -0m02.39s | -11.54%
1m43.31s  | Fancy/Barrett256.vo                             | 1m42.09s  || +0m01.21s | +1.19%
0m32.46s  | ExtractionHaskell/saturated_solinas             | 0m30.92s  || +0m01.53s | +4.98%
0m23.44s  | ExtractionOCaml/word_by_word_montgomery         | 0m22.26s  || +0m01.17s | +5.30%
0m12.17s  | ExtractionOCaml/word_by_word_montgomery.ml      | 0m13.58s  || -0m01.41s | -10.38%
0m10.04s  | p224_32.c                                       | 0m08.20s  || +0m01.83s | +22.43%
0m09.98s  | ExtractionOCaml/saturated_solinas               | 0m11.67s  || -0m01.68s | -14.48%
0m07.80s  | ExtractionOCaml/saturated_solinas.ml            | 0m06.16s  || +0m01.63s | +26.62%
0m06.87s  | ExtractionHaskell/saturated_solinas.hs          | 0m04.98s  || +0m01.88s | +37.95%
3m23.11s  | p384_32.c                                       | 3m22.61s  || +0m00.50s | +0.24%
0m59.32s  | ExtractionHaskell/word_by_word_montgomery       | 0m58.76s  || +0m00.56s | +0.95%
0m46.19s  | p521_32.c                                       | 0m47.16s  || -0m00.96s | -2.05%
0m45.26s  | RewriterInterpProofs1.vo                        | 0m45.64s  || -0m00.38s | -0.83%
0m39.50s  | p521_64.c                                       | 0m38.97s  || +0m00.53s | +1.36%
0m36.38s  | PushButtonSynthesis/UnsaturatedSolinas.vo       | 0m36.00s  || +0m00.38s | +1.05%
0m34.40s  | Fancy/Montgomery256.vo                          | 0m34.63s  || -0m00.23s | -0.66%
0m26.95s  | PushButtonSynthesis/WordByWordMontgomery.vo     | 0m26.44s  || +0m00.50s | +1.92%
0m25.62s  | SlowPrimeSynthesisExamples.vo                   | 0m26.04s  || -0m00.41s | -1.61%
0m24.39s  | RewriterRulesProofs.vo                          | 0m24.18s  || +0m00.21s | +0.86%
0m20.49s  | PushButtonSynthesis/BarrettReduction.vo         | 0m20.62s  || -0m00.13s | -0.63%
0m18.54s  | p448_solinas_64.c                               | 0m19.15s  || -0m00.60s | -3.18%
0m17.37s  | secp256k1_32.c                                  | 0m17.70s  || -0m00.32s | -1.86%
0m14.80s  | p434_64.c                                       | 0m14.16s  || +0m00.64s | +4.51%
0m14.05s  | ExtractionOCaml/unsaturated_solinas             | 0m14.28s  || -0m00.22s | -1.61%
0m09.17s  | ExtractionOCaml/unsaturated_solinas.ml          | 0m09.58s  || -0m00.41s | -4.27%
0m08.47s  | ExtractionHaskell/word_by_word_montgomery.hs    | 0m08.22s  || +0m00.25s | +3.04%
0m07.69s  | p384_64.c                                       | 0m07.72s  || -0m00.02s | -0.38%
0m06.80s  | BoundsPipeline.vo                               | 0m06.65s  || +0m00.14s | +2.25%
0m06.49s  | ExtractionHaskell/unsaturated_solinas.hs        | 0m05.59s  || +0m00.90s | +16.10%
0m03.54s  | PushButtonSynthesis/Primitives.vo               | 0m03.46s  || +0m00.08s | +2.31%
0m03.35s  | PushButtonSynthesis/SmallExamples.vo            | 0m03.36s  || -0m00.00s | -0.29%
0m03.19s  | PushButtonSynthesis/SaturatedSolinas.vo         | 0m03.15s  || +0m00.04s | +1.26%
0m02.79s  | curve25519_32.c                                 | 0m03.32s  || -0m00.52s | -15.96%
0m02.66s  | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s  || -0m00.06s | -2.56%
0m02.55s  | RewriterRules.vo                                | 0m02.52s  || +0m00.02s | +1.19%
0m01.98s  | curve25519_64.c                                 | 0m01.57s  || +0m00.40s | +26.11%
0m01.78s  | p224_64.c                                       | 0m01.30s  || +0m00.48s | +36.92%
0m01.60s  | secp256k1_64.c                                  | 0m01.74s  || -0m00.13s | -8.04%
0m01.45s  | p256_64.c                                       | 0m01.55s  || -0m00.10s | -6.45%
0m01.34s  | RewriterProofs.vo                               | 0m01.16s  || +0m00.18s | +15.51%
0m01.33s  | CLI.vo                                          | 0m01.40s  || -0m00.06s | -4.99%
0m01.12s  | StandaloneOCamlMain.vo                          | 0m01.09s  || +0m00.03s | +2.75%
0m01.10s  | CompilersTestCases.vo                           | 0m01.08s  || +0m00.02s | +1.85%
0m01.08s  | StandaloneHaskellMain.vo                        | 0m01.02s  || +0m00.06s | +5.88%

1 files changed, 36 insertions, 163 deletions

diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v
index c4486ef67..c05bcc23e 100644
--- a/src/RewriterRulesGood.v
+++ b/src/RewriterRulesGood.v
@@ -44,151 +44,11 @@ Module Compilers.
   Module Import RewriteRules.
     Import Rewriter.Compilers.RewriteRules.
 
-    Lemma nbe_rewrite_head_eq : @nbe_rewrite_head = @nbe_rewrite_head0.
-    Proof. reflexivity. Qed.
-
-    Lemma fancy_rewrite_head_eq
-      : (fun var do_again => @fancy_rewrite_head var)
-        = @fancy_rewrite_head0.
-    Proof. reflexivity. Qed.
-
-    Lemma arith_rewrite_head_eq max_const_val : (fun var do_again => @arith_rewrite_head max_const_val var) = (fun var => @arith_rewrite_head0 var max_const_val).
-    Proof. reflexivity. Qed.
-
-    Lemma fancy_with_casts_rewrite_head_eq invert_low invert_high value_range flag_range
-      : (fun var do_again => @fancy_with_casts_rewrite_head invert_low invert_high value_range flag_range var)
-        = (fun var => @fancy_with_casts_rewrite_head0 var invert_low invert_high value_range flag_range).
-    Proof. reflexivity. Qed.
-
-    Lemma arith_with_casts_rewrite_head_eq : @arith_with_casts_rewrite_head = @arith_with_casts_rewrite_head0.
-    Proof. reflexivity. Qed.
-
-    Lemma strip_literal_casts_rewrite_head_eq : (fun var do_again => @strip_literal_casts_rewrite_head var) = @strip_literal_casts_rewrite_head0.
-    Proof. reflexivity. Qed.
-
-    Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules.
-    Proof. reflexivity. Qed.
-
-    Lemma fancy_all_rewrite_rules_eq : @fancy_all_rewrite_rules = @fancy_rewrite_rules.
-    Proof. reflexivity. Qed.
-
-    Lemma arith_all_rewrite_rules_eq : @arith_all_rewrite_rules = @arith_rewrite_rules.
-    Proof. reflexivity. Qed.
-
-    Lemma fancy_with_casts_all_rewrite_rules_eq : @fancy_with_casts_all_rewrite_rules = @fancy_with_casts_rewrite_rules.
-    Proof. reflexivity. Qed.
-
-    Lemma arith_with_casts_all_rewrite_rules_eq : @arith_with_casts_all_rewrite_rules = @arith_with_casts_rewrite_rules.
-    Proof. reflexivity. Qed.
-
-    Lemma strip_literal_casts_all_rewrite_rules_eq : @strip_literal_casts_all_rewrite_rules = @strip_literal_casts_rewrite_rules.
-    Proof. reflexivity. Qed.
-
     Section good.
       Context {var1 var2 : type -> Type}.
 
       Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2).
 
-      Lemma wf_rlist_rect_gen
-            {ivar1 ivar2 A P}
-            Q
-            N1 N2 C1 C2 ls1 ls2 G
-            (Hwf : expr.wf G ls1 ls2)
-            (HN : UnderLets.wf Q G N1 N2)
-            (HC : forall G' x xs y ys rec1 rec2,
-                (exists seg, G' = (seg ++ G)%list)
-                -> expr.wf G x y
-                -> expr.wf G (reify_list xs) (reify_list ys)
-                -> Q G' rec1 rec2
-                -> UnderLets.wf Q G' (C1 x xs rec1) (C2 y ys rec2))
-        : option_eq (UnderLets.wf Q G)
-                    (@rlist_rect var1 A P ivar1 N1 C1 ls1)
-                    (@rlist_rect var2 A P ivar2 N2 C2 ls2).
-      Proof using Type.
-        cbv [rlist_rect].
-        cbv [Compile.option_bind' Option.bind].
-        break_innermost_match.
-        all: repeat first [ match goal with
-                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
-                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
-                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
-                                exfalso; clear -H H'; congruence
-                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                            end
-                          | progress expr.invert_subst
-                          | progress cbn [sequence_return option_eq]
-                          | assumption
-                          | reflexivity
-                          | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G')
-                          | progress intros ].
-        lazymatch goal with
-        | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ]
-          => revert dependent l'; intro l2; revert dependent l; intro l1
-        end.
-        revert l2; induction l1 as [|l1 ls1 IHls1], l2; cbn [list_rect];
-          rewrite ?expr.reify_list_cons, ?expr.reify_list_nil;
-          intros; expr.inversion_wf_constr; [ assumption | ].
-        all: repeat first [ match goal with
-                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
-                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
-                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
-                                exfalso; clear -H H'; congruence
-                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                            end
-                          | progress expr.invert_subst
-                          | progress cbn [sequence_return option_eq]
-                          | assumption
-                          | reflexivity
-                          | solve [ auto ]
-                          | progress subst
-                          | apply @UnderLets.wf_splice with (P:=Q)
-                          | progress intros
-                          | wf_safe_t_step
-                          | progress type.inversion_type
-                          | progress expr.inversion_wf_constr ].
-      Qed.
-      Lemma wf_rlist_rect {A P}
-            N1 N2 C1 C2 ls1 ls2 G
-            (Hwf : expr.wf G ls1 ls2)
-            (HN : UnderLets.wf (fun G' => expr.wf G') G N1 N2)
-            (HC : forall G' x xs y ys rec1 rec2,
-                (exists seg, G' = (seg ++ G)%list)
-                -> expr.wf G x y
-                -> expr.wf G (reify_list xs) (reify_list ys)
-                -> expr.wf G' rec1 rec2
-                -> UnderLets.wf (fun G'' => expr.wf G'') G' (C1 x xs rec1) (C2 y ys rec2))
-        : option_eq (UnderLets.wf (fun G' => expr.wf G') G)
-                    (@rlist_rect var1 A P var1 N1 C1 ls1)
-                    (@rlist_rect var2 A P var2 N2 C2 ls2).
-      Proof using Type. apply wf_rlist_rect_gen; assumption. Qed.
-      Lemma wf_rlist_rectv {A P}
-            N1 N2 C1 C2 ls1 ls2 G
-            (Hwf : expr.wf G ls1 ls2)
-            (HN : UnderLets.wf (fun G' v1 v2
-                                => exists G'',
-                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                    /\ expr.wf G'' v1 v2) G N1 N2)
-            (HC : forall G' x xs y ys rec1 rec2,
-                (exists seg, G' = (seg ++ G)%list)
-                -> expr.wf G x y
-                -> expr.wf G (reify_list xs) (reify_list ys)
-                -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                /\ expr.wf G'' rec1 rec2)
-                -> UnderLets.wf (fun G' v1 v2
-                                 => exists G'',
-                                     (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                     /\ expr.wf G'' v1 v2)
-                                G' (C1 x xs rec1) (C2 y ys rec2))
-        : option_eq (UnderLets.wf
-                       (fun G' v1 v2
-                        => exists G'',
-                            (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                            /\ expr.wf G'' v1 v2)
-                       G)
-                    (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1)
-                    (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2).
-      Proof using Type. apply wf_rlist_rect_gen; assumption. Qed.
-
       Lemma wf_list_rect {T A}
             G N1 N2 C1 C2 ls1 ls2
             (HN : Compile.wf_value G N1 N2)
@@ -222,22 +82,29 @@ Module Compilers.
             (nat_rect (fun _ => @Compile.value_with_lets base.type ident var2 A) O2 S2 n).
       Proof. induction n; cbn [nat_rect]; try eapply HS; eauto using (ex_intro _ nil). Qed.
 
+      Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps].
+
       Local Ltac start_good :=
-        apply Compile.rewrite_rules_goodT_by_curried;
-        split; [ reflexivity | ];
-        lazymatch goal with
-        | [ |- forall x p x' p', In (@existT ?A ?P x p, @existT ?A' ?P' x' p') ?ls -> @?Q x x' p p' ]
-          => apply (@forall_In_pair_existT A A' P P' Q ls); cbn [projT1 projT2 fst snd]; cbv [id]
-        end;
-        (exists eq_refl);
-        cbn [eq_rect];
-        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default pattern.base.lookup_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq];
-        cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb];
-        repeat first [ progress intros
-                     | match goal with
-                       | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
-                       end
-                     | progress cbn [eq_rect] in * ].
+        match goal with
+        | [ |- rewrite_rules_goodT ?rew1 ?rew2 ]
+          => let H := fresh in
+             pose proof (@Compile.rewrite_rules_goodT_by_curried _ _ _ _ _ rew1 rew2 eq_refl) as H;
+             let data := lazymatch rew1 with rewrite_rules ?data _ => data end in
+             let h := head data in
+             cbv [h rewrite_rules] in H;
+             let h' := lazymatch type of H with
+                       | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => head rew1
+                       end in
+             let pident_arg_types
+                 := lazymatch type of H with
+                    | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => pident_arg_types
+                    end in
+             cbv [h' pident_arg_types Compile.rewrite_rules_goodT_curried_cps] in H;
+             (* make [Qed] not take forever by explicitly recording a cast node *)
+             let H' := fresh in
+             pose proof H as H'; clear H;
+             apply H'; clear H'; intros
+        end.
 
       Local Ltac fin_wf :=
         repeat first [ progress intros
@@ -286,15 +153,16 @@ Module Compilers.
                      | progress intros
                      | progress fin_wf ].
 
+      Local Notation nbe_rewrite_rules := (rewrite_rules nbe_rewriter_data _).
       Lemma nbe_rewrite_rules_good
         : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules.
       Proof using Type.
         Time start_good.
-        Time all: handle_reified_rewrite_rules; handle_extra_nbe.
+        Time all: abstract (handle_reified_rewrite_rules; handle_extra_nbe).
       Qed.
 
       Local Ltac handle_extra_arith_rules :=
-        repeat first [ progress cbv [rwhenl option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast]
+        repeat first [ progress cbv [option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] in *
                      | break_innermost_match_step
                      | match goal with
                        | [ Hwf : Compile.wf_value _ ?x _, H : context[SubstVarLike.is_recursively_var_or_ident _ ?x] |- _ ] => erewrite SubstVarLike.wfT_is_recursively_var_or_ident in H by exact Hwf
@@ -302,37 +170,42 @@ Module Compilers.
                      | congruence
                      | progress fin_wf ].
 
+      Local Notation arith_rewrite_rules max_const := (rewrite_rules (arith_rewriter_data max_const) _).
       Lemma arith_rewrite_rules_good max_const
         : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const).
       Proof using Type.
         Time start_good.
         Time all: handle_reified_rewrite_rules; handle_extra_arith_rules.
-      Qed.
+      Time Qed.
 
+      Local Notation arith_with_casts_rewrite_rules := (rewrite_rules arith_with_casts_rewriter_data _).
       Lemma arith_with_casts_rewrite_rules_good
         : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules.
       Proof using Type.
         Time start_good.
         Time all: handle_reified_rewrite_rules.
-      Qed.
+      Time Qed.
 
+      Local Notation strip_literal_casts_rewrite_rules := (rewrite_rules strip_literal_casts_rewriter_data _).
       Lemma strip_literal_casts_rewrite_rules_good
         : rewrite_rules_goodT strip_literal_casts_rewrite_rules strip_literal_casts_rewrite_rules.
       Proof using Type.
         Time start_good.
         Time all: handle_reified_rewrite_rules.
-      Qed.
+      Time Qed.
 
+      Local Notation fancy_rewrite_rules invert_low invert_high := (rewrite_rules (fancy_rewriter_data invert_low invert_high) _).
       Lemma fancy_rewrite_rules_good
             (invert_low invert_high : Z -> Z -> option Z)
             (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
             (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
-        : rewrite_rules_goodT fancy_rewrite_rules fancy_rewrite_rules.
+        : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high).
       Proof using Type.
         Time start_good.
         Time all: handle_reified_rewrite_rules.
-      Qed.
+      Time Qed.
 
+      Local Notation fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range := (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _).
       Lemma fancy_with_casts_rewrite_rules_good
             (invert_low invert_high : Z -> Z -> option Z)
             (value_range flag_range : ZRange.zrange)
@@ -342,7 +215,7 @@ Module Compilers.
       Proof using Type.
         Time start_good.
         Time all: handle_reified_rewrite_rules.
-      Qed.
+      Time Qed.
     End good.
   End RewriteRules.
 End Compilers.