More modularity in autosolve

4 files changed, 160 insertions, 110 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 3428a77e9..51c13647c 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -1,115 +1,15 @@
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.SideConditions.CorePackages.
-Require Import Crypto.Util.Tactics.HeadUnderBinders.
+Require Import Crypto.Util.SideConditions.ReductionPackages.
+Require Import Crypto.Util.SideConditions.RingPackage.
 
-Definition vm_decide_package (P : Prop) := P.
-Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P.
-Definition vm_compute_reflexivity_package (P : Prop) := P.
-Inductive cast_bias := LHS | RHS.
-Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
-  @evar_package T v.
-Notation vm_compute_evar_package_vm_small := (@vm_compute_evar_package_gen LHS).
-Notation vm_compute_evar_package_vm_large := (@vm_compute_evar_package_gen RHS).
-Notation vm_compute_evar_package := vm_compute_evar_package_vm_small.
-Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v.
-Definition cast_evar_package {s} (v : s) d := @evard_package s d v.
-Definition vm_compute_cast_evar_package {s} (v : s) d := @evard_package s d v.
-
-Definition optional_evar_Prop_package {T} (P : T -> Prop) (alt_pkg : Type)
-  := @evar_Prop_package
-       (option T)
-       (fun v => match v with
-                 | Some v => P v
-                 | None => True
-                 end).
-
-Definition None_evar_Prop_package' {alt_pkg T P} : @optional_evar_Prop_package T P alt_pkg
-  := {| val := None ; evar_package_pf := I |}.
-Notation None_evar_Prop_package := (@None_evar_Prop_package' unit).
-
-Notation optional_evar_package pkg_type
-  := (optional_evar_Prop_package
-        (ltac:(lazymatch eval hnf in pkg_type with evar_Prop_package ?P => exact P end))
-        pkg_type)
-       (only parsing).
-
-Definition option_evar_rel_package {A} (v : option A) B (R : B -> A -> Prop) (alt_pkg : A -> Type)
-  := @evar_Prop_package
-       (option B)
-       (fun v' => match v', v with
-                  | Some v', Some v => R v' v
-                  | None, None => True
-                  | Some _, None | None, Some _ => False
-                  end).
-
-Notation optional_evar_rel_package pkg_type x
-  := (option_evar_rel_package
-        x
-        _
-        (fun a b
-         => ltac:(lazymatch eval hnf in (pkg_type b) with
-                  | evar_Prop_package ?P
-                    => let P := (eval cbv beta in (P a)) in
-                       exact P
-                  end))
-        pkg_type)
-       (only parsing).
-
-Definition unoption_evar_rel_package {A v B R alt_pkg}
-           (f : forall v, alt_pkg v -> @evar_rel_package A v B R)
-  : forall (pkg : match v with
-                  | Some v => alt_pkg v
-                  | None => True
-                  end),
-    @option_evar_rel_package A v B R alt_pkg
-  := match v
-           return match v with
-                  | Some v => alt_pkg v
-                  | None => True
-                  end -> @option_evar_rel_package A v B R alt_pkg
-     with
-     | Some v => fun pkg => {| val := Some (val (f _ pkg));
-                               evar_package_pf := evar_package_pf (f _ pkg) |}
-     | None => fun _ => None_evar_Prop_package
-     end.
+Ltac autosolve_gen autosolve_tac else_tac :=
+  CorePackages.preautosolve ();
+  CorePackages.Internal.autosolve ltac:(fun _ =>
+  ReductionPackages.autosolve autosolve_tac ltac:(fun _ =>
+  RingPackage.autosolve ltac:(fun _ =>
+  CorePackages.autosolve else_tac
+                                       ))).
 
 Ltac autosolve else_tac :=
-  CorePackages.preautosolve ();
-  lazymatch goal with
-  | [ |- True ] => exact I
-  | [ |- unit ] => exact tt
-  | [ |- IDProp ] => exact idProp
-  | [ |- match ?x with Some _ => _ | None => _ end ]
-    => let x' := (eval hnf in x) in
-       progress change x with x';
-       cbv beta iota;
-       autosolve else_tac
-  | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
-  | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
-  | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
-  | [ |- vm_compute_evar_package_vm_small ?v ]
-    => let v' := (eval vm_compute in v) in
-       (exists v'); abstract vm_cast_no_check (eq_refl v')
-  | [ |- vm_compute_evar_package_vm_large ?v ]
-    => let v' := (eval vm_compute in v) in
-       (exists v'); abstract vm_cast_no_check (eq_refl v)
-  | [ |- vm_cast_evar_package ?v ?d ]
-    => unshelve eexists (v <: d);
-       [ vm_compute; reflexivity
-       | cbv beta;
-         let lhs := lazymatch goal with |- ?lhs = _ => lhs end in
-         abstract exact_no_check (eq_refl lhs) ]
-  | [ |- cast_evar_package (s:=?s) ?v ?d ]
-    => exact (@Build_evard_package
-                s d v
-                v eq_refl eq_refl)
-  | [ |- vm_compute_cast_evar_package (s:=?s) ?v ?d ]
-    => let v' := (eval vm_compute in v) in
-       exact (@Build_evard_package
-                s d v
-                v' eq_refl eq_refl)
-  | [ |- @option_evar_rel_package ?A ?v ?B ?R ?alt_pkg ]
-    => refine (@unoption_evar_rel_package A v B R alt_pkg (fun _ x => x) _);
-       autosolve else_tac
-  | _ => CorePackages.autosolve else_tac
-  end.
+  autosolve_gen autosolve else_tac.
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v
index 7af4cc133..c4511c93e 100644
--- a/src/Util/SideConditions/CorePackages.v
+++ b/src/Util/SideConditions/CorePackages.v
@@ -46,4 +46,14 @@ Definition evard_package_pf {s d v} (pkg : @evard_package s d v)
 Ltac preautosolve _ :=
   repeat autounfold with autosolve in *.
 
+Module Internal.
+  Ltac autosolve else_tac :=
+    lazymatch goal with
+    | [ |- True ] => exact I
+    | [ |- unit ] => exact tt
+    | [ |- IDProp ] => exact idProp
+    | _ => else_tac ()
+    end.
+End Internal.
+
 Ltac autosolve else_tac := else_tac ().
diff --git a/src/Util/SideConditions/ReductionPackages.v b/src/Util/SideConditions/ReductionPackages.v
new file mode 100644
index 000000000..3266540ac
--- /dev/null
+++ b/src/Util/SideConditions/ReductionPackages.v
@@ -0,0 +1,111 @@
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.SideConditions.CorePackages.
+Require Import Crypto.Util.Tactics.HeadUnderBinders.
+
+Definition vm_decide_package (P : Prop) := P.
+Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P.
+Definition vm_compute_reflexivity_package (P : Prop) := P.
+Inductive cast_bias := LHS | RHS.
+Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
+  @evar_package T v.
+Notation vm_compute_evar_package_vm_small := (@vm_compute_evar_package_gen LHS).
+Notation vm_compute_evar_package_vm_large := (@vm_compute_evar_package_gen RHS).
+Notation vm_compute_evar_package := vm_compute_evar_package_vm_small.
+Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v.
+Definition cast_evar_package {s} (v : s) d := @evard_package s d v.
+Definition vm_compute_cast_evar_package {s} (v : s) d := @evard_package s d v.
+
+Definition optional_evar_Prop_package {T} (P : T -> Prop) (alt_pkg : Type)
+  := @evar_Prop_package
+       (option T)
+       (fun v => match v with
+                 | Some v => P v
+                 | None => True
+                 end).
+
+Definition None_evar_Prop_package' {alt_pkg T P} : @optional_evar_Prop_package T P alt_pkg
+  := {| val := None ; evar_package_pf := I |}.
+Notation None_evar_Prop_package := (@None_evar_Prop_package' unit).
+
+Notation optional_evar_package pkg_type
+  := (optional_evar_Prop_package
+        (ltac:(lazymatch eval hnf in pkg_type with evar_Prop_package ?P => exact P end))
+        pkg_type)
+       (only parsing).
+
+Definition option_evar_rel_package {A} (v : option A) B (R : B -> A -> Prop) (alt_pkg : A -> Type)
+  := @evar_Prop_package
+       (option B)
+       (fun v' => match v', v with
+                  | Some v', Some v => R v' v
+                  | None, None => True
+                  | Some _, None | None, Some _ => False
+                  end).
+
+Notation optional_evar_rel_package pkg_type x
+  := (option_evar_rel_package
+        x
+        _
+        (fun a b
+         => ltac:(lazymatch eval hnf in (pkg_type b) with
+                  | evar_Prop_package ?P
+                    => let P := (eval cbv beta in (P a)) in
+                       exact P
+                  end))
+        pkg_type)
+       (only parsing).
+
+Definition unoption_evar_rel_package {A v B R alt_pkg}
+           (f : forall v, alt_pkg v -> @evar_rel_package A v B R)
+  : forall (pkg : match v with
+                  | Some v => alt_pkg v
+                  | None => True
+                  end),
+    @option_evar_rel_package A v B R alt_pkg
+  := match v
+           return match v with
+                  | Some v => alt_pkg v
+                  | None => True
+                  end -> @option_evar_rel_package A v B R alt_pkg
+     with
+     | Some v => fun pkg => {| val := Some (val (f _ pkg));
+                               evar_package_pf := evar_package_pf (f _ pkg) |}
+     | None => fun _ => None_evar_Prop_package
+     end.
+
+Ltac autosolve autosolve_tac else_tac :=
+  lazymatch goal with
+  | [ |- match ?x with Some _ => _ | None => _ end ]
+    => let x' := (eval hnf in x) in
+       progress change x with x';
+       cbv beta iota;
+       autosolve_tac else_tac
+  | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
+  | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
+  | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
+  | [ |- vm_compute_evar_package_vm_small ?v ]
+    => let v' := (eval vm_compute in v) in
+       (exists v'); abstract vm_cast_no_check (eq_refl v')
+  | [ |- vm_compute_evar_package_vm_large ?v ]
+    => let v' := (eval vm_compute in v) in
+       (exists v'); abstract vm_cast_no_check (eq_refl v)
+  | [ |- vm_cast_evar_package ?v ?d ]
+    => unshelve eexists (v <: d);
+       [ vm_compute; reflexivity
+       | cbv beta;
+         let lhs := lazymatch goal with |- ?lhs = _ => lhs end in
+         abstract exact_no_check (eq_refl lhs) ]
+  | [ |- cast_evar_package (s:=?s) ?v ?d ]
+    => exact (@Build_evard_package
+                s d v
+                v eq_refl eq_refl)
+  | [ |- vm_compute_cast_evar_package (s:=?s) ?v ?d ]
+    => let v' := (eval vm_compute in v) in
+       exact (@Build_evard_package
+                s d v
+                v' eq_refl eq_refl)
+  | [ |- @option_evar_rel_package ?A ?v ?B ?R ?alt_pkg ]
+    => refine (@unoption_evar_rel_package A v B R alt_pkg (fun _ x => x) _);
+       autosolve_tac else_tac
+  | _ => else_tac ()
+  end.
diff --git a/src/Util/SideConditions/RingPackage.v b/src/Util/SideConditions/RingPackage.v
new file mode 100644
index 000000000..f979b77ba
--- /dev/null
+++ b/src/Util/SideConditions/RingPackage.v
@@ -0,0 +1,29 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.setoid_ring.Ring_tac.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.SideConditions.CorePackages.
+Require Export Crypto.Util.FixCoqMistakes.
+
+Definition eq_by_Zring_prod_package (P : Prop) := P.
+
+Ltac auto_split_prod_step _ :=
+  match goal with
+  | [ H : prod _ _ |- _ ] => destruct H
+  | [ |- forall a, _ ] => let a := fresh in intro a; compute in a
+  | [ |- pair _ _ = pair _ _ ] => apply f_equal2
+  | [ |- @eq (prod _ _) _ _ ] => apply path_prod
+  end.
+
+Ltac Zring_prod_eq_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 ()
+         | [ |- @eq Z _ _ ] => ring
+         end.
+
+Ltac autosolve else_tac :=
+  lazymatch goal with
+  | [ |- eq_by_Zring_prod_package _ ]
+    => solve [ Zring_prod_eq_tac () ]
+  | _ => else_tac ()
+  end.