More changes for 8.5

[Local Coercion :=] changed meanings.  Use [Let] and [Local Coercion] for consistent behavior

4 files changed, 36 insertions, 35 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..322db1792 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,9 +1,11 @@
 Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Coq.omega.Omega.
 
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope Z_scope.
 Local Open Scope F_scope.
-  
+
 Section Pre.
   Context {q : BinInt.Z}.
   Context {a : F q}.
@@ -20,8 +22,8 @@ Section Pre.
      postprocess [Fpostprocess],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   (* the canonical definitions are in Spec *)
   Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
   Local Notation unifiedAdd' P1' P2' := (
@@ -29,7 +31,7 @@ Section Pre.
     let '(x2, y2) := P2' in
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
   ).
-  
+
   Lemma char_gt_2 : ZToField 2 <> (0: F q).
     intro; find_injection.
     pose proof two_lt_q.
@@ -38,7 +40,7 @@ Section Pre.
 
   Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
   Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
-  
+
   Ltac whatsNotZero :=
     repeat match goal with
     | [H: ?lhs = ?rhs |- _ ] =>
@@ -67,11 +69,11 @@ Section Pre.
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
     intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
-  
-    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
     destruct a_square as [sqrt_a a_square'].
     rewrite <-a_square' in *.
-  
+
     (* Furthermore... *)
     pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
     rewrite Hc2 in Heqt at 2.
@@ -80,7 +82,7 @@ Section Pre.
     rewrite Hcontra in Heqt.
     replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
     rewrite <-Hc1 in Heqt.
-  
+
     (* main equation for both potentially nonzero denominators *)
     destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
       try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
@@ -97,11 +99,11 @@ Section Pre.
             destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
         end
       end.
-  
+
     assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
-  
+
     replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
-  
+
     (* contradiction: product of nonzero things is zero *)
     destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
     destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
@@ -119,7 +121,7 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
       intro Hz; rewrite Hz in H; intuition.
   Qed.
-  
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) ->
     onCurve (x2, y2) ->
@@ -130,27 +132,27 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
       intro Hz; rewrite Hz in H; apply H; field.
   Qed.
-  
+
   Definition zeroOnCurve : onCurve (0, 1).
     simpl. field.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
     (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
     onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
   Proof.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
-      * c=1 and an extra a in front of x^2 *) 
-  
+      * c=1 and an extra a in front of x^2 *)
+
     injection H; clear H; intros.
-  
+
     Ltac t x1 y1 x2 y2 :=
       assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
              = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
       assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
              = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
     t x1 y1 x2 y2; t x2 y2 x1 y1.
-  
+
     remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
       (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
     assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
@@ -158,7 +160,7 @@ Section Pre.
     (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
      y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
     replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-  
+
     match goal with [ |- ?x = 1 ] => replace x with
     ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
      ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
@@ -175,7 +177,7 @@ Section Pre.
       auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
         edwardsAddCompleteMinus, edwardsAddCompletePlus.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
     onCurve (unifiedAdd' P1 P2).
   Proof.
@@ -183,4 +185,4 @@ Section Pre.
     remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
     eapply unifiedAdd'_onCurve'; eauto.
   Qed.
-End Pre.
\ No newline at end of file
+End Pre.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 8566177a1..6168f88bd 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -11,7 +11,7 @@ Require Export Crypto.Util.IterAssocOp.
 
 Section ModularArithmeticPreliminaries.
   Context {m:Z}.
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm.
+  Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
 
   Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
   Proof.
@@ -318,7 +318,7 @@ End FandZ.
 
 Section RingModuloPre.
   Context {m:Z}.
-  Local Coercion ZToFm' := ZToField : Z -> F m. Hint Unfold ZToFm'.
+  Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
   (* Substitution to prove all Compats *)
   Ltac compat := repeat intro; subst; trivial.
 
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index d6c7fa4b8..7d354ab3e 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -9,9 +9,9 @@ Section Mod24.
 
   (* Specify modulus *)
   Let q := 24.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [ring]. Similar boilerplate works for [field] if
   the modulus is prime . *)
@@ -21,7 +21,7 @@ Section Mod24.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
   Proof.
@@ -37,9 +37,9 @@ Section Modq.
 
   (* Set notations + - * / refer to F operations *)
   Local Open Scope F_scope.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [field]. Similar boilerplate works for [ring] if
   the modulus is not prime . *)
@@ -49,7 +49,7 @@ Section Modq.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
   Proof.
@@ -170,7 +170,7 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; try exact Fq_1_neq_0.
   Qed.
 
-  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, 
+  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
    ZQ <> 0 ->
    ZP <> 0 ->
    ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
@@ -187,4 +187,3 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; assumption.
   Qed.
 End TimesZeroParametricTestModule.
-
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 76efe3d79..8ee07fe5d 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -26,8 +26,8 @@ Section FieldOperations.
   Context {m : BinInt.Z}.
 
   (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *)
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m.
-  
+  Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F.
+
   Definition add (a b:F m) : F m := ZToField (a + b).
   Definition mul (a b:F m) : F m := ZToField (a * b).
 
@@ -69,4 +69,4 @@ Infix "-" := sub : F_scope.
 Infix "/" := div : F_scope.
 Infix "^" := pow : F_scope.
 Notation "0" := (ZToField 0) : F_scope.
-Notation "1" := (ZToField 1) : F_scope.
\ No newline at end of file
+Notation "1" := (ZToField 1) : F_scope.