Add ModInv autosolver

1 files changed, 24 insertions, 0 deletions

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.