From 6ebe0ff5b046658b198c645e72b6484d2342c4cf Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 30 Oct 2016 13:27:24 -0400
Subject: Premature optimization of [Reify_rhs]

This might or might not actually speed up proving things.
---
 src/Reflection/Reify.v   | 36 ++++++++++++++++++++++--------------
 src/Reflection/Z/Reify.v |  8 +++++---
 2 files changed, 27 insertions(+), 17 deletions(-)

(limited to 'src/Reflection')

diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
index c83d15fe8..3a47bcbcc 100644
--- a/src/Reflection/Reify.v
+++ b/src/Reflection/Reify.v
@@ -244,21 +244,29 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac :=
   let rhs := rhs_of_goal in
   let RHS := Reify rhs in
   let RHS' := (eval vm_compute in RHS) in
-  transitivity (Syntax.Interp interp_op RHS');
-  [
-  | transitivity (Syntax.Interp interp_op RHS);
-    [ lazymatch goal with
-      | [ |- ?R ?x ?y ]
-        => cut (x = y)
-      end;
-      [ let H := fresh in
-        intro H; rewrite H; reflexivity
-      | apply f_equal; vm_compute; reflexivity ]
-    | etransitivity; (* first we strip off the [InputSyntax.Compile]
+  let RHSH := fresh in
+  let RHSH' := fresh in
+  pose RHS as RHSH;
+  pose RHS' as RHSH';
+  transitivity (Syntax.Interp interp_op RHSH');
+  [ subst RHSH RHSH'
+  | transitivity (Syntax.Interp interp_op RHSH);
+    [ abstract (
+          lazymatch goal with
+          | [ |- ?R ?x ?y ]
+            => cut (x = y)
+          end;
+          [ let H := fresh in
+            intro H; rewrite H; reflexivity
+          | apply f_equal; vm_compute; reflexivity ]
+        )
+    | clear RHSH';
+      etransitivity; (* first we strip off the [InputSyntax.Compile]
                         bit; Coq is bad at inferring the type, so we
                         help it out by providing it *)
-      [ prove_interp_compile_correct ()
-      | try_tac
+      [ subst RHSH; prove_interp_compile_correct ()
+      | subst RHSH;
+        try_tac
           ltac:(fun _
                 => (* now we unfold the interpretation function,
                       including the parameterized bits; we assume that
@@ -272,7 +280,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac :=
                            change interp_base_type with interp_base_type';
                            change interp_op with interp_op'
                       end;
-                      cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; reflexivity)) ] ] ].
+                      cbv iota beta delta [Let_In InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; reflexivity)) ] ] ].
 
 Ltac prove_compile_correct :=
   fun _ => lazymatch goal with
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 3c42c162c..a67fe12fb 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -33,10 +33,12 @@ Ltac Reify e :=
 Ltac prove_InlineConst_Linearize_Compile_correct :=
   fun _
   => lazymatch goal with
-     | [ |- Syntax.interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst (Linearize _))) _ ]
-       => etransitivity;
+     | [ |- Syntax.interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst (Linearize (InputSyntax.Compile ?e)))) _ ]
+       => let eH := fresh in
+          set (eH := e);
+          etransitivity;
           [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op t);
-            reflect_Wf base_type_eq_semidec_is_dec op_beq_bl
+            abstract reflect_Wf base_type_eq_semidec_is_dec op_beq_bl
           | etransitivity;
             [ apply (@Interp_Linearize base_type_code interp_base_type op interp_op t)
             | prove_compile_correct () ] ]
-- 
cgit v1.2.3