aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-09-16 12:56:10 -0400
committerGravatar Andres Erbsen <andreser@mit.edu>2016-09-16 19:00:06 -0400
commite51fb9ecd03fb1ce14870b40312d7259da0c4776 (patch)
tree972dec549752fa9379a34f51913039c84339de11 /src
parentd69661159ba18e05815e442d727e20b05b4343ad (diff)
ModularArithmetic: conversions between [F] and [nat]
Diffstat (limited to 'src')
-rw-r--r--src/ModularArithmetic/ModularArithmeticTheorems.v36
-rw-r--r--src/Spec/ModularArithmetic.v13
2 files changed, 48 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index ca7cb4ef4..5984b4e6d 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -139,6 +139,42 @@ Module F.
Qed.
End FandZ.
+ Section FandNat.
+ Import NPeano Nat.
+ Local Infix "mod" := modulo : nat_scope.
+ Local Open Scope nat_scope.
+
+ Context {m} (m_pos: (0 < m)%Z).
+ Let to_nat_m_nonzero : Z.to_nat m <> 0.
+ rewrite Z2Nat.inj_lt in m_pos; omega.
+ Qed.
+
+ Lemma to_nat_of_nat (n:nat) : F.to_nat (F.of_nat m n) = (n mod (Z.to_nat m))%nat.
+ Proof.
+ unfold F.to_nat, F.of_nat.
+ rewrite F.to_Z_of_Z.
+ pose proof (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero) as Hmod.
+ rewrite Z2Nat.id in Hmod by omega.
+ rewrite <- Hmod.
+ rewrite <-Nat2Z.id by omega.
+ reflexivity.
+ Qed.
+
+ Lemma of_nat_to_nat x : F.of_nat m (F.to_nat x) = x.
+ unfold F.to_nat, F.of_nat.
+ rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; trivial].
+ Qed.
+
+ Lemma of_nat_mod (n:nat) : F.of_nat m (n mod (Z.to_nat m)) = F.of_nat m n.
+ Proof.
+ unfold F.of_nat.
+ replace (Z.of_nat (n mod Z.to_nat m)) with(Z.of_nat n mod Z.of_nat (Z.to_nat m))%Z
+ by (symmetry; eapply (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero)).
+ rewrite Z2Nat.id by omega.
+ rewrite <-F.of_Z_mod; reflexivity.
+ Qed.
+ End FandNat.
+
Section RingTacticGadgets.
Context (m:Z).
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 95d7d4e75..a3e80fcf9 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -22,6 +22,7 @@ Local Open Scope Z_scope.
Module F.
Definition F (m : BinInt.Z) := { z : BinInt.Z | z = z mod m }.
+ Bind Scope F_scope with F.
Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod.
Program Definition of_Z m (a:BinNums.Z) : F m := a mod m.
Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a.
@@ -50,6 +51,16 @@ Module F.
} := Pre.pow_impl.
Definition pow : F m -> BinNums.N -> F m := Eval hnf in proj1_sig pow_with_spec.
End FieldOperations.
+
+ Definition of_nat m (n:nat) := F.of_Z m (BinInt.Z.of_nat n).
+ Definition to_nat {m} (x:F m) := BinInt.Z.to_nat (F.to_Z x).
+ Notation nat_mod := of_nat (only parsing).
+
+ Definition of_N m n := F.of_Z m (BinInt.Z.of_N n).
+ Definition to_N {m} (x:F m) := BinInt.Z.to_N (F.to_Z x).
+ Notation N_mod := of_N (only parsing).
+
+ Notation Z_mod := of_Z (only parsing).
End F.
Notation F := F.F.
@@ -61,4 +72,4 @@ Infix "-" := F.sub : F_scope.
Infix "/" := F.div : F_scope.
Infix "^" := F.pow : F_scope.
Notation "0" := (F.of_Z _ 0) : F_scope.
-Notation "1" := (F.of_Z _ 1) : F_scope. \ No newline at end of file
+Notation "1" := (F.of_Z _ 1) : F_scope.