Integrate Wf and Interp proofs

Now the only admits remaining in Toplevel1 are glue ones about
freeze/to_bytes/from_bytes/fe_nonzero.  What remains (beyond those
admits, and the ones about word-by-word montgomery building blocks in
Arithmetic), are the proofs about abstract interpretation and the
rewriter.

After     | File Name                                                | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------
12m13.17s | Total                                                    | 11m45.42s || +0m27.75s | +3.93%
--------------------------------------------------------------------------------------------------------
3m47.20s  | Experiments/NewPipeline/Toplevel1                        | 3m27.51s  || +0m19.68s | +9.48%
0m17.98s  | Experiments/NewPipeline/UnderLetsProofs                  |    N/A    || +0m17.98s | ∞
   N/A    | Experiments/NewPipeline/UnderLetsWf                      | 0m17.94s  || -0m17.94s | -100.00%
4m49.57s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples       | 4m45.22s  || +0m04.34s | +1.52%
1m16.28s  | Experiments/NewPipeline/Toplevel2                        | 1m13.33s  || +0m02.95s | +4.02%
0m02.96s  | Experiments/NewPipeline/MiscCompilerPassesProofs         |    N/A    || +0m02.96s | ∞
   N/A    | Experiments/NewPipeline/MiscCompilerPassesWf             | 0m02.91s  || -0m02.91s | -100.00%
0m58.32s  | Experiments/NewPipeline/Rewriter                         | 0m58.58s  || -0m00.25s | -0.44%
0m28.19s  | Experiments/NewPipeline/LanguageInversion                | 0m28.02s  || +0m00.17s | +0.60%
0m13.14s  | Experiments/NewPipeline/LanguageWf                       | 0m13.09s  || +0m00.05s | +0.38%
0m10.11s  | Experiments/NewPipeline/CStringification                 | 0m10.12s  || -0m00.00s | -0.09%
0m01.21s  | Experiments/NewPipeline/CLI                              | 0m01.19s  || +0m00.02s | +1.68%
0m01.11s  | Experiments/NewPipeline/StandaloneOCamlMain              | 0m01.13s  || -0m00.01s | -1.76%
0m01.09s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.08s  || +0m00.01s | +0.92%
0m01.05s  | Experiments/NewPipeline/StandaloneHaskellMain            | 0m01.07s  || -0m00.02s | -1.86%
0m00.98s  | Experiments/NewPipeline/Language                         | 0m00.96s  || +0m00.02s | +2.08%
0m00.96s  | Experiments/NewPipeline/AbstractInterpretation           | 0m00.90s  || +0m00.05s | +6.66%
0m00.90s  | Experiments/NewPipeline/CompilersTestCases               | 0m00.92s  || -0m00.02s | -2.17%
0m00.66s  | Experiments/NewPipeline/RewriterProofs                   |    N/A    || +0m00.66s | ∞
0m00.64s  | Experiments/NewPipeline/MiscCompilerPasses               | 0m00.65s  || -0m00.01s | -1.53%
0m00.42s  | Experiments/NewPipeline/UnderLets                        | 0m00.38s  || +0m00.03s | +10.52%
0m00.40s  | Experiments/NewPipeline/AbstractInterpretationProofs     | 0m00.42s  || -0m00.01s | -4.76%

1 files changed, 45 insertions, 1 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index c8b19a5f4..4f4a2f473 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -26,6 +26,10 @@ Module Compilers.
   Import Language.Compilers.
   Import LanguageInversion.Compilers.
   Import expr.Notations.
+
+  Create HintDb wf discriminated.
+  Create HintDb interp discriminated.
+
   Module type.
     Section eqv.
       Context {base_type} {interp_base_type : base_type -> Type}.
@@ -43,6 +47,37 @@ Module Compilers.
         etransitivity; first [ eassumption | symmetry; eassumption ].
       Qed.
     End eqv.
+
+    Section app_curried_instances.
+      Context {base_type} {base_interp : base_type -> Type}.
+      (* Might want to add the following to make [app_curried_Proper] usable by [setoid_rewrite]? *)
+      (* See https://github.com/coq/coq/issues/8179
+<<
+Lemma PER_valid_l {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R x.
+Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
+Lemma PER_valid_r {A} {R : relation A} {HS : Symmetric R} {HT : Transitive R} x y (H : R x y) : Proper R y.
+Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed.
+Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_l _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.
+Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto with nocore ] ] : typeclass_instances.
+>>
+*)
+      Lemma app_curried_Proper {t}
+        : Proper (@type.eqv base_type base_interp t ==> type.and_for_each_lhs_of_arrow (@type.eqv _ _) ==> eq)
+                 (@type.app_curried base_type base_interp t).
+      Proof.
+        cbv [Proper respectful]; induction t; cbn [type.eqv type.app_curried]; cbv [Proper respectful]; [ intros; subst; reflexivity | ].
+        intros f g Hfg x y [Hxy ?]; eauto.
+      Qed.
+      Global Instance and_for_each_lhs_of_arrow_Reflexive {f} {R} {_ : forall t, Reflexive (R t)} {t}
+        : Reflexive (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Reflexive] in *; induction t; cbn; repeat split; eauto. Qed.
+      Global Instance and_for_each_lhs_of_arrow_Symmetric {f} {R} {_ : forall t, Symmetric (R t)} {t}
+        : Symmetric (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Symmetric] in *; induction t; cbn; repeat split; intuition eauto. Qed.
+      Global Instance and_for_each_lhs_of_arrow_Transitive {f} {R} {_ : forall t, Transitive (R t)} {t}
+        : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t).
+      Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed.
+    End app_curried_instances.
   End type.
 
   Module ident.
@@ -444,6 +479,11 @@ Module Compilers.
     Notation Interp_Reify := Interp_Reify_as.
   End expr.
 
+  Hint Resolve expr.Wf_Reify : wf.
+  Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list : interp.
+
+  Notation Wf := expr.Wf.
+
   Local Ltac destructure_step :=
     first [ progress subst
           | progress inversion_option
@@ -798,6 +838,10 @@ Module Compilers.
 
   Ltac prove_Wf _ :=
     lazymatch goal with
-    | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_compute; split; reflexivity
+    | [ |- expr.Wf ?e ] => apply (@GeneralizeVar.Wf_via_flat _ e); vm_cast_no_check (conj (eq_refl e) (eq_refl true))
     end.
+
+  Global Hint Extern 0 (?x == ?x) => apply expr.Wf_Interp_Proper : wf interp.
+  Hint Resolve GeneralizeVar.Wf_FromFlat_ToFlat GeneralizeVar.Wf_GeneralizeVar : wf.
+  Hint Rewrite @GeneralizeVar.Interp_GeneralizeVar @GeneralizeVar.Interp_FromFlat_ToFlat : interp.
 End Compilers.