diff options
author | Jason Gross <jagro@google.com> | 2016-07-27 17:18:30 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-27 17:25:08 -0700 |
commit | 6dc1781b13e14c64a6e209a0981c03203fdd9e70 (patch) | |
tree | 1f8d21aae565caa22251d185ecf47ed7366cae3b /src/Algebra.v | |
parent | d763f699ae49e60cfadd0e334f4f20e65aa494b4 (diff) |
Move most notation level declarations into Util
This reveals and prevents notation clashes.
Notable breakage:
- `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.`
(@jadephilipoom)
- `x [[ y ]]` breaks `destruct x as [[a]|[b]].` (@jadephilipoom)
- `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)`
(@varomodt)
After | File Name | Before || Change
------------------------------------------------------------------------------------
3m16.07s | Total | 3m23.63s || -0m07.55s
------------------------------------------------------------------------------------
0m16.90s | ModularArithmetic/ModularBaseSystemProofs | 0m19.02s || -0m02.12s
0m03.29s | ModularArithmetic/ModularBaseSystemOpt | 0m05.30s || -0m02.00s
0m12.04s | Experiments/SpecEd25519 | 0m13.89s || -0m01.85s
0m36.02s | CompleteEdwardsCurve/ExtendedCoordinates | 0m36.12s || -0m00.09s
0m34.48s | Specific/GF25519 | 0m34.27s || +0m00.20s
0m15.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.76s || -0m00.14s
0m07.36s | Specific/GF1305 | 0m07.34s || +0m00.02s
0m06.64s | Algebra | 0m06.14s || +0m00.50s
0m05.12s | WeierstrassCurve/Pre | 0m05.09s || +0m00.03s
0m04.58s | ModularArithmetic/Tutorial | 0m03.83s || +0m00.75s
0m04.46s | BaseSystemProofs | 0m04.33s || +0m00.12s
0m04.26s | ModularArithmetic/Pow2BaseProofs | 0m05.16s || -0m00.90s
0m03.91s | CompleteEdwardsCurve/Pre | 0m04.62s || -0m00.71s
0m02.75s | Assembly/State | 0m03.12s || -0m00.37s
0m02.55s | Experiments/EdDSARefinement | 0m01.85s || +0m00.69s
0m02.46s | Util/ZUtil | 0m02.45s || +0m00.00s
0m01.86s | Assembly/Wordize | 0m02.02s || -0m00.15s
0m01.68s | ModularArithmetic/ModularArithmeticTheorems | 0m01.68s || +0m00.00s
0m01.67s | ModularArithmetic/PrimeFieldTheorems | 0m01.96s || -0m00.29s
0m01.50s | Encoding/PointEncodingPre | 0m02.20s || -0m00.70s
0m01.46s | ModularArithmetic/BarrettReduction/Z | 0m01.02s || +0m00.43s
0m01.26s | BaseSystem | 0m01.21s || +0m00.05s
0m01.24s | Assembly/Pseudize | 0m01.22s || +0m00.02s
0m01.20s | ModularArithmetic/ExtendedBaseVector | 0m01.86s || -0m00.66s
0m01.04s | Util/IterAssocOp | 0m00.74s || +0m00.30s
0m00.96s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.67s || +0m00.28s
0m00.96s | Assembly/Pipeline | 0m00.65s || +0m00.30s
0m00.93s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.98s || -0m00.04s
0m00.93s | ModularArithmetic/ModularBaseSystemField | 0m00.95s || -0m00.01s
0m00.92s | Util/NumTheoryUtil | 0m01.19s || -0m00.26s
0m00.90s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.89s || +0m00.01s
0m00.82s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.95s || -0m00.13s
0m00.81s | Assembly/QhasmEvalCommon | 0m00.86s || -0m00.04s
0m00.80s | Assembly/StringConversion | 0m00.60s || +0m00.20s
0m00.79s | Assembly/Qhasm | 0m00.54s || +0m00.25s
0m00.73s | Assembly/Pseudo | 0m00.98s || -0m00.25s
0m00.72s | Util/AdditionChainExponentiation | 0m00.92s || -0m00.20s
0m00.69s | Experiments/SpecificCurve25519 | 0m00.72s || -0m00.03s
0m00.65s | Spec/ModularWordEncoding | 0m00.85s || -0m00.19s
0m00.65s | ModularArithmetic/ModularBaseSystemList | 0m00.68s || -0m00.03s
0m00.65s | Assembly/PseudoConversion | 0m00.67s || -0m00.02s
0m00.64s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.02s
0m00.64s | Spec/EdDSA | 0m00.93s || -0m00.29s
0m00.64s | Testbit | 0m00.94s || -0m00.29s
0m00.63s | Encoding/ModularWordEncodingTheorems | 0m00.66s || -0m00.03s
0m00.62s | Assembly/AlmostQhasm | 0m00.49s || +0m00.13s
0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.02s
0m00.49s | Spec/WeierstrassCurve | 0m00.43s || +0m00.06s
0m00.49s | Assembly/QhasmUtil | 0m00.51s || -0m00.02s
0m00.49s | ModularArithmetic/Pre | 0m00.47s || +0m00.02s
0m00.47s | Assembly/Vectorize | 0m00.51s || -0m00.04s
0m00.46s | Assembly/AlmostConversion | 0m00.44s || +0m00.02s
0m00.42s | ModularArithmetic/Pow2Base | 0m00.42s || +0m00.00s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.45s || -0m00.04s
0m00.41s | Spec/ModularArithmetic | 0m00.41s || +0m00.00s
0m00.39s | Spec/CompleteEdwardsCurve | 0m00.41s || -0m00.01s
0m00.03s | Util/Notations | 0m00.03s || +0m00.00s
Diffstat (limited to 'src/Algebra.v')
-rw-r--r-- | src/Algebra.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index f4afcb935..9bd3cac5e 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -9,12 +9,11 @@ Require Export Crypto.Util.FixCoqMistakes. Module Import ModuloCoq8485. Import NPeano Nat. - Infix "mod" := modulo (at level 40, no associativity). + Infix "mod" := modulo. End ModuloCoq8485. Notation is_eq_dec := (DecidableRel _) (only parsing). -Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) - (at level 10, T at level 8, R at level 8, only parsing). +Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (only parsing). Notation eq_dec x y := (@dec (_ x y) _) (only parsing). Notation "x =? y" := (eq_dec x y) : type_scope. @@ -305,7 +304,7 @@ Module Group. Lemma surjective_homomorphism_from_group {G EQ OP ID INV} {groupG:@group G EQ OP ID INV} {H eq op id inv} - {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y}} + {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} } {Proper_op:Proper(eq==>eq==>eq)op} {Proper_inv:Proper(eq==>eq)inv} {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph} @@ -330,7 +329,7 @@ Module Group. Lemma isomorphism_to_subgroup_group {G EQ OP ID INV} - {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OP:Proper(EQ==>EQ==>EQ)OP} {Proper_INV:Proper(EQ==>EQ)INV} {H eq op id inv} {groupG:@group H eq op id inv} @@ -534,7 +533,7 @@ Module Ring. Lemma isomorphism_to_subring_ring {T EQ ZERO ONE OPP ADD SUB MUL} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OPP:Proper(EQ==>EQ)OPP} {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} @@ -664,7 +663,7 @@ Module Field. Lemma isomorphism_to_subfield_field {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } {Proper_OPP:Proper(EQ==>EQ)OPP} {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} |