Add ModInv autosolver

2 files changed, 27 insertions, 1 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 7d2f1a9c7..9f8eb61de 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.SideConditions.CorePackages.
 Require Import Crypto.Util.SideConditions.AdmitPackage.
+Require Import Crypto.Util.SideConditions.ModInvPackage.
 Require Import Crypto.Util.SideConditions.ReductionPackages.
 Require Import Crypto.Util.SideConditions.RingPackage.
 
@@ -8,10 +9,11 @@ Ltac autosolve_gen autosolve_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 _ =>
   CorePackages.autosolve else_tac
-                                       )))).
+                                       ))))).
 
 Ltac autosolve else_tac :=
   autosolve_gen autosolve else_tac.
diff --git a/src/Util/SideConditions/ModInvPackage.v b/src/Util/SideConditions/ModInvPackage.v
new file mode 100644
index 000000000..8aef3cb75
--- /dev/null
+++ b/src/Util/SideConditions/ModInvPackage.v
@@ -0,0 +1,24 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ZUtil.ModInv.
+Require Import Crypto.Util.SideConditions.CorePackages.
+
+Local Open Scope Z_scope.
+
+Definition modinv_evar_package (modinv_fuel : nat) (a modulus : Z)
+  := evar_Prop_package
+       (fun a' => (a * a') mod modulus = 1).
+
+Ltac autosolve else_tac :=
+  lazymatch goal with
+  | [ |- modinv_evar_package ?modinv_fuel ?a ?modulus ]
+    => let v0 := constr:(Option.invert_Some (Z.modinv_fueled modinv_fuel a modulus)) in
+       let v := (eval vm_compute in v0) in
+       let v := lazymatch type of v with (* if the computation failed, display a reasonable error message about the attempted computation *)
+                | Z => v
+                | _ => (eval cbv -[Option.invert_Some Z.modinv_fueled] in v0)
+                end in
+       let v := (eval vm_compute in (v <: Z)) in
+       (exists v); vm_compute; reflexivity
+  | _ => else_tac ()
+  end.