diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-07-07 00:18:13 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-07-07 00:18:13 -0400 |
| commit | bf8572ea461758b8b66155ec6573d8f99c59065e (patch) | |
| tree | 8f734b35ae6ae2cb7011df0bdeda20413ca394ee /src/Arithmetic/ModularArithmeticTheorems.v | |
| parent | 18cb95257b2707cb3ead6f4f4de7ccb9f4e532e8 (diff) | |
enforce use of [F.zero], [F.one]; prove Ed25519 admits
Diffstat (limited to 'src/Arithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index d634cc0ce..666dd54eb 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -15,7 +15,7 @@ Module F. Ltac unwrap_F := intros; repeat match goal with [ x : F _ |- _ ] => destruct x end; - lazy iota beta delta [F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *; + lazy iota beta delta [F.one F.zero F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *; try apply eqsig_eq; pull_Zmod. @@ -63,7 +63,7 @@ Module F. Proof using Type. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. Lemma to_Z_nonzero (x:F m) : x <> 0 -> F.to_Z x <> 0%Z. - Proof using Type. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. + Proof using Type. cbv [F.zero]. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. Lemma to_Z_range (x : F m) : 0 < m -> 0 <= F.to_Z x < m. Proof using Type. intros. rewrite <- mod_to_Z. apply Z.mod_pos_bound. trivial. Qed. |