From 058fcebd2ededf7b3ddc803d39ac067032dba7c0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Jun 2016 17:47:07 -0700 Subject: Fix a missing mod resolution Apparently this only triggered in 8.4 --- src/Experiments/DerivationsOptionRectLetInEncoding.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Experiments') diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index d03bafbb1..e5b74085e 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -335,10 +335,15 @@ Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). re Definition natToField {m} x : F m := ZToField (Z.of_nat x). Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x). + +Section with_unqualified_modulo2. +Import NPeano Nat. +Local Infix "mod" := modulo : nat_scope. Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x). unfold natToField, FieldToNat; intros. rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial. Qed. +End with_unqualified_modulo2. Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. Proof. -- cgit v1.2.3