From 980c92a3b46897b4e1b1d72bc552d3a48e27c673 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 20 Jul 2016 18:53:24 -0400 Subject: automate a proof --- src/ModularArithmetic/Pre.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 47a38b867..5e61278f6 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -4,6 +4,7 @@ Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Tactics.VerdiTactics. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. @@ -106,7 +107,7 @@ Program Definition mod_inv_sig {m} (a:{z : Z | z = z mod m}) : {z : Z | z = z mo | _ => powmod m a (Z.to_N (m-2)) end. Next Obligation. - abstract (destruct a; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity). + intros; break_match; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity. Qed. Program Definition inv_impl {m : BinNums.Z} : -- cgit v1.2.3