diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-09-17 17:58:16 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-09-17 23:55:12 -0400 |
| commit | a5906d5e6b22e93377e786200e206921215fb5df (patch) | |
| tree | 8c593dcbea60c578799514d302f56b0d2aad769f /src | |
| parent | 05cf7a292393567d696630dc4ed050a5da3672a1 (diff) | |
overlflow-checking ZToGF function
Diffstat (limited to 'src')
| -rw-r--r-- | src/Galois/GaloisField.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v index 5add86af9..860e830b9 100644 --- a/src/Galois/GaloisField.v +++ b/src/Galois/GaloisField.v @@ -1,6 +1,7 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import Eqdep_dec. +Require Import Tactics.VerdiTactics. Section GaloisPreliminaries. Definition Prime := {x: Z | prime x}. @@ -20,6 +21,17 @@ Module GaloisField (M: Modulus). Definition GFToZ(x: GF) := proj1_sig x. Coercion GFToZ: GF >-> Z. + Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True. + break_if; [|trivial]. + exists x. + destruct (Bool.andb_true_eq _ _ (eq_sym Heqb)); clear Heqb. + erewrite Zmod_small; [trivial|]. + intuition. + - rewrite <- Z.leb_le; auto. + - rewrite <- Z.ltb_lt; auto. + Defined. + + Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. Proof. destruct x, y; intuition; simpl in *; try congruence. |