1 files changed, 10 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.