Add support for custom intro tactic in ring pkg, for speed

2 files changed, 21 insertions, 12 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 9f8eb61de..840d3a592 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -5,15 +5,17 @@ Require Import Crypto.Util.SideConditions.ModInvPackage.
 Require Import Crypto.Util.SideConditions.ReductionPackages.
 Require Import Crypto.Util.SideConditions.RingPackage.
 
-Ltac autosolve_gen autosolve_tac else_tac :=
+Ltac autosolve_gen autosolve_tac ring_intros_tac else_tac :=
   CorePackages.preautosolve ();
   CorePackages.Internal.autosolve ltac:(fun _ =>
   AdmitPackage.autosolve ltac:(fun _ =>
   ModInvPackage.autosolve ltac:(fun _ =>
   ReductionPackages.autosolve autosolve_tac ltac:(fun _ =>
-  RingPackage.autosolve ltac:(fun _ =>
+  RingPackage.autosolve_gen_intros ring_intros_tac ltac:(fun _ =>
   CorePackages.autosolve else_tac
                                        ))))).
 
-Ltac autosolve else_tac :=
-  autosolve_gen autosolve else_tac.
+Ltac autosolve_gen_intros ring_intros_tac else_tac :=
+  autosolve_gen ltac:(autosolve_gen_intros ring_intros_tac) ring_intros_tac else_tac.
+
+Ltac autosolve else_tac := autosolve_gen_intros default_ring_intros_tac else_tac.
diff --git a/src/Util/SideConditions/RingPackage.v b/src/Util/SideConditions/RingPackage.v
index 3cb7b64da..8541c00fc 100644
--- a/src/Util/SideConditions/RingPackage.v
+++ b/src/Util/SideConditions/RingPackage.v
@@ -6,31 +6,38 @@ Require Export Crypto.Util.FixCoqMistakes.
 
 Definition eq_by_Zring_prod_package (P : Prop) := P.
 
-Ltac auto_split_prod_step_early _ :=
+Ltac auto_split_prod_step_early special_ring_intros_tac :=
   match goal with
   | _ => progress hnf
+  | _ => progress special_ring_intros_tac ()
   | [ H : prod _ _ |- _ ] => destruct H
   | [ |- forall a, _ ] => let a := fresh in intro a; compute in a
   end.
 
-Ltac auto_split_prod_step _ :=
+Ltac auto_split_prod_step special_ring_intros_tac :=
   match goal with
-  | _ => auto_split_prod_step_early ()
+  | _ => auto_split_prod_step_early special_ring_intros_tac
   | [ |- pair _ _ = pair _ _ ] => apply f_equal2
   | [ |- @eq (prod _ _) _ _ ] => apply path_prod
   end.
 
-Ltac Zring_prod_eq_tac _ :=
-  repeat auto_split_prod_step_early ();
+Ltac Zring_prod_eq_tac_gen special_ring_intros_tac :=
+  repeat auto_split_prod_step_early special_ring_intros_tac;
   cbv -[Z.add Z.sub Z.mul Z.div Z.pow Z.opp Z.log2 Z.land Z.lor Z.log2_up Z.abs];
   repeat match goal with
-         | _ => auto_split_prod_step ()
+         | _ => auto_split_prod_step special_ring_intros_tac
          | [ |- @eq Z _ _ ] => ring
          end.
 
-Ltac autosolve else_tac :=
+Ltac default_ring_intros_tac _ := fail.
+
+Ltac Zring_prod_eq_tac _ := Zring_prod_eq_tac_gen default_ring_intros_tac.
+
+Ltac autosolve_gen_intros special_ring_intros_tac else_tac :=
   lazymatch goal with
   | [ |- eq_by_Zring_prod_package _ ]
-    => abstract Zring_prod_eq_tac ()
+    => abstract Zring_prod_eq_tac_gen special_ring_intros_tac
   | _ => else_tac ()
   end.
+
+Ltac autosolve else_tac := autosolve_gen_intros default_ring_intros_tac else_tac.