Finish reifying list lemmas

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
22m23.84s | Total                                        | 21m34.63s || +0m49.21s | +3.80%
--------------------------------------------------------------------------------------------
1m52.62s  | RewriterRulesInterpGood.vo                   | 1m37.14s  || +0m15.48s | +15.93%
3m25.91s  | p384_32.c                                    | 3m14.24s  || +0m11.66s | +6.00%
1m32.94s  | RewriterRulesGood.vo                         | 1m42.36s  || -0m09.42s | -9.20%
0m33.72s  | RewriterWf1.vo                               | 0m24.30s  || +0m09.41s | +38.76%
1m17.31s  | Rewriter.vo                                  | 1m12.10s  || +0m05.21s | +7.22%
0m43.01s  | ExtractionHaskell/unsaturated_solinas        | 0m39.84s  || +0m03.16s | +7.95%
0m45.21s  | p521_32.c                                    | 0m42.86s  || +0m02.35s | +5.48%
1m46.30s  | Fancy/Barrett256.vo                          | 1m45.08s  || +0m01.21s | +1.16%
0m38.74s  | p521_64.c                                    | 0m37.49s  || +0m01.25s | +3.33%
0m23.16s  | ExtractionOCaml/word_by_word_montgomery      | 0m21.44s  || +0m01.71s | +8.02%
0m18.74s  | p256_32.c                                    | 0m16.88s  || +0m01.85s | +11.01%
0m15.00s  | ExtractionOCaml/unsaturated_solinas          | 0m13.98s  || +0m01.01s | +7.29%
0m11.92s  | ExtractionOCaml/saturated_solinas            | 0m10.13s  || +0m01.78s | +17.67%
0m07.82s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.98s  || +0m01.83s | +30.76%
1m47.42s  | RewriterWf2.vo                               | 1m47.81s  || -0m00.39s | -0.36%
0m58.35s  | ExtractionHaskell/word_by_word_montgomery    | 0m57.41s  || +0m00.94s | +1.63%
0m45.47s  | RewriterInterpProofs1.vo                     | 0m45.67s  || -0m00.20s | -0.43%
0m37.34s  | Fancy/Montgomery256.vo                       | 0m37.09s  || +0m00.25s | +0.67%
0m36.14s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m36.52s  || -0m00.38s | -1.04%
0m29.91s  | ExtractionHaskell/saturated_solinas          | 0m29.70s  || +0m00.21s | +0.70%
0m26.77s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m26.72s  || +0m00.05s | +0.18%
0m25.87s  | SlowPrimeSynthesisExamples.vo                | 0m25.49s  || +0m00.38s | +1.49%
0m18.72s  | p448_solinas_64.c                            | 0m19.16s  || -0m00.44s | -2.29%
0m16.94s  | secp256k1_32.c                               | 0m17.18s  || -0m00.23s | -1.39%
0m13.92s  | p434_64.c                                    | 0m13.08s  || +0m00.83s | +6.42%
0m13.15s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m12.58s  || +0m00.57s | +4.53%
0m08.97s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m08.95s  || +0m00.02s | +0.22%
0m08.37s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s  || -0m00.14s | -1.64%
0m08.35s  | p224_32.c                                    | 0m08.10s  || +0m00.25s | +3.08%
0m07.77s  | p384_64.c                                    | 0m07.29s  || +0m00.47s | +6.58%
0m06.92s  | BoundsPipeline.vo                            | 0m06.85s  || +0m00.07s | +1.02%
0m05.70s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m06.14s  || -0m00.43s | -7.16%
0m05.12s  | ExtractionHaskell/saturated_solinas.hs       | 0m06.09s  || -0m00.96s | -15.92%
0m03.53s  | PushButtonSynthesis/Primitives.vo            | 0m03.55s  || -0m00.02s | -0.56%
0m03.38s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.34s  || +0m00.04s | +1.19%
0m03.16s  | PushButtonSynthesis/BarrettReduction.vo      | 0m03.24s  || -0m00.08s | -2.46%
0m03.06s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m03.23s  || -0m00.16s | -5.26%
0m02.81s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m02.84s  || -0m00.02s | -1.05%
0m02.62s  | curve25519_32.c                              | 0m02.22s  || +0m00.39s | +18.01%
0m01.88s  | p224_64.c                                    | 0m01.47s  || +0m00.40s | +27.89%
0m01.68s  | curve25519_64.c                              | 0m02.19s  || -0m00.51s | -23.28%
0m01.32s  | CLI.vo                                       | 0m01.33s  || -0m00.01s | -0.75%
0m01.24s  | secp256k1_64.c                               | 0m01.30s  || -0m00.06s | -4.61%
0m01.22s  | p256_64.c                                    | 0m01.47s  || -0m00.25s | -17.00%
0m01.16s  | RewriterProofs.vo                            | 0m01.16s  || +0m00.00s | +0.00%
0m01.10s  | StandaloneHaskellMain.vo                     | 0m01.00s  || +0m00.10s | +10.00%
0m01.05s  | CompilersTestCases.vo                        | 0m01.09s  || -0m00.04s | -3.66%
0m01.04s  | StandaloneOCamlMain.vo                       | 0m01.04s  || +0m00.00s | +0.00%

1 files changed, 300 insertions, 0 deletions

diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index 49af85a60..411287bcc 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -27,6 +27,7 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Sigma.Related.
 Require Import Crypto.Util.ListUtil.SetoidList.
+Require Import Crypto.Util.ListUtil.Forall.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Logic.ExistsEqAnd.
@@ -2569,5 +2570,304 @@ Module Compilers.
         End with_interp.
       End with_var.
     End Compile.
+
+    Module Reify.
+      Import Compile.
+      Import Rewriter.Compilers.RewriteRules.Compile.
+      Import Rewriter.Compilers.RewriteRules.Reify.
+
+      Local Notation type := (type.type base.type).
+      Local Notation expr := (@expr.expr base.type ident).
+      Local Notation value := (@value base.type ident).
+      Local Notation UnderLets := (@UnderLets.UnderLets base.type ident).
+
+      Ltac wf_ctors :=
+        repeat first [ match goal with
+                       | [ |- UnderLets.wf _ _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor
+                       | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor
+                       | [ |- expr.wf ?seg (#_) (#_) ]
+                         => (tryif is_evar seg then instantiate (1:=nil) else idtac);
+                            constructor
+                       | [ |- expr.wf _ ($_) ($_) ] => constructor
+                       | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros
+                       | [ |- expr.wf _ (UnderLets.to_expr _) (UnderLets.to_expr _) ] => apply UnderLets.wf_to_expr
+                       | [ H : expr.wf ?G ?x ?y |- expr.wf ?seg ?x ?y ] => first [ is_evar seg | constr_eq G seg ]; exact H
+                       | [ H : List.Forall2 (expr.wf _) ?x ?y |- List.Forall2 (expr.wf _) ?x ?y ]
+                         => eapply Forall2_Proper_impl; [ | reflexivity | reflexivity | exact H ]; repeat intro
+                       | [ H : List.Forall2 (expr.wf ?G) ?x ?y |- List.Forall2 (expr.wf ?seg) ?x ?y ]
+                         => first [ is_evar seg | constr_eq seg G ]; exact H
+                       | [ H : List.Forall2 ?P ?x ?y |- List.Forall2 ?Pe ?x ?y ]
+                         => first [ is_evar Pe | constr_eq Pe P ]; exact H
+                       | [ H : forall x y, List.In (x, y) ?G -> expr.wf ?G' x y, H' : List.In (?v1, ?v2) ?G |- expr.wf ?seg ?v1 ?v2 ]
+                         => first [ is_evar seg | constr_eq seg G' ]; exact (H _ _ H')
+                       | [ |- expr.wf _ (reify_list _) (reify_list _) ]
+                         => rewrite expr.wf_reify_list
+                       | [ H : expr.wf _ (reify_list ?xs) (reify_list ?ys) |- List.Forall2 _ ?xs ?xy ]
+                         => rewrite expr.wf_reify_list in H
+                       | [ |- ?G ] => tryif has_evar G then fail else solve [ destruct_head'_ex; subst; wf_t ]
+                       end ].
+      Ltac handle_wf_rec do_try :=
+        let tac _
+            := solve
+                 [ repeat
+                     first
+                     [ progress wf_ctors
+                     | handle_wf_rec do_try
+                     | match goal with
+                       | [ |- List.In ?v ?seg ] => is_evar seg; unify seg (cons v nil)
+                       | [ |- List.In ?v (?seg1 ++ ?seg2) ]
+                         => rewrite in_app_iff;
+                            first [ is_evar seg1; left
+                                  | is_evar seg2; right ]
+                       (*| [ |- ?x ++ ?y = ?x ++ ?z ] => apply f_equal2*)
+                       | [ |- ?x = ?y ]
+                         => is_evar x; tryif has_evar y then fail else reflexivity
+                       | [ |- forall t v1 v2, List.In (existT _ t (v1, v2)) (?x ++ ?G1) -> List.In (existT _ t (v1, v2)) (?x ++ ?G2) ]
+                         => is_evar G2;
+                            tryif first [ has_evar x | has_evar G1 ] then fail else (do 3 intro; exact id)
+                       end ] ] in
+        match goal with
+        | [ H : expr.wf ?segv ?x1 ?x2
+            |- UnderLets.wf _ ?Gv (nat_rect _ _ _ _ ?x1) (nat_rect _ _ _ _ ?x2) ]
+          => unshelve
+               (eapply UnderLets.wf_Proper_list;
+                [ | | eapply @UnderLets.wf_nat_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ];
+                [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ];
+                [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ];
+                [ try match goal with |- _ = _ => shelve end.. ]);
+             shelve_unifiable;
+             do_try tac
+        | [ H : expr.wf ?segv ?x1 ?x2
+            |- UnderLets.wf _ ?Gv (list_rect _ _ _ _ ?x1) (list_rect _ _ _ _ ?x2) ]
+          => unshelve
+               (eapply UnderLets.wf_Proper_list;
+                [ | | eapply @UnderLets.wf_list_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ];
+                [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ];
+                [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ];
+                [ try match goal with |- _ = _ => shelve end.. ]);
+             shelve_unifiable;
+             do_try tac
+        | [ |- UnderLets.wf _ _ ?x ?y ]
+          => let f := head x in
+             let g := head y in
+             is_var f; is_var g;
+             unshelve
+               (lazymatch goal with
+                | [ H : context[UnderLets.wf _ _ (f _) (g _)] |- _ ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H ]
+                | [ H : context[UnderLets.wf _ _ (f _ _) (g _ _)] |- _ ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H ]
+                | [ H : context[UnderLets.wf _ _ (f _ _ _) (g _ _ _)] |- _ ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H ]
+                | [ H : context[UnderLets.wf _ _ (f _ _ _ _) (g _ _ _ _)] |- _ ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H ]
+                end;
+                [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ];
+                [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ];
+                [ try match goal with |- _ = _ => shelve end.. ]);
+             shelve_unifiable;
+             do_try tac
+        end.
+
+      Ltac reify_wf_t_step :=
+        first [ progress subst
+              | 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
+                end
+              | progress inversion_option
+              | progress destruct_head'_False
+              | progress intros
+              | progress cbn [invert_expr.invert_Literal invert_expr.ident.invert_Literal value' type.interp base.interp base.base_interp] in *
+              | match goal with
+                | [ H : ident.Literal _ = ident.Literal _ |- _ ]
+                  => pose proof (f_equal invert_expr.ident.invert_Literal H); clear H
+                end
+              | progress expr.inversion_wf_constr
+              | break_innermost_match_hyps_step
+              | progress expr.inversion_wf_one_constr
+              | progress expr.invert_subst
+              | progress expr.inversion_expr
+              | progress expr.invert_match
+              | progress wf_ctors
+              | match goal with
+                | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ]
+                  => apply UnderLets.wf_nat_rect; intros
+                | [ |- UnderLets.wf _ ?G (list_rect _ _ _ _) (list_rect _ _ _ _) ]
+                  => apply @UnderLets.wf_list_rect with (RA := expr.wf G)
+                | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ]
+                  => apply @UnderLets.wf_splice with (P := fun G => expr.wf G); intros; subst
+                | [ H : expr.wf _ (reify_list ?l1) (reify_list ?l2)
+                    |- expr.wf ?G (nth_default ?d1 ?l1 ?n) (nth_default ?d2 ?l2 ?n) ]
+                  => cut (List.Forall2 (expr.wf G) l1 l2 /\ expr.wf G d1 d2);
+                     [ rewrite Forall2_forall_iff'';
+                       let H := fresh in intro H; apply H
+                     | split ]
+                | [ |- ?x = ?x ] => reflexivity
+                end
+              | progress handle_wf_rec ltac:(fun tac => try tac (); tac ()) ].
+      Ltac reify_wf_t := repeat reify_wf_t_step.
+
+      Section with_var.
+        Context {var1 var2 : type -> Type}.
+
+        Lemma wf_reflect_ident_iota G {t} (idc : ident t)
+          : option_eq
+              (wf_value G)
+              (@reflect_ident_iota var1 t idc)
+              (@reflect_ident_iota var2 t idc).
+        Proof using Type.
+          destruct idc; cbv [reflect_ident_iota option_eq]; try reflexivity.
+          all: cbv [wf_value wf_value']; intros; subst; break_innermost_match; cbn [reify reflect] in *;
+            lazymatch 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
+            | _ => idtac
+            end;
+            expr.invert_subst; subst.
+          all: reify_wf_t.
+        Qed.
+
+        Lemma wf_reflect_expr_beta_iota
+              {ident}
+              {reflect_ident_iota1 reflect_ident_iota2}
+              (Hwf_reflect_ident_iota
+               : forall G {t} (idc : ident t),
+                  option_eq
+                    (@wf_value _ ident var1 var2 G _)
+                    (@reflect_ident_iota1 t idc)
+                    (@reflect_ident_iota2 t idc))
+              G G'
+              (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2)
+              {t} e1 e2
+              (Hwf : expr.wf G' e1 e2)
+          : UnderLets.wf
+              (fun G'' => wf_value G'')
+              G
+              (@reflect_expr_beta_iota ident var1 reflect_ident_iota1 t e1)
+              (@reflect_expr_beta_iota ident var2 reflect_ident_iota2 t e2).
+        Proof using Type.
+          revert G HG'; induction Hwf; cbn [reflect_expr_beta_iota]; intros.
+          all: repeat first [ match goal with
+                              | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                              | [ |- expr.wf _ _ _ ] => constructor
+                              | [ |- wf_value' _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor
+                              | [ Hwf_reflect_ident_iota : forall G t' idc', option_eq (wf_value G) (?reflect_ident_iota1 t' idc') (?reflect_ident_iota2 t' idc'),
+                                    H1 : ?reflect_ident_iota1 ?t ?idc = _, H2 : ?reflect_ident_iota2 ?t ?idc = _ |- _ ]
+                                => let H' := fresh in
+                                   pose proof (fun G => Hwf_reflect_ident_iota G t idc) as H';
+                                   rewrite H1, H2 in H'; clear H1 H2; cbv [option_eq] in H'
+                              | [ H : list _ -> ?T |- _ ] => specialize (H nil)
+                              | [ |- UnderLets.wf ?Pv ?Gv (UnderLets.splice _ _) (UnderLets.splice _ _) ]
+                                => apply @UnderLets.wf_splice with (P:=fun G => wf_value G); intros; subst
+                              | [ H : context[reflect_expr_beta_iota] |- UnderLets.wf _ _ (reflect_expr_beta_iota _ _) (reflect_expr_beta_iota _ _) ]
+                                => apply H; intros
+                              | [ |- wf_value _ (fun x => _) (fun y => _) ] => hnf; intros; subst
+                              | [ |- wf_value' _ (splice_under_lets_with_value _ _) (splice_under_lets_with_value _ _) ]
+                                => apply wf_splice_under_lets_with_value
+                              | [ |- UnderLets.wf (fun G a1 a2 => wf_value_with_lets G (Base_value a1) (Base_value a2)) ?G' ?x ?y ]
+                                => cut (UnderLets.wf (fun G => wf_value G) G' x y);
+                                   [ apply UnderLets.wf_Proper_list_impl; cbv [wf_value_with_lets Base_value]
+                                   | ]
+                              end
+                            | progress destruct_head'_False
+                            | progress inversion_option
+                            | solve [ auto ]
+                            | break_innermost_match_step
+                            | apply wf_reflect
+                            | apply wf_reify
+                            | progress intros
+                            | progress cbn [List.In eq_rect fst snd] in *
+                            | progress destruct_head'_or
+                            | progress inversion_sigma
+                            | progress subst
+                            | progress inversion_prod
+                            | cbn [wf_value wf_value'] in *;
+                              handle_wf_rec ltac:(fun tac => try tac (); try eassumption; tac ())
+                            | eapply wf_value'_Proper_list; [ | match goal with H : _ |- _ => now eapply H end ]; solve [ destruct_head'_ex; subst; wf_t ]
+                            | match goal with
+                              | [ H : wf_value _ ?f ?g |- wf_value _ (?f _) (?g _) ]
+                                => eapply wf_value'_Proper_list; revgoals; [ hnf in H; eapply H; revgoals | ]; try eassumption; try reflexivity; now destruct_head'_ex; subst; wf_t
+                              end ].
+        Qed.
+
+        Lemma wf_reify_expr_beta_iota
+              {ident}
+              {reflect_ident_iota1 reflect_ident_iota2}
+              (Hwf_reflect_ident_iota
+               : forall G {t} (idc : ident t),
+                  option_eq
+                    (@wf_value _ ident var1 var2 G _)
+                    (@reflect_ident_iota1 t idc)
+                    (@reflect_ident_iota2 t idc))
+              G G'
+              (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2)
+              {t} e1 e2
+              (Hwf : expr.wf G' e1 e2)
+          : UnderLets.wf
+              (fun G'' => expr.wf G'')
+              G
+              (@reify_expr_beta_iota ident var1 reflect_ident_iota1 t e1)
+              (@reify_expr_beta_iota ident var2 reflect_ident_iota2 t e2).
+        Proof using Type.
+          cbv [reify_expr_beta_iota reify_to_UnderLets].
+          eapply @UnderLets.wf_splice with (P := fun G => wf_value G);
+            intros; destruct_head'_ex; subst.
+          all: repeat first [ break_innermost_match_step
+                            | progress cbn [reflect reify] in *
+                            | progress fold (@reflect ident var1) (@reflect ident var2)
+                            | progress fold (@reify ident var1) (@reify ident var2)
+                            | progress intros
+                            | assumption
+                            | apply wf_reify
+                            | apply wf_reflect
+                            | eapply wf_reflect_expr_beta_iota
+                            | match goal with
+                              | [ |- List.In ?x ?seg ] => is_evar seg; unify seg (cons x nil); left
+                              end
+                            | constructor
+                            | match goal with H : _ |- _ => eapply H; revgoals; clear H end ].
+        Qed.
+
+        Lemma wf_expr_value_to_rewrite_rule_replacement
+              {ident}
+              {reflect_ident_iota1 reflect_ident_iota2}
+              (Hwf_reflect_ident_iota
+               : forall G {t} (idc : ident t),
+                  option_eq
+                    (@wf_value _ ident var1 var2 G _)
+                    (@reflect_ident_iota1 t idc)
+                    (@reflect_ident_iota2 t idc))
+              (should_do_again : bool)
+              G {t} e1 e2
+              (Hwf : @wf_maybe_do_again_expr ident var1 var2 t true true G e1 e2)
+          : UnderLets.wf
+              (fun G' => @wf_maybe_do_again_expr ident var1 var2 t should_do_again should_do_again G')
+              G
+              (@expr_value_to_rewrite_rule_replacement ident var1 reflect_ident_iota1 should_do_again t e1)
+              (@expr_value_to_rewrite_rule_replacement ident var2 reflect_ident_iota2 should_do_again t e2).
+        Proof using Type.
+          cbv [expr_value_to_rewrite_rule_replacement].
+          eapply @UnderLets.wf_splice with (P := @wf_maybe_do_again_expr ident var1 var2 _ true true); intros; destruct_head'_ex; subst.
+          { destruct Hwf as [G' [HG' Hwf] ].
+            eapply UnderLets.wf_flat_map;
+              cbv [wf_value] in *;
+              eauto using wf_value'_Proper_list, UnderLets.wf_of_expr, wf_reify_expr_beta_iota.
+            { intros; eapply wf_reflect; now repeat constructor. } }
+          { repeat first [ progress cbv [wf_maybe_do_again_expr] in *
+                         | break_innermost_match_step
+                         | progress destruct_head'_ex
+                         | progress destruct_head'_and
+                         | progress subst
+                         | eapply wf_reify_expr_beta_iota; try eassumption
+                         | constructor
+                         | solve [ eauto ] ]. }
+        Qed.
+      End with_var.
+    End Reify.
   End RewriteRules.
 End Compilers.