port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer nonzero ports. remove FField and FNsatz

8 files changed, 396 insertions, 361 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index f6b2fa330..27c0d2e59 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -181,6 +181,15 @@ Module Monoid.
   End Monoid.
 End Monoid.
 
+Section ZeroNeqOne.
+  Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}.
+
+  Lemma one_neq_zero : not (eq one zero).
+  Proof.
+    intro HH; symmetry in HH. auto using zero_neq_one.
+  Qed.
+End ZeroNeqOne.
+
 Module Group.
   Section BasicProperties.
     Context {T eq op id inv} `{@group T eq op id inv}.
@@ -195,11 +204,37 @@ Module Group.
     Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
     Lemma inv_op x y : (inv y*inv x)*(x*y) =id.
     Proof. eauto using Monoid.inv_op, left_inverse. Qed.
+
+    Lemma inv_unique x ix : ix * x = id -> ix = inv x.
+    Proof.
+      intro Hix.
+      cut (ix*x*inv x = inv x).
+      - rewrite <-associative, right_inverse, right_identity; trivial.
+      - rewrite Hix, left_identity; reflexivity.
+    Qed.
+
+    Lemma inv_id : inv id = id.
+    Proof. symmetry. eapply inv_unique, left_identity. Qed.
+
+    Lemma inv_nonzero_nonzero : forall x, x <> id -> inv x <> id.
+    Proof.
+      intros ? Hx Ho.
+      assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity).
+      rewrite Ho, right_identity in Hxo. intuition.
+   Qed.
+
+    Section ZeroNeqOne.
+      Context {one} `{is_zero_neq_one T eq id one}.
+      Lemma opp_one_neq_zero : inv one <> id.
+      Proof. apply inv_nonzero_nonzero, one_neq_zero. Qed.
+      Lemma zero_neq_opp_one : id <> inv one.
+      Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
+    End ZeroNeqOne.
   End BasicProperties.
 
   Section Homomorphism.
-    Context {H eq op id inv} `{@group H eq op id inv}.
-    Context {G EQ OP ID INV} `{@group G EQ OP ID INV}.
+    Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
+    Context {H eq op id inv} {groupH:@group H eq op id inv}.
     Context {phi:G->H}.
     Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
 
@@ -296,6 +331,8 @@ Module Ring.
       rewrite <-!associative, right_inverse, right_identity; reflexivity.
     Qed.
 
+    Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero.
+
     Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul).
     Proof.
       split; intros. rewrite !ring_sub_definition, left_distributive.
@@ -319,13 +356,6 @@ Module Ring.
       - intros; eapply right_distributive.
       - intros; eapply left_distributive.
     Qed.
-    
-    Lemma opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0.
-    Proof.
-      intros ? Hx Ho.
-      assert (Hxo: x + opp x = 0) by (rewrite right_inverse; reflexivity).
-      rewrite Ho, right_identity in Hxo. intuition.
-   Qed.
   End Ring.
 
   Section Homomorphism.
@@ -382,7 +412,7 @@ Module Ring.
 End Ring.
 
 Module IntegralDomain.
-  Section CommutativeRing.
+  Section IntegralDomain.
     Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}.
     
     Lemma mul_nonzero_nonzero_cases (x y : T)
@@ -400,7 +430,7 @@ Module IntegralDomain.
       - auto using mul_nonzero_nonzero_cases.
       - intro bad; symmetry in bad; auto using zero_neq_one.
     Qed.
-  End CommutativeRing.
+  End IntegralDomain.
 End IntegralDomain.
 
 Module Field.
@@ -454,7 +484,6 @@ Module Field.
   End Homomorphism.
 End Field.
 
-
 (*** Tactics for manipulating field equations *)
 Require Import Coq.setoid_ring.Field_tac.
 
@@ -488,7 +517,7 @@ Ltac common_denominator_in H :=
 
 Ltac common_denominator_all := 
   common_denominator;
-  repeat match goal with [H: _ |- _ _ _ ] => common_denominator_in H end.
+  repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end.
 
 Inductive field_simplify_done {T} : T -> Type :=
   Field_simplify_done : forall H, field_simplify_done H.
@@ -510,15 +539,22 @@ Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
 
 (*** Polynomial equations over fields *)
 
+Ltac neq01 :=
+  try solve
+      [apply zero_neq_one
+      |apply Group.zero_neq_opp_one
+      |apply one_neq_zero
+      |apply Group.opp_one_neq_zero].
+
 Ltac field_algebra :=
   intros;
   common_denominator_all;
   try (nsatz; dropRingSyntax);
   repeat (apply conj);
   try solve
-      [nsatz_nonzero
-      |apply Ring.opp_nonzero_nonzero;trivial
-      |unfold not; intro; nsatz_contradict].
+      [neq01
+      |trivial
+      |apply Ring.opp_nonzero_nonzero;trivial].
 
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 4ad76856e..e6ec7ab86 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -4,6 +4,9 @@ Require Import Crypto.Algebra Crypto.Nsatz.
 Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Crypto.Util.Fieldwise.
 
 Module E.
   Import Group Ring Field CompleteEdwardsCurve.E.
@@ -21,12 +24,10 @@ Module E.
 
     Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)).
   
-    Definition eq (P Q:point) :=
-      let Feq2 (ab xy:F*F) := fst ab = fst xy /\ snd ab = snd xy in
-      Feq2 (coordinates P) (coordinates Q).
+    Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q).
     Infix "=" := eq : E_scope.
   
-    (* TODO:port
+    (* TODO: decide whether we still want something like this, then port
     Local Ltac t :=
       unfold point_eqb;
         repeat match goal with
@@ -108,23 +109,30 @@ Module E.
       exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
     Solve All Obligations using intros; destruct_points; simpl; field_algebra.
 
+    Ltac bash :=
+      repeat match goal with
+             | |- _ => progress intros
+             | [H: _ /\ _ |- _ ] => destruct H
+             | |- _ => progress destruct_points
+             | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in *
+             | |- _ => split
+             | |- Feq _ _ => field_algebra
+             | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
+             | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
+             end.
+
+    Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed.
+    Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed.
+    Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. bash. Qed.
+
     Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof.
-        repeat match goal with
-               | |- _ => progress intros
-               | [H: _ /\ _ |- _ ] => destruct H
-               | |- _ => progress destruct_points
-               | |- _ => progress cbv [fst snd coordinates proj1_sig eq add zero opp] in *
-               | |- _ => split
-               | |- Feq _ _ => common_denominator_all; try nsatz
-               | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
-               | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
-               end.
-        (* TODO: port denominator-nonzero proofs for associativity *)
-        match goal with | |- _ <> 0 => admit end.
-        match goal with | |- _ <> 0 => admit end.
-        match goal with | |- _ <> 0 => admit end.
-        match goal with | |- _ <> 0 => admit end.
+      bash.
+      (* TODO: port denominator-nonzero proofs for associativity *)
+      match goal with | |- _ <> 0 => admit end.
+      match goal with | |- _ <> 0 => admit end.
+      match goal with | |- _ <> 0 => admit end.
+      match goal with | |- _ <> 0 => admit end.
     Qed.
 
     (* TODO: move to [Group] and [AbelianGroup] as appropriate *)
@@ -144,13 +152,8 @@ Module E.
     Qed.
     Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
     Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
-    (*
     Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
-    Proof.
-      induction n. intros. simpl. admit.
-    Qed.
-     *)
-  
+    Admitted.
 
     Section PointCompression.
       Local Notation "x ^2" := (x*x).
@@ -169,4 +172,57 @@ Module E.
       Qed.
     End PointCompression.
   End CompleteEdwardsCurveTheorems.
+
+  Section Homomorphism.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
+            {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
+    Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
+            {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+            {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
+    Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
+                                                   K Keq Kone Kadd Kmul phi}.
+    Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}.
+    Local Notation Fpoint := (@point F Feq Fone Fadd Fmul Fa Fd).
+    Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd).
+
+    Create HintDb field_homomorphism discriminated.
+    Hint Rewrite <-
+         homomorphism_one
+         homomorphism_add 
+         homomorphism_sub 
+         homomorphism_mul 
+         homomorphism_div 
+         Ha
+         Hd
+      : field_homomorphism.
+
+    Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
+      let (x, y) := coordinates P in (phi x, phi y)) _.
+    Next Obligation.
+      destruct P as [[? ?] ?]; simpl.
+      rewrite_strat bottomup hints field_homomorphism.
+      eauto using is_homomorphism_phi_proper; assumption.
+    Qed.
+
+    Context {point_phi:Fpoint->Kpoint}
+            {point_phi_Proper:Proper (eq==>eq) point_phi}
+            {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}.
+
+    Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
+    Proof.
+      repeat match goal with
+             | |- Group.is_homomorphism => split
+             | |- _ => intro
+             | |-  _ /\ _ => split
+             | [H: _ /\ _ |- _ ] => destruct H
+             | [p: point |- _ ] => destruct p as [[??]?]
+             | |- context[point_phi] => setoid_rewrite point_phi_correct
+             | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in *
+             | |- Keq ?x ?x => reflexivity
+             | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism
+             | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition]
+             end.
+      Qed.
+  End Homomorphism.
 End E.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 44033097d..4a352c738 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -1,202 +1,154 @@
-Require Import Crypto.CompleteEdwardsCurve.Pre.
-Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.FField.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Util.IterAssocOp BinNat NArith.
-Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
-Local Open Scope equiv_scope.
-Local Open Scope F_scope.
-
-Section ExtendedCoordinates.
-  Context {prm:TwistedEdwardsParams}.
-  Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *)
-  Existing Instance prime_q.
-
-  Add Field Ffield_p' : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
-
-  Add Field Ffield_notConstant : (OpaqueFieldTheory q)
-    (constants [notConstant]).
-
-  (** [extended] represents a point on an elliptic curve using extended projective
-  * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
-  Record extended := mkExtended {extendedX : F q;
-                                 extendedY : F q;
-                                 extendedZ : F q;
-                                 extendedT : F q}.
-  Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
-
-  Definition twistedToExtended (P : (F q*F q)) : extended :=
-    let '(x, y) := P in (x, y, 1, x*y).
-  Definition extendedToTwisted (P : extended) : F q * F q :=
-    let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)).
-  Definition rep (P:extended) (rP:(F q*F q)) : Prop :=
-    let '(X, Y, Z, T) := P in
-    extendedToTwisted P = rP /\
-    Z <> 0 /\
-    T = X*Y/Z.
-  Local Hint Unfold twistedToExtended extendedToTwisted rep.
-  Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-
-  Ltac unfoldExtended :=
-    repeat progress (autounfold; unfold E.onCurve, E.add, E.add', rep in *; intros);
-    repeat match goal with
-      | [ p : (F q*F q)%type |- _ ] =>
-          let x := fresh "x" p in
-          let y := fresh "y" p in
-          destruct p as [x y]
-      | [ p : extended |- _ ] =>
-          let X := fresh "X" p in
-          let Y := fresh "Y" p in
-          let Z := fresh "Z" p in
-          let T := fresh "T" p in
-          destruct p as [X Y Z T]
-      | [ H: _ /\ _ |- _ ] => destruct H
-      | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H
-      | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H
-  end.
-
-  Ltac solveExtended := unfoldExtended;
-    repeat match goal with
-      | [ |- _ /\ _ ] => split
-      | [ |- @eq (F q * F q)%type _ _] => apply f_equal2
-      | _ => progress rewrite ?@F_add_0_r, ?@F_add_0_l, ?@F_sub_0_l, ?@F_sub_0_r,
-           ?@F_mul_0_r, ?@F_mul_0_l, ?@F_mul_1_l, ?@F_mul_1_r, ?@F_div_1_r
-      | _ => solve [eapply @Fq_1_neq_0; eauto with typeclass_instances]
-      | _ => solve [eauto with typeclass_instances]
-      | [ H: a = _ |- _ ] => rewrite H
-  end.
-
-  Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P.
-  Proof.
-    solveExtended.
-  Qed.
-
-  Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP.
-  Proof.
-    solveExtended.
-  Qed.
-
-  Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }.
-
-  Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended.
-  Next Obligation.
-    destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
-  Qed.
-
-  Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted.
-  Next Obligation.
-    destruct x; simpl; intuition.
-  Qed.
-
-  Definition extendedPoint_eq P Q := unExtendedPoint P = unExtendedPoint Q.
-  Global Instance Equivalence_extendedPoint_eq : Equivalence extendedPoint_eq.
-  Proof.
-    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
-  Qed.
-
-  Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P.
-  Proof.
-    destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
-  Qed.
-
-  Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint.
-  Proof.
-    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
-  Qed.
-
-  Global Instance Proper_unExtendedPoint : Proper (equiv==>eq) unExtendedPoint.
-  Proof.
-    repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence.
-  Qed.
-
-  Definition twice_d := d + d.
-
-  Section TwistMinus1.
-    Context (a_eq_minus1 : a = opp 1).
-    (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
-    Definition unifiedAddM1' (P1 P2 : extended) : extended :=
-      let '(X1, Y1, Z1, T1) := P1 in
-      let '(X2, Y2, Z2, T2) := P2 in
-      let  A := (Y1-X1)*(Y2-X2) in
-      let  B := (Y1+X1)*(Y2+X2) in
-      let  C := T1*twice_d*T2 in
-      let  D := Z1*(Z2+Z2) in
-      let  E := B-A in
-      let  F := D-C in
-      let  G := D+C in
-      let  H := B+A in
-      let X3 := E*F in
-      let Y3 := G*H in
-      let T3 := E*H in
-      let Z3 := F*G in
-      (X3, Y3, Z3, T3).
-    Local Hint Unfold E.add.
-
-    Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
-
-    Lemma F_mul_2_l : forall x : F q, ZToField 2 * x = x + x.
-      intros. ring.
-    Qed.
-
-    Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ).
-    Proof.
-      intros P Q rP rQ HoP HoQ HrP HrQ.
-      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
-      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
-      unfoldExtended; unfold twice_d; rewrite a_eq_minus1 in *; simpl in *. repeat rewrite <-F_mul_2_l.
-        repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto;
-        repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
-           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r;
-        field_nonzero tnz.
-    Qed.
-
-    Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q).
-    Proof.
-      intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto.
-    Qed.
-
-    Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'.
-    Next Obligation.
-      destruct x, x0; simpl; intuition.
-      - erewrite extendedToTwisted_rep; eauto using unifiedAddM1'_rep.
-      - erewrite extendedToTwisted_rep.
-        (* It would be nice if I could use eauto here, but it gets evars wrong :( *)
-        2: eapply unifiedAddM1'_rep. 5:apply H1. 4:apply H. 3:auto. 2:auto.
-        eauto using unifiedAdd'_onCurve.
-    Qed.
-
-    Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q).
-    Proof.
-      destruct P, Q; unfold unExtendedPoint, E.add, unifiedAddM1; eapply E.point_eq; simpl in *; intuition.
-      pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0));
-        destruct (unifiedAddM1' x x0);
-        unfold rep in *; intuition.
-    Qed.
-
-    Lemma unifiedAddM1_correct : forall P Q, mkExtendedPoint (E.add P Q) === unifiedAddM1 (mkExtendedPoint P) (mkExtendedPoint Q).
-    Proof.
-      unfold equiv, extendedPoint_eq; intros;
-        pose proof unifiedAddM1_rep (mkExtendedPoint P) (mkExtendedPoint Q);
-        pose proof unExtendedPoint_mkExtendedPoint;
-        congruence.
-    Qed.
-
-    Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1.
-    Proof.
-      repeat (econstructor || intro).
-      repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq.
-      rewrite <-!unifiedAddM1_rep.
-      destruct x, y, x0, y0; simpl in *; eapply E.point_eq; congruence.
-    Qed.
+Require Export Crypto.Spec.CompleteEdwardsCurve.
 
+Require Import Crypto.Algebra Crypto.Nsatz.
+Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Coq.Logic.Eqdep_dec.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Crypto.Util.Fieldwise.
+
+Module Extended.
+  Section ExtendedCoordinates.
+    Import Group Ring Field.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
+            {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {prm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
+    Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d).
+
+    Add Field _edwards_curve_extended_field : (field_theory_for_stdlib_tactic (H:=field)).
+
+    (** [Extended.point] represents a point on an elliptic curve using extended projective
+     * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
+    Definition point := { P | let '(X,Y,Z,T) := P in onCurve((X/Z), (Y/Z)) /\ Z<>0 /\ Z*T=X*Y }.
+    Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
+
+    Create HintDb bash discriminated.
+    Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash.
+    Ltac bash :=
+      repeat match goal with
+             | |- Proper _ _ => intro
+             | _ => progress intros
+             | [ H: _ /\ _ |- _ ] => destruct H
+             | [ p:E.point |- _ ] => destruct p as [[??]?]
+             | [ p:point |- _ ] => destruct p as [[[[??]?]?]?]
+             | _ => progress autounfold with bash in *
+             | |- _ /\ _ => split
+             | _ => solve [neq01]
+             | _ => solve [eauto]
+             | _ => solve [intuition]
+             | _ => solve [etransitivity; eauto]
+             | |- Feq _ _ => field_algebra
+             | |- _ <> 0 => apply mul_nonzero_nonzero
+             | [ H : _ <> 0 |- _ <> 0 ] =>
+               intro; apply H;
+               field_algebra;
+               solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2
+                     | apply E.char_gt_2]
+             end.
+
+    Obligation Tactic := bash.
+
+    Program Definition from_twisted (P:Epoint) : point := exist _
+      (let (x,y) := E.coordinates P in (x, y, 1, x*y)) _.
+
+    Program Definition to_twisted (P:point) : Epoint := exist _
+      (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _.
+
+    Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q).
+
+    Local Hint Unfold from_twisted to_twisted eq : bash.
+
+    Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; bash. Qed.
+    Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. bash. Qed.
+    Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. bash. Qed.
+    Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. Proof. bash. Qed.
+
+    Section TwistMinus1.
+      Context {a_eq_minus1 : a = Fopp 1}.
+      Context {twice_d:F} {Htwice_d:twice_d = d + d}.
+      (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
+      Definition add_coordinates P1 P2 : F*F*F*F :=
+        let '(X1, Y1, Z1, T1) := P1 in
+        let '(X2, Y2, Z2, T2) := P2 in
+        let  A := (Y1-X1)*(Y2-X2) in
+        let  B := (Y1+X1)*(Y2+X2) in
+        let  C := T1*twice_d*T2 in
+        let  D := Z1*(Z2+Z2) in
+        let  E := B-A in
+        let  F := D-C in
+        let  G := D+C in
+        let  H := B+A in
+        let X3 := E*F in
+        let Y3 := G*H in
+        let T3 := E*H in
+        let Z3 := F*G in
+        (X3, Y3, Z3, T3).
+
+      Local Hint Unfold E.add E.coordinates add_coordinates : bash.
+
+      Lemma add_coordinates_correct (P Q:point) :
+        let '(X,Y,Z,T) := add_coordinates (coordinates P) (coordinates Q) in
+        let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in
+        (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z).
+      Proof.
+        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ.
+        pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ.
+        bash.
+      Qed.
+
+      Obligation Tactic := idtac.
+      Program Definition add (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q).
+      Next Obligation.
+        intros.
+        pose proof (add_coordinates_correct P Q) as Hrep.
+        pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon.
+        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz1.
+        pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz2.
+        autounfold with bash in *; simpl in *.
+        destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB.
+        bash.
+      Qed.
+      Local Hint Unfold add : bash.
+
+      Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)).
+      Proof.
+        pose proof (add_coordinates_correct P Q) as Hrep.
+        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        autounfold with bash in *; simpl in *.
+        destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB.
+        split; reflexivity.
+      Qed.
+      
+      Global Instance Proper_add : Proper (eq==>eq==>eq) add.
+      Proof.
+        unfold eq. intros x y H x0 y0 H0.
+        transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity.
+      Qed.
+
+      Lemma homomorphism_to_twisted : @Group.is_homomorphism point eq add Epoint E.eq E.add to_twisted.
+      Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed.
+
+      Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)).
+      Proof.
+        pose proof (to_twisted_add (from_twisted P) (from_twisted Q)).
+        unfold eq; rewrite !to_twisted_from_twisted in *.
+        symmetry; assumption.
+      Qed.
+
+      Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted.
+      Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed.
+
+      (* TODO: decide whether we still need those, then port *)
+    (*
     Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P.
       unfold equiv, extendedPoint_eq; intros.
       rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto.
@@ -223,19 +175,70 @@ Section ExtendedCoordinates.
       unfold E.mul; fold E.mul.
       rewrite <-IHn, unifiedAddM1_rep; auto.
     Qed.
-  End TwistMinus1.
-
-  Definition negateExtended' P := let '(X, Y, Z, T) := P in (opp X, Y, Z, opp T).
-  Program Definition negateExtended (P:extendedPoint) : extendedPoint := negateExtended' (proj1_sig P).
-  Next Obligation.
-  Proof.
-    unfold negateExtended', rep; destruct P as [[X Y Z T] H]; simpl. destruct H as [[[] []] ?]; subst.
-    repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; repeat split; trivial.
-  Qed.
-  
-  Lemma negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P).
-  Proof.
-    unfold E.opp, unExtendedPoint, negateExtended; destruct P as [[]]; simpl; intros.
-    eapply E.point_eq; repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial.
-  Qed.
-End ExtendedCoordinates.
+     *)
+    End TwistMinus1.
+  End ExtendedCoordinates.
+
+  Section Homomorphism.
+    Import Group Ring Field.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
+            {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Fprm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
+    Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
+            {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+            {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
+    Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
+                                                   K Keq Kone Kadd Kmul phi}.
+    Context {phi_nonzero : forall x, ~ Feq x Fzero -> ~ Keq (phi x) Kzero}.
+    Context {HFa: Feq Fa (Fopp Fone)} {HKa:Keq Ka (Kopp Kone)}.
+    Context {Hd:Keq (phi Fd) Kd} {Kdd Fdd} {HKdd:Keq Kdd (Kadd Kd Kd)} {HFdd:Feq Fdd (Fadd Fd Fd)}.
+    Local Notation Fpoint := (@point F Feq Fzero Fone Fadd Fmul Fdiv Fa Fd).
+    Local Notation Kpoint := (@point K Keq Kzero Kone Kadd Kmul Kdiv Ka Kd).
+
+    Lemma Ha : Keq (phi Fa) Ka.
+    Proof. rewrite HFa, HKa, <-homomorphism_one. eapply homomorphism_opp. Qed.
+
+    Lemma Hdd : Keq (phi Fdd) Kdd.
+    Proof. rewrite HFdd, HKdd. rewrite homomorphism_add. repeat f_equiv; auto. Qed.
+
+    Create HintDb field_homomorphism discriminated.
+    Hint Rewrite <-
+         homomorphism_one
+         homomorphism_add 
+         homomorphism_sub 
+         homomorphism_mul 
+         homomorphism_div 
+         Ha
+         Hd
+         Hdd
+      : field_homomorphism.
+
+    Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
+      let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _.
+    Next Obligation.
+      destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl.
+      rewrite_strat bottomup hints field_homomorphism.
+      eauto 10 using is_homomorphism_phi_proper, phi_nonzero.
+    Qed.
+
+    Context {point_phi:Fpoint->Kpoint}
+            {point_phi_Proper:Proper (eq==>eq) point_phi}
+            {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}.
+
+    Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi.
+    Proof.
+      repeat match goal with
+             | |- Group.is_homomorphism => split
+             | |- _ => intro
+             | |-  _ /\ _ => split
+             | [H: _ /\ _ |- _ ] => destruct H
+             | [p: point |- _ ] => destruct p as [[[[] ?] ?] [? [? ?]]]
+             | |- context[point_phi] => setoid_rewrite point_phi_correct
+             | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates ref_phi] in *
+             | |- Keq ?x ?x => reflexivity
+             | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism
+             | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition]
+             end.
+    Qed.
+  End Homomorphism.
+End Extended.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 19f2fd9db..4744afe6b 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
-Require Import Crypto.Algebra.
+Require Import Crypto.Algebra Crypto.Nsatz.
 
 Generalizable All Variables.
 Section Pre.
@@ -38,7 +38,7 @@ Section Pre.
         => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
                                            /(f (sqrt_a * x2) y2   *   x1 * y1           ))
       | _ => apply a_nonzero
-      end; field_algebra; auto using Ring.opp_nonzero_nonzero.
+      end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict.
   Qed.
 
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v
deleted file mode 100644
index 4f2b623e0..000000000
--- a/src/ModularArithmetic/FField.v
+++ /dev/null
@@ -1,63 +0,0 @@
-Require Export Crypto.Spec.ModularArithmetic.
-Require Export Coq.setoid_ring.Field.
-
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-
-Local Open Scope F_scope.
-
-Definition OpaqueF := F.
-Definition OpaqueZmodulo := BinInt.Z.modulo.
-Definition Opaqueadd {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @add p.
-Definition Opaquemul {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @mul p.
-Definition Opaquesub {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @sub p.
-Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p.
-Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p.
-Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p.
-Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p.
-Definition Opaqueadd_correct {p} : @Opaqueadd p = @add p := eq_refl.
-Definition Opaquesub_correct {p} : @Opaquesub p = @sub p := eq_refl.
-Definition Opaquemul_correct {p} : @Opaquemul p = @mul p := eq_refl.
-Definition Opaquediv_correct {p} : @Opaquediv p = @div p := eq_refl.
-Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField.
-
-Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p.
-
-Ltac FIELD_SIMPL_idtac FLD lH rl :=
-  let Simpl := idtac (* (protect_fv "field") *) in
-  let lemma := get_SimplifyEqLemma FLD in
-  get_FldPre FLD ();
-  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
-  get_FldPost FLD ().
-Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G.
-
-Ltac F_to_Opaque :=
-  change F with OpaqueF in *;
-  change BinInt.Z.modulo with OpaqueZmodulo in *;
-  change @add with @Opaqueadd in *;
-  change @mul with @Opaquemul in *;
-  change @sub with @Opaquesub in *;
-  change @div with @Opaquediv in *;
-  change @opp with @Opaqueopp in *;
-  change @inv with @Opaqueinv in *;
-  change @ZToField with @OpaqueZToField in *.
-
-Ltac F_from_Opaque p :=
-  change OpaqueF with F in *;
-  change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *;
-  change OpaqueZmodulo with BinInt.Z.modulo in *;
-  change @Opaqueopp with @opp in *;
-  change @Opaqueinv with @inv in *;
-  change @OpaqueZToField with @ZToField in *;
-  rewrite ?@Opaqueadd_correct, ?@Opaquesub_correct, ?@Opaquemul_correct, ?@Opaquediv_correct in *.
-
-Ltac F_field_simplify_eq :=
-  lazymatch goal with |- @eq (F ?p) _ _ =>
-    F_to_Opaque;
-    field_simplify_eq_idtac;
-    compute;
-    F_from_Opaque p
-  end.
-
-Ltac F_field := F_field_simplify_eq; [ring|..].
-
-Ltac notConstant t := constr:NotConstant.
diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v
deleted file mode 100644
index 221b8d799..000000000
--- a/src/ModularArithmetic/FNsatz.v
+++ /dev/null
@@ -1,40 +0,0 @@
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Export Crypto.ModularArithmetic.FField.
-Require Import Coq.nsatz.Nsatz.
-
-Ltac FqAsIntegralDomain :=
-  lazymatch goal with [H:Znumtheory.prime ?q |- _ ] =>
-    pose proof (_:@Integral_domain.Integral_domain (F q) _ _ _ _ _ _ _ _ _ _) as FqIntegralDomain;
-    lazymatch type of FqIntegralDomain with @Integral_domain.Integral_domain _ _ _ _ _ _ _ _ ?ringOps ?ringOk ?ringComm =>
-      generalize dependent ringComm; intro Cring;
-      generalize dependent ringOk; intro Ring;
-      generalize dependent ringOps; intro RingOps;
-      lazymatch type of RingOps with @Ncring.Ring_ops ?t ?z ?o ?a ?m ?s ?p ?e =>
-        generalize dependent e; intro equiv;
-        generalize dependent p; intro opp;
-        generalize dependent s; intro sub;
-        generalize dependent m; intro mul;
-        generalize dependent a; intro add;
-        generalize dependent o; intro one;
-        generalize dependent z; intro zero;
-        generalize dependent t; intro R
-      end
-    end; intros;
-    clear q H
-  end.
-
-Ltac fixed_equality_to_goal H x y := generalize (psos_r1 x y H); clear H.
-Ltac fixed_equalities_to_goal :=
-  match goal with
-  | H:?x == ?y |- _ => fixed_equality_to_goal H x y
-  | H:_ ?x ?y |- _ => fixed_equality_to_goal H x y
-  | H:_ _ ?x ?y |- _ => fixed_equality_to_goal H x y
-  | H:_ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y
-  | H:_ _ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y
-  end.
-Ltac fixed_nsatz :=
-  intros; try apply psos_r1b;
-   lazymatch goal with
-   | |- @equality ?T _ _ _ => repeat fixed_equalities_to_goal; nsatz_generic 6%N 1%Z (@nil T) (@nil T)
-  end.
-Ltac F_nsatz := abstract (FqAsIntegralDomain; fixed_nsatz).
diff --git a/src/Nsatz.v b/src/Nsatz.v
index c8a648626..469ba4c29 100644
--- a/src/Nsatz.v
+++ b/src/Nsatz.v
@@ -1,5 +1,5 @@
 (*** Tactics for manipulating polynomial equations *)
-Require Nsatz.
+Require Coq.nsatz.Nsatz.
 Require Import List.
 
 Generalizable All Variables.
@@ -109,6 +109,7 @@ Tactic Notation "nsatz" constr(n) :=
 Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
 
 Ltac nsatz_contradict :=
+  unfold not;
   intros;
   let domain := nsatz_guess_domain in
   lazymatch type of domain with
diff --git a/src/Util/Fieldwise.v b/src/Util/Fieldwise.v
new file mode 100644
index 000000000..f2f0b5acb
--- /dev/null
+++ b/src/Util/Fieldwise.v
@@ -0,0 +1,42 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+
+Fixpoint tuple' n T : Type :=
+  match n with
+  | O => T
+  | S n' => (tuple' n' T * T)%type
+  end.
+
+Definition tuple n T : Type :=
+  match n with
+    | O => unit
+    | S n' => tuple' n' T
+  end.
+
+Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' n A) (b:tuple' n B) {struct n} : Prop.
+  destruct n; simpl @tuple' in *.
+  { exact (R a b). }
+  { exact (R (snd a) (snd b) /\ fieldwise' _ _ n R (fst a) (fst b)). }
+Defined.
+
+Definition fieldwise {A B} (n:nat) (R:A->B->Prop) (a:tuple n A) (b:tuple n B) : Prop.
+  destruct n; simpl @tuple in *.
+  { exact True. }
+  { exact (fieldwise' _ R a b). }
+Defined.
+
+Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}:
+    Equivalence (fieldwise' n R).
+Proof.
+  induction n; [solve [auto]|].
+  simpl; constructor; repeat intro; intuition eauto.
+Qed.
+
+Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}:
+    Equivalence (fieldwise n R).
+Proof.
+  destruct n; (repeat constructor || apply Equivalence_fieldwise').
+Qed.
+
+Arguments fieldwise' {A B n} _ _ _.
+Arguments fieldwise {A B n} _ _ _.
\ No newline at end of file