blob: 8aef3cb75e007ffbe563863ad306ecc7a28d720f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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.
|
