Finish rule-specific rewriter wf proofs

But don't run them yet, because they are really slow

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
19m35.38s | Total                                                                | 19m35.69s || -0m00.30s | -0.02%
--------------------------------------------------------------------------------------------------------------------
5m57.04s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m58.04s  || -0m01.00s | -0.27%
1m12.61s  | Experiments/NewPipeline/RewriterWf2                                  | 1m11.61s  || +0m01.00s | +1.39%
4m32.41s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.28s  || -0m00.87s | -0.31%
1m38.38s  | Experiments/NewPipeline/Toplevel2                                    | 1m38.56s  || -0m00.18s | -0.18%
1m16.21s  | Experiments/NewPipeline/RewriterRulesGood                            | 1m16.18s  || +0m00.03s | +0.03%
0m39.26s  | p521_32.c                                                            | 0m39.50s  || -0m00.24s | -0.60%
0m37.34s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.33s  || +0m00.01s | +0.02%
0m34.83s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m35.33s  || -0m00.50s | -1.41%
0m32.68s  | p521_64.c                                                            | 0m32.73s  || -0m00.04s | -0.15%
0m23.62s  | p384_32.c                                                            | 0m23.67s  || -0m00.05s | -0.21%
0m21.00s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.22s  || +0m00.78s | +3.85%
0m18.92s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.62s  || +0m00.30s | +1.61%
0m13.79s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.70s  || +0m00.08s | +0.65%
0m10.70s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.51s  || +0m00.18s | +1.80%
0m08.55s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.59s  || -0m00.03s | -0.46%
0m08.43s  | p384_64.c                                                            | 0m08.54s  || -0m00.10s | -1.28%
0m05.62s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.34s  || +0m00.28s | +5.24%
0m05.47s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.48s  || -0m00.01s | -0.18%
0m04.40s  | Experiments/NewPipeline/RewriterWf1                                  | 0m04.36s  || +0m00.04s | +0.91%
0m03.97s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m03.89s  || +0m00.08s | +2.05%
0m03.95s  | secp256k1_32.c                                                       | 0m03.91s  || +0m00.04s | +1.02%
0m03.92s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.01s  || -0m00.08s | -2.24%
0m03.78s  | p256_32.c                                                            | 0m03.77s  || +0m00.00s | +0.26%
0m03.31s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.13s  || +0m00.18s | +5.75%
0m02.14s  | curve25519_32.c                                                      | 0m02.11s  || +0m00.03s | +1.42%
0m02.14s  | p224_32.c                                                            | 0m02.23s  || -0m00.08s | -4.03%
0m01.55s  | p224_64.c                                                            | 0m01.69s  || -0m00.13s | -8.28%
0m01.54s  | p256_64.c                                                            | 0m01.52s  || +0m00.02s | +1.31%
0m01.52s  | curve25519_64.c                                                      | 0m01.43s  || +0m00.09s | +6.29%
0m01.49s  | secp256k1_64.c                                                       | 0m01.65s  || -0m00.15s | -9.69%
0m01.40s  | Experiments/NewPipeline/CLI                                          | 0m01.41s  || -0m00.01s | -0.70%
0m01.29s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.23s  || +0m00.06s | +4.87%
0m01.24s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.18s  || +0m00.06s | +5.08%
0m00.88s  | Experiments/NewPipeline/RewriterProofs                               | 0m00.94s  || -0m00.05s | -6.38%

4 files changed, 61 insertions, 67 deletions

diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v
index 2632560be..d0d106a02 100644
--- a/src/Experiments/NewPipeline/RewriterProofs.v
+++ b/src/Experiments/NewPipeline/RewriterProofs.v
@@ -66,8 +66,7 @@ Module Compilers.
       pattern.ident.internal_ident_dec_bl,
       pattern.ident.try_make_transport_ident_cps_correct,
       pattern.ident.eta_ident_cps_correct
-        with nocore;
-      [ .. | intros; eapply UnderLets.wf_Proper_list; [ | | eapply wf_do_again; assumption ]; solve [ wf_t ] ].
+        with nocore.
     Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 :=
       start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0.
 
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 605cbf5ca..3bdfa9913 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -166,28 +166,27 @@ Module Compilers.
             N1 N2 C1 C2 ls1 ls2 G
             (Hwf : expr.wf G ls1 ls2)
             (HN : UnderLets.wf (fun G' v1 v2
-                                => forall G'',
+                                => 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)
+                                    /\ 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)
-                -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                          -> expr.wf G'' rec1 rec2)
+                -> (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
-                                => forall 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))
+                                 => 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 (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P),
-                            forall G'',
-                              (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                              -> expr.wf G''
-                                        (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
-                                        (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
+                        => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'',
+                            (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                            /\ expr.wf G''
+                                       (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
+                                       (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
                        G)
                     (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1 _ id)
                     (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2 _ id).
@@ -199,8 +198,8 @@ Module Compilers.
         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
+                                       | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                 exfalso; clear -H H'; congruence
                             | [ |- UnderLets.wf _ _ _ _ ] => constructor
                             | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
                             end
@@ -208,10 +207,11 @@ Module Compilers.
                           | progress cbn [sequence_return option_eq]
                           | assumption
                           | reflexivity
+                          | (exists eq_refl)
                           | apply @UnderLets.wf_splice with (P:=fun G' v1 v2
-                                                                => forall G'',
+                                                                => exists G'',
                                                                     (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                                                    -> expr.wf G'' v1 v2)
+                                                                    /\ expr.wf G'' v1 v2)
                           | progress intros ].
         lazymatch goal with
         | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ]
@@ -223,8 +223,8 @@ Module Compilers.
         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
+                                       | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                 exfalso; clear -H H'; congruence
                             | [ |- UnderLets.wf _ _ _ _ ] => constructor
                             end
                           | progress expr.invert_subst
@@ -235,9 +235,9 @@ Module Compilers.
                           | solve [ auto ]
                           | progress subst
                           | apply @UnderLets.wf_splice with (P:=fun G' v1 v2
-                                                                => forall G'',
+                                                                => exists G'',
                                                                     (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                                                    -> expr.wf G'' v1 v2)
+                                                                    /\ expr.wf G'' v1 v2)
                           | progress intros
                           | wf_safe_t_step
                           | progress type.inversion_type
@@ -248,28 +248,27 @@ Module Compilers.
             N1 N2 C1 C2 ls1 ls2 G
             (Hwf : expr.wf G ls1 ls2)
             (HN : UnderLets.wf (fun G' x1 x2
-                                => forall G'',
+                                => exists G'',
                                     (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                    -> Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2)
+                                    /\ Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) 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)
-                -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                          -> expr.wf G'' rec1 rec2)
+                -> (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
-                                => forall G'',
+                                => exists G'',
                                     (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                                    -> expr.wf 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 (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P),
-                            forall G'',
-                              (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
-                              -> expr.wf G''
-                                        (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
-                                        (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
+                        => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P) G'',
+                            (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                            /\ expr.wf G''
+                                       (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
+                                       (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
                        G)
                     (@rlist_rect_cast var1 A A' P (@Compile.value _ ident var1) N1 C1 ls1 _ id)
                     (@rlist_rect_cast var2 A A' P (@Compile.value _ ident var2) N2 C2 ls2 _ id).
@@ -280,7 +279,8 @@ Module Compilers.
         apply wf_rlist_rectv; auto.
         eapply UnderLets.wf_Proper_list_impl; [ | | eassumption ]; trivial; cbn; intros ? ? ? H.
         repeat let x := fresh in intro x; specialize (H x).
-        inversion H; inversion_sigma; type.inversion_type; subst; assumption.
+        destruct H as [? [H0 H1] ].
+        inversion H1; inversion_sigma; type.inversion_type; subst; eauto.
       Qed.
 
 
@@ -394,16 +394,6 @@ Module Compilers.
         eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto).
       Qed.
 
-      (** TODO: MOVE ME *)
-      Lemma combine_repeat {A B} (a : A) (b : B) n : combine (repeat a n) (repeat b n) = repeat (a, b) n.
-      Proof. induction n; cbn; congruence. Qed.
-      Lemma combine_rev_rev_samelength {A B} ls1 ls2 : length ls1 = length ls2 -> @combine A B (rev ls1) (rev ls2) = rev (combine ls1 ls2).
-      Proof.
-        revert ls2; induction ls1 as [|? ? IHls1], ls2; cbn in *; try congruence; intros.
-        rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine].
-        reflexivity.
-      Qed.
-
       Local Ltac start_good cps_id rewrite_rules :=
         split; [ reflexivity | ];
         repeat apply conj; try solve [ eapply cps_id ]; [];
@@ -547,6 +537,13 @@ Module Compilers.
                   => is_evar R; revert H; instantiate (1:=fun G' => expr.wf G'); solve [ auto ]
                 | [ H : expr.wf ?G ?a ?b |- ?R ?G ?a ?b ]
                   => is_evar R; instantiate (1:=fun G' => expr.wf G'); solve [ auto ]
+                | [ |- (forall t v1 v2, In _ _ -> _) /\ expr.wf _ _ _ ] => apply conj; revgoals
+                | [ |- (forall t v1 v2, In _ _ -> _) /\ Compile.wf_anyexpr _ _ _ _ ] => apply conj; revgoals
+                | [ H : expr.wf _ ?x ?y |- Compile.wf_value _ ?x ?y ] => hnf
+                | [ |- Compile.wf_value _ ?x ?y ] => eapply Compile.wf_value'_Proper_list; [ | solve [ cbv [Compile.wf_value] in *; eauto ] ]; solve [ wf_t ]
+                | [ |- In ?x ?ls ] => is_evar ls; refine (or_introl eq_refl : In x (x :: _)); shelve
+                | [ |- or (_ = _) ?G ] => first [ left; reflexivity | has_evar G; right ]
+                | [ H : @In ?A _ ?ls |- _ ] => is_evar ls; unify ls (@nil A); cbn [In] in H
                 end
               | progress expr.invert_subst
               | solve [ wf_t ]
@@ -557,12 +554,9 @@ Module Compilers.
       Lemma nbe_rewrite_rules_good
         : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules.
       Proof.
-        (*Time start_good (@nbe_cps_id) (@nbe_rewrite_rules).
-        Set Ltac Profiling.
-        Time all: try solve [ repeat repeat good_t_step ].
-        Show Ltac Profile.
-        (*start_good (@nbe_cps_id) (@nbe_rewrite_rules).
-        all: repeat good_t_step.*)
+        (*
+        Time start_good (@nbe_cps_id) (@nbe_rewrite_rules).
+        Time all: repeat repeat good_t_step.
          *)
       Admitted.
 
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 0cbaaaacf..06c71e480 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -623,12 +623,11 @@ Module Compilers.
                                           | true, true
                                             => UnderLets.wf
                                                  (fun G' v1 v2
-                                                  => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t),
-                                                      forall G'',
-                                                        (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2')
-                                                        -> expr.wf G''
-                                                                   (rew [fun t : base.type => expr t] pf1 in unwrap v1)
-                                                                   (rew [fun t : base.type => expr t] pf2 in unwrap v2))
+                                                  => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t) G'',
+                                                      (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2')
+                                                      /\ expr.wf G''
+                                                                (rew [fun t : base.type => expr t] pf1 in unwrap v1)
+                                                                (rew [fun t : base.type => expr t] pf2 in unwrap v2))
                                                  G
                                           | false, false
                                             => UnderLets.wf (fun G' => wf_anyexpr G' t) G
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index bdad9d840..5d1bae6e4 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -484,7 +484,7 @@ Module Compilers.
                 (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t))
                 (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t))
                 (wf_do_again : forall G (t : base.type) e1 e2,
-                    expr.wf nil e1 e2
+                    (exists G', (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2) /\ expr.wf G' e1 e2)
                     -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2))
                 (d : @decision_tree pident)
                 (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2)
@@ -757,8 +757,9 @@ Module Compilers.
                     (Hrew : rewrite_rules_goodT rew1 rew2)
                     (do_again1 : forall t : base.type, @expr.expr base.type ident (@value var1) t -> @UnderLets var1 (@expr var1 t))
                     (do_again2 : forall t : base.type, @expr.expr base.type ident (@value var2) t -> @UnderLets var2 (@expr var2 t))
-                    (wf_do_again : forall G (t : base.type) e1 e2,
-                        expr.wf nil e1 e2
+                    (wf_do_again : forall G G' (t : base.type) e1 e2,
+                        (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2)
+                        -> expr.wf G' e1 e2
                         -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)).
 
             Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident full_types invert_bind_args type_of_pident pident_to_typed of_typed_ident arg_types bind_args try_make_transport_ident_cps dtree).
@@ -776,7 +777,8 @@ Module Compilers.
             Proof.
               revert dependent G; revert dependent re1; revert dependent re2; induction t as [t|s IHs d IHd];
                 intros; cbn [assemble_identifier_rewriters'].
-              { rewrite HK1, HK2; apply wf_eval_rewrite_rules; assumption. }
+              { rewrite HK1, HK2; apply wf_eval_rewrite_rules; try assumption.
+                intros; destruct_head'_ex; destruct_head'_and; eauto. }
               { hnf; intros; subst.
                 unshelve eapply IHd; cbn [type_of_rawexpr]; [ shelve | shelve | constructor | cbn; reflexivity | cbn; reflexivity ].
                 all: rewrite ?HK1, ?HK2.
@@ -903,9 +905,10 @@ Module Compilers.
                   do_again1
                   do_again2
                   (wf_do_again
-                   : forall (t : base.type) e1 e2,
-                      expr.wf nil e1 e2
-                      -> UnderLets.wf (fun G' => expr.wf G') nil (do_again1 t e1) (do_again2 t e2))
+                   : forall G G' (t : base.type) e1 e2,
+                      (forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> Compile.wf_value G v1 v2)
+                      -> expr.wf G' e1 e2
+                      -> UnderLets.wf (fun G' => expr.wf G') G (do_again1 t e1) (do_again2 t e2))
                   t (idc : ident t),
                   wf_value_with_lets nil (rewrite_head var1 do_again1 t idc) (rewrite_head var2 do_again2 t idc))
               fuel {t} (e : Expr t) (Hwf : Wf e)
@@ -913,7 +916,6 @@ Module Compilers.
       Proof.
         intros var1 var2; cbv [Rewrite]; eapply wf_rewrite with (G:=nil); [ | apply Hwf | wf_t ].
         intros; subst; eapply wf_value'_Proper_list; [ | eapply wf_rewrite_head ]; wf_t.
-        eapply wf_do_again; [ | eassumption ]; wf_t.
       Qed.
     End Compile.
   End RewriteRules.