diff options
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Algebra.v | 12 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 | ||||
| -rw-r--r-- | src/Tactics/Algebra_syntax/Nsatz.v (renamed from src/Tactics/Nsatz.v) | 11 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 3 |
7 files changed, 24 insertions, 11 deletions
diff --git a/_CoqProject b/_CoqProject index f3f07e840..f8aa1e966 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v +src/Encoding/PointEncodingPre.v src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v @@ -54,8 +55,8 @@ src/Spec/ModularWordEncoding.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v -src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v +src/Tactics/Algebra_syntax/Nsatz.v src/Util/CaseUtil.v src/Util/Decidable.v src/Util/IterAssocOp.v diff --git a/src/Algebra.v b/src/Algebra.v index f9dfbd519..9f53c0613 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1,9 +1,10 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Notations. Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. +Require Crypto.Tactics.Algebra_syntax.Nsatz. Module Import ModuloCoq8485. Import NPeano Nat. @@ -637,6 +638,11 @@ Module Field. End Homomorphism. End Field. +(** Tactics *) + +Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax. +Ltac nsatz_contradict := Algebra_syntax.Nsatz.nsatz_contradict; dropRingSyntax. + (*** Tactics for manipulating field equations *) Require Import Coq.setoid_ring.Field_tac. @@ -981,7 +987,7 @@ Ltac neq01 := Ltac conservative_field_algebra := intros; conservative_common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 @@ -991,7 +997,7 @@ Ltac conservative_field_algebra := Ltac field_algebra := intros; common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 65d899463..44bb80157 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 364d7f9ec..263582508 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index ed4511fc9..432e834aa 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.Util.Notations. Generalizable All Variables. diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v index 04f35c200..a5b04cfa2 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Algebra_syntax/Nsatz.v @@ -121,11 +121,14 @@ Ltac nsatz_sugar_power sugar power := let domain := nsatz_guess_domain in nsatz_domain_sugar_power domain sugar power. -Tactic Notation "nsatz" constr(n) := - let nn := (eval compute in (BinNat.N.of_nat n)) in - nsatz_sugar_power BinInt.Z0 nn. +Ltac nsatz_power power := + let power_N := (eval compute in (BinNat.N.of_nat power)) in + nsatz_sugar_power BinInt.Z0 power_N. -Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat. +Ltac nsatz := nsatz_power 1%nat || nsatz_power 2%nat || nsatz_power 3%nat || nsatz_power 4%nat || nsatz_power 5%nat. + +Tactic Notation "nsatz" := nsatz. +Tactic Notation "nsatz" constr(n) := nsatz_power n. (** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] contradicts any hypothesis of the form [?x' <> ?y'], we turn this diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 4630e4ab7..01d72def9 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -7,6 +7,9 @@ Tactic Notation "test" tactic3(tac) := (** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *) Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds"). +Ltac get_goal := + match goal with |- ?G => G end. + (** find the head of the given expression *) Ltac head expr := match expr with |