From 29a82aac609e7ae9358ce2bdd98b51f25fcd2b8e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 13:17:38 -0700 Subject: Update _CoqProject --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 9c4cdd3cf..3b2350b77 100644 --- a/_CoqProject +++ b/_CoqProject @@ -36,6 +36,7 @@ src/Specific/GF25519.v src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v +src/Util/Decidable.v src/Util/IterAssocOp.v src/Util/ListUtil.v src/Util/NatUtil.v -- cgit v1.2.3 From 18b79f83ce6c947eaa49baf586cc475d50e3d9ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 13:34:00 -0700 Subject: Aggregate all level specifications not in Spec/* This prevents notation conflicts (see comment in Notations.v for more explanation). --- _CoqProject | 1 + src/BaseSystem.v | 3 ++- src/BaseSystemProofs.v | 3 ++- .../CompleteEdwardsCurveTheorems.v | 3 ++- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 3 ++- src/CompleteEdwardsCurve/Pre.v | 5 +++-- src/ModularArithmetic/ModularBaseSystem.v | 3 ++- src/ModularArithmetic/ModularBaseSystemProofs.v | 11 ++++++----- src/Specific/GF25519.v | 11 ++++++----- src/Util/Notations.v | 20 ++++++++++++++++++++ 10 files changed, 46 insertions(+), 17 deletions(-) create mode 100644 src/Util/Notations.v (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 3b2350b77..85aa5a0df 100644 --- a/_CoqProject +++ b/_CoqProject @@ -40,6 +40,7 @@ src/Util/Decidable.v src/Util/IterAssocOp.v src/Util/ListUtil.v src/Util/NatUtil.v +src/Util/Notations.v src/Util/NumTheoryUtil.v src/Util/Tactics.v src/Util/Tuple.v diff --git a/src/BaseSystem.v b/src/BaseSystem.v index c07aad759..1985520f0 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -2,6 +2,7 @@ Require Import Coq.Lists.List. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.Notations. Import Nat. Local Open Scope Z. @@ -47,7 +48,7 @@ Section BaseSystem. | _, nil => us | _, _ => vs end. - Infix ".+" := add (at level 50). + Infix ".+" := add. Hint Extern 1 (@eq Z _ _) => ring. diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 4414877b4..85835aabe 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -3,9 +3,10 @@ Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import ZArith.ZArith ZArith.Zdiv. Require Import Omega NPeano Arith. Require Import Crypto.BaseSystem. +Require Import Crypto.Util.Notations. Local Open Scope Z. -Local Infix ".+" := add (at level 50). +Local Infix ".+" := add. Local Hint Extern 1 (@eq Z _ _) => ring. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 683addd5d..c217303aa 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. Module E. Import Group Ring Field CompleteEdwardsCurve.E. @@ -18,7 +19,7 @@ Module E. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. - Local Notation "x ^2" := (x*x) (at level 30). + Local Notation "x ^2" := (x*x). Local Notation point := (@point F Feq Fone Fadd Fmul a d). Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 25af83a0a..e2ffa0313 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. Module Extended. Section ExtendedCoordinates. @@ -18,7 +19,7 @@ Module Extended. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. - Local Notation "x ^2" := (x*x) (at level 30). + Local Notation "x ^2" := (x*x). Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d). diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 5314ee37c..7e9f14321 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Notations. Generalizable All Variables. Section Pre. @@ -9,7 +10,7 @@ Section Pre. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. - Local Notation "x '^' 2" := (x*x) (at level 30). + Local Notation "x ^2" := (x*x). Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). @@ -97,4 +98,4 @@ Section RespectsFieldHomomorphism. apply conj; (rewrite_strat topdown hints field_homomorphism); reflexivity. Qed. -End RespectsFieldHomomorphism. \ No newline at end of file +End RespectsFieldHomomorphism. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index ca8c19d18..08545bdb4 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -7,6 +7,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.Notations. Local Open Scope Z_scope. Section PseudoMersenneBase. @@ -15,7 +16,7 @@ Section PseudoMersenneBase. Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x. - Local Notation "u '~=' x" := (rep u x) (at level 70). + Local Notation "u ~= x" := (rep u x). Local Hint Unfold rep. Definition encode (x : F modulus) := encode x ++ BaseSystem.zeros (length base - 1)%nat. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 0462b0f37..6f82a8950 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -6,15 +6,16 @@ Require Import VerdiTactics. Require Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Util.Notations. Local Open Scope Z_scope. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. Local Hint Unfold decode. - Local Notation "u '~=' x" := (rep u x) (at level 70). - Local Notation "u '.+' x" := (add u x) (at level 70). - Local Notation "u '.*' x" := (ModularBaseSystem.mul u x) (at level 70). + Local Notation "u ~= x" := (rep u x). + Local Notation "u .+ x" := (add u x). + Local Notation "u .* x" := (ModularBaseSystem.mul u x). Local Hint Unfold rep. Lemma rep_decode : forall us x, us ~= x -> decode us = x. @@ -256,7 +257,7 @@ End PseudoMersenneProofs. Section CarryProofs. Context `{prm : PseudoMersenneBaseParams}. - Local Notation "u '~=' x" := (rep u x) (at level 70). + Local Notation "u ~= x" := (rep u x). Hint Unfold log_cap. Lemma base_length_lt_pred : (pred (length base) < length base)%nat. @@ -2086,4 +2087,4 @@ Section CanonicalizationProofs. eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs. \ No newline at end of file +End CanonicalizationProofs. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 471c1d548..6d7e2c38c 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -9,6 +9,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Crypto.Util.Notations. Local Open Scope Z. (* BEGIN PseudoMersenneBaseParams instance construction. *) @@ -60,8 +61,8 @@ Proof. (* Uncomment this to see a pretty-printed mulmod Local Transparent Let_In. -Infix "<<" := Z.shiftr (at level 50). -Infix "&" := Z.land (at level 50). +Infix "<<" := Z.shiftr. +Infix "&" := Z.land. Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => proj1_sig ( @@ -122,9 +123,9 @@ Defined. (* Set Printing Depth 1000. Local Transparent Let_In. -Infix "<<" := Z.shiftr (at level 50). -Infix "&" := Z.land (at level 50). +Infix "<<" := Z.shiftr. +Infix "&" := Z.land. Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig ( GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9). -*) \ No newline at end of file +*) diff --git a/src/Util/Notations.v b/src/Util/Notations.v new file mode 100644 index 000000000..6cc80944b --- /dev/null +++ b/src/Util/Notations.v @@ -0,0 +1,20 @@ +(** * Reserved Notations *) + +(** Putting them all together in one file prevents conflicts. Coq's + parser (camlpX) is really bad at conflicting notation levels and + is sometimes really bad at backtracking, too. Not having level + declarations in other files makes it harder for us to confuse + Coq's parser. *) + +Reserved Infix "=?" (at level 70, no associativity). +Reserved Infix "?=" (at level 70, no associativity). +Reserved Infix "?<" (at level 70, no associativity). +Reserved Infix ".+" (at level 50). +Reserved Notation "x ^2" (at level 30, format "x ^2"). +Reserved Infix "mod" (at level 40, no associativity). +Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50). +Reserved Infix "<<" (at level 50). +Reserved Infix "&" (at level 50). +Reserved Infix "<<" (at level 50). +Reserved Infix "&" (at level 50). +Reserved Infix "~=" (at level 70). -- cgit v1.2.3