Better transport lemmas in LanguageInversion

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
19m03.98s | Total                                                                | 19m03.09s || +0m00.89s | +0.07%
--------------------------------------------------------------------------------------------------------------------
4m32.38s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.84s  || -0m01.46s | -0.53%
0m24.50s  | Experiments/NewPipeline/UnderLetsProofs                              | 0m23.34s  || +0m01.16s | +4.97%
5m55.71s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.23s  || +0m00.47s | +0.13%
1m36.24s  | Experiments/NewPipeline/Toplevel2                                    | 1m36.50s  || -0m00.25s | -0.26%
0m39.34s  | p521_32.c                                                            | 0m39.28s  || +0m00.06s | +0.15%
0m38.62s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m38.04s  || +0m00.57s | +1.52%
0m37.21s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.13s  || +0m00.07s | +0.21%
0m35.25s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m35.00s  || +0m00.25s | +0.71%
0m34.16s  | Experiments/NewPipeline/LanguageInversion                            | 0m33.72s  || +0m00.43s | +1.30%
0m32.71s  | p521_64.c                                                            | 0m32.83s  || -0m00.11s | -0.36%
0m23.87s  | p384_32.c                                                            | 0m23.81s  || +0m00.06s | +0.25%
0m21.16s  | Experiments/NewPipeline/LanguageWf                                   | 0m21.12s  || +0m00.03s | +0.18%
0m20.25s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.41s  || -0m00.16s | -0.78%
0m18.58s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.61s  || -0m00.03s | -0.16%
0m13.59s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.53s  || +0m00.06s | +0.44%
0m10.33s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.46s  || -0m00.13s | -1.24%
0m08.56s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.54s  || +0m00.02s | +0.23%
0m08.47s  | p384_64.c                                                            | 0m08.43s  || +0m00.04s | +0.47%
0m05.43s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.50s  || -0m00.07s | -1.27%
0m05.39s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.32s  || +0m00.06s | +1.31%
0m04.01s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m04.04s  || -0m00.03s | -0.74%
0m04.00s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.01s  || -0m00.00s | -0.24%
0m03.90s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m03.96s  || -0m00.06s | -1.51%
0m03.84s  | Experiments/NewPipeline/MiscCompilerPassesProofs                     | 0m03.83s  || +0m00.00s | +0.26%
0m03.81s  | p256_32.c                                                            | 0m03.74s  || +0m00.06s | +1.87%
0m03.79s  | secp256k1_32.c                                                       | 0m03.90s  || -0m00.10s | -2.82%
0m03.13s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.15s  || -0m00.02s | -0.63%
0m02.09s  | curve25519_32.c                                                      | 0m02.16s  || -0m00.07s | -3.24%
0m02.08s  | p224_32.c                                                            | 0m02.24s  || -0m00.16s | -7.14%
0m01.69s  | p224_64.c                                                            | 0m01.55s  || +0m00.13s | +9.03%
0m01.58s  | secp256k1_64.c                                                       | 0m01.64s  || -0m00.05s | -3.65%
0m01.56s  | p256_64.c                                                            | 0m01.51s  || +0m00.05s | +3.31%
0m01.54s  | curve25519_64.c                                                      | 0m01.45s  || +0m00.09s | +6.20%
0m01.44s  | Experiments/NewPipeline/CLI                                          | 0m01.46s  || -0m00.02s | -1.36%
0m01.32s  | Experiments/NewPipeline/RewriterProofs                               | 0m01.38s  || -0m00.05s | -4.34%
0m01.26s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.23s  || +0m00.03s | +2.43%
0m01.19s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.20s  || -0m00.01s | -0.83%

1 files changed, 73 insertions, 62 deletions

diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index 825881771..962cabcea 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -90,8 +90,7 @@ Module Compilers.
 
     Local Ltac t_red :=
       repeat first [ progress intros
-                   | progress cbn [type.type_beq base.type.type_beq base.type.base_beq base.try_make_transport_cps base.try_make_base_transport_cps eq_rect andb] in *
-                   | progress cbv [cpsreturn cpsbind cps_option_bind Option.bind cpscall] in * ].
+                   | progress cbn [type.type_beq base.type.type_beq base.type.base_beq base.try_make_transport_cps base.try_make_base_transport_cps eq_rect andb] in * ].
     Local Ltac t :=
       repeat first [ progress t_red
                    | reflexivity
@@ -110,30 +109,33 @@ Module Compilers.
                      | [ H : _ |- _ ] => rewrite H
                      end ].
 
-    Lemma try_make_base_transport_cps_correct P t1 t2 T k
-      : base.try_make_base_transport_cps P t1 t2 T k
-        = k match Sumbool.sumbool_of_bool (base.type.base_beq t1 t2) with
-            | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_base_dec_bl _ _ pf) in id)
-            | right _ => None
-            end.
-    Proof. revert P t2 T k; induction t1, t2; t. Qed.
+    Lemma try_make_base_transport_cps_correct P t1 t2
+      : base.try_make_base_transport_cps P t1 t2
+        = fun T k
+          => k match Sumbool.sumbool_of_bool (base.type.base_beq t1 t2) with
+              | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_base_dec_bl _ _ pf) in id)
+              | right _ => None
+              end.
+    Proof. revert P t2; induction t1, t2; t. Qed.
 
-    Lemma try_make_transport_cps_correct P t1 t2 T k
-      : base.try_make_transport_cps P t1 t2 T k
-        = k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with
-            | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_type_dec_bl _ _ pf) in id)
-            | right _ => None
-            end.
-    Proof. revert P t2 T k; induction t1, t2; t_red; rewrite ?try_make_base_transport_cps_correct; t. Qed.
+    Lemma try_make_transport_cps_correct P t1 t2
+      : base.try_make_transport_cps P t1 t2
+        = fun T k
+          => k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with
+              | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_type_dec_bl _ _ pf) in id)
+              | right _ => None
+              end.
+    Proof. revert P t2; induction t1, t2; t_red; rewrite ?try_make_base_transport_cps_correct; t. Qed.
 
-    Lemma try_transport_cps_correct P t1 t2 v T k
-      : base.try_transport_cps P t1 t2 v T k
-        = k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with
-            | left pf => Some (rew [P] (base.type.internal_type_dec_bl _ _ pf) in v)
-            | right _ => None
-            end.
+    Lemma try_transport_cps_correct P t1 t2 v
+      : base.try_transport_cps P t1 t2 v
+        = fun T k
+          => k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with
+              | left pf => Some (rew [P] (base.type.internal_type_dec_bl _ _ pf) in v)
+              | right _ => None
+              end.
     Proof.
-      cbv [base.try_transport_cps cpscall cps_option_bind cpsreturn cpsbind Option.bind]; rewrite try_make_transport_cps_correct;
+      cbv [base.try_transport_cps]; rewrite try_make_transport_cps_correct;
         t.
     Qed.
 
@@ -189,7 +191,8 @@ Module Compilers.
           end.
     Ltac inversion_type_step :=
       cbv [defaults.type_base] in *;
-      first [ lazymatch goal with
+      first [ base.type.inversion_type_step
+            | lazymatch goal with
               | [ H : ?x = ?x :> type.type _ |- _ ] => clear H
               | [ H : ?x = ?y :> type.type _ |- _ ] => subst x || subst y
               end
@@ -233,12 +236,13 @@ Module Compilers.
               (base_type_lb : forall t1 t2, t1 = t2 -> base_type_beq t1 t2 = true)
               (try_make_transport_base_type_cps : forall (P : base_type -> Type) t1 t2, ~> option (P t1 -> P t2))
               (try_make_transport_base_type_cps_correct
-               : forall P t1 t2 T k,
-                  try_make_transport_base_type_cps P t1 t2 T k
-                  = k match Sumbool.sumbool_of_bool (base_type_beq t1 t2) with
-                      | left pf => Some (rew [fun t => P t1 -> P t] (base_type_bl _ _ pf) in id)
-                      | right _ => None
-                      end).
+               : forall P t1 t2,
+                  try_make_transport_base_type_cps P t1 t2
+                  = fun T k
+                    => k match Sumbool.sumbool_of_bool (base_type_beq t1 t2) with
+                        | left pf => Some (rew [fun t => P t1 -> P t] (base_type_bl _ _ pf) in id)
+                        | right _ => None
+                        end).
 
       Let base_type_eq_dec : DecidableRel (@eq base_type)
         := dec_rel_of_bool_dec_rel base_type_beq base_type_bl base_type_lb.
@@ -266,31 +270,34 @@ Module Compilers.
                        | [ H : _ |- _ ] => rewrite H
                        end ].
 
-      Lemma try_make_transport_cps_correct P t1 t2 T k
-        : type.try_make_transport_cps try_make_transport_base_type_cps P t1 t2 T k
-          = k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
-              | left pf => Some (rew [fun t => P t1 -> P t] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in id)
-              | right _ => None
-              end.
-      Proof. revert P t2 T k; induction t1, t2; t. Qed.
-
-      Lemma try_transport_cps_correct P t1 t2 v T k
-        : type.try_transport_cps try_make_transport_base_type_cps P t1 t2 v T k
-          = k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
-              | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v)
-              | right _ => None
-              end.
+      Lemma try_make_transport_cps_correct P t1 t2
+        : type.try_make_transport_cps try_make_transport_base_type_cps P t1 t2
+          = fun T k
+            => k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
+                | left pf => Some (rew [fun t => P t1 -> P t] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in id)
+                | right _ => None
+                end.
+      Proof. revert P t2; induction t1, t2; t. Qed.
+
+      Lemma try_transport_cps_correct P t1 t2
+        : type.try_transport_cps try_make_transport_base_type_cps P t1 t2
+          = fun v T k
+            => k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
+                | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v)
+                | right _ => None
+                end.
       Proof.
-        cbv [type.try_transport_cps cpscall cps_option_bind cpsreturn cpsbind Option.bind]; rewrite try_make_transport_cps_correct;
+        cbv [type.try_transport_cps]; rewrite try_make_transport_cps_correct;
           t.
       Qed.
 
-      Lemma try_transport_correct P t1 t2 v
-        : type.try_transport try_make_transport_base_type_cps P t1 t2 v
-          = match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
-            | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v)
-            | right _ => None
-            end.
+      Lemma try_transport_correct P t1 t2
+        : type.try_transport try_make_transport_base_type_cps P t1 t2
+          = fun v
+            => match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with
+              | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v)
+              | right _ => None
+              end.
       Proof. cbv [type.try_transport]; rewrite try_transport_cps_correct; reflexivity. Qed.
     End transport_cps.
   End type.
@@ -328,8 +335,7 @@ Module Compilers.
 
   Ltac rewrite_type_transport_correct :=
     cbv [type.try_transport_cps type.try_transport base.try_transport base.try_transport_cps] in *;
-    cbn [type.try_make_transport_cps] in *;
-    cbv [cpscall cpsbind cps_option_bind cpsreturn id] in *;
+    cbv [cpsbind cpscall cpsreturn id cps_option_bind] in *;
     repeat match goal with
            | [ |- context[type.try_make_transport_cps ?bmt ?P ?t1 ?t2] ]
              => erewrite type.try_make_transport_cps_correct
@@ -341,6 +347,10 @@ Module Compilers.
              => rewrite base.try_make_transport_cps_correct
            | [ H : context[base.try_make_transport_cps ?P ?t1 ?t2] |- _ ]
              => rewrite base.try_make_transport_cps_correct in H
+           | [ |- context[base.try_make_base_transport_cps ?P ?t1 ?t2] ]
+             => rewrite base.try_make_base_transport_cps_correct
+           | [ H : context[base.try_make_base_transport_cps ?P ?t1 ?t2] |- _ ]
+             => rewrite base.try_make_base_transport_cps_correct in H
            end.
 
   Module ident.
@@ -485,13 +495,11 @@ Module Compilers.
                      | discriminate
                      | reflexivity
                      | progress type.inversion_type
-                     | progress base.type.inversion_type
                      | progress invert_match
                      | progress ident.invert_match
                      | progress break_innermost_match_hyps
                      | exists eq_refl; cbn
-                     | progress cbv [type.try_transport type.try_transport_cps type.try_make_transport_cps cpsbind cpscall cps_option_bind cpsreturn id] in *
-                     | rewrite base.try_make_transport_cps_correct in *
+                     | progress rewrite_type_transport_correct
                      | progress type_beq_to_eq
                      | congruence ].
 
@@ -539,8 +547,7 @@ Module Compilers.
       Proof.
         intros T k; subst e; cbn [invert_expr.reflect_list_cps']; cbv [id type_base] in *.
         rewrite_type_transport_correct; break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect]; try reflexivity.
-        etransitivity; rewrite rec; clear rec; [ | reflexivity ]; cbv [id]; break_innermost_match; try reflexivity.
-        all: do 2 (rewrite_type_transport_correct; break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect]; try reflexivity).
+        all: etransitivity; rewrite rec; clear rec; [ | reflexivity ]; cbv [id]; break_innermost_match; try reflexivity.
       Qed.
 
 
@@ -571,7 +578,7 @@ Module Compilers.
             end.
       Proof.
         type.invert_one e; cbv [invert_expr.invert_nil invert_expr.invert_Ident type_base]; try reflexivity;
-          [ ident.invert_match; cbv [type_base] in *; base.type.inversion_type; reflexivity | ].
+          [ ident.invert_match; cbv [type_base] in *; type.inversion_type; reflexivity | ].
         do 2 (let f := match goal with f : expr (_ -> _) |- _ => f end in
               type.invert_one f; try reflexivity; []).
         cbv [type_base] in *; ident.invert; break_innermost_match_hyps; subst; destruct_head' False; try reflexivity; [].
@@ -579,9 +586,13 @@ Module Compilers.
         cbv [invert_expr.reflect_list invert_expr.invert_cons invert_expr.invert_AppIdent2 invert_expr.invert_App2 invert_expr.invert_App Option.bind invert_expr.invert_Ident].
         cbv [invert_expr.reflect_list_cps].
         cbn [invert_expr.reflect_list_cps'].
-        rewrite_type_transport_correct; break_innermost_match_step; type_beq_to_eq; try discriminate; base.type.inversion_type; [].
-        rewrite reflect_list_cps'_id; cbv [id]; break_innermost_match; try reflexivity; [].
-        rewrite_type_transport_correct; break_innermost_match_step; type_beq_to_eq; base.type.inversion_type; try discriminate; reflexivity.
+        repeat first [ reflexivity
+                     | discriminate
+                     | progress rewrite_type_transport_correct
+                     | progress type_beq_to_eq
+                     | progress break_innermost_match
+                     | progress type.inversion_type
+                     | rewrite reflect_list_cps'_id; reflexivity ].
       Qed.
 
       Lemma reify_list_nil {t} : reify_list nil = ([])%expr :> expr (base.type.list t).