deleted src/Specific/GF25519ExtendedAddCoordinates.v

1 files changed, 0 insertions, 81 deletions

diff --git a/src/Specific/GF25519ExtendedAddCoordinates.v b/src/Specific/GF25519ExtendedAddCoordinates.v
deleted file mode 100644
index 255792cf9..000000000
--- a/src/Specific/GF25519ExtendedAddCoordinates.v
+++ /dev/null
@@ -1,81 +0,0 @@
-Require Import Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
-Require Import Crypto.Algebra.
-Require Import Crypto.Util.Relations.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Tactics.
-
-Require Import Crypto.Specific.GF25519.
-Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
-
-Definition edwards_extended_add_coordinates td P Q :=
-    (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-Definition edwards_extended_carry_add_coordinates td P Q :=
-    (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-
-Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Local Existing Instance field25519.
-Hint Rewrite
-     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode))
-     (Ring.homomorphism_add(H1             :=homomorphism_F25519_decode))
-     (Ring.homomorphism_sub(H1             :=homomorphism_F25519_decode))
-  : edwards_extended_add_coordinates_correct.
-Lemma edwards_extended_add_coordinates_correct td P Q :
-  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-Proof.
-  change (edwards_extended_add_coordinates td P Q)
-  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-  destruct_head' prod.
-  simpl.
-  (*rewrite_strat topdown hints edwards_extended_add_coordinates_correct.*) (* loops on Coq 8.4 *)
-  repeat (rewrite ?(Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode)),
-          ?(Ring.homomorphism_add(H1             :=homomorphism_F25519_decode)),
-          ?(Ring.homomorphism_sub(H1             :=homomorphism_F25519_decode))).
-  reflexivity.
-Qed.
-Local Existing Instance carry_field25519.
-Hint Rewrite
-     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_decode))
-     (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_decode))
-     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_decode))
-  : edwards_extended_add_coordinates_correct.
-Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-Proof.
-  change (edwards_extended_carry_add_coordinates td P Q)
-  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-  destruct_head' prod.
-  simpl.
-  (*rewrite_strat topdown hints edwards_extended_add_coordinates_correct.*) (* loops on Coq 8.4 *)
-  (* This is an annoying replacement for rewrite_strat loopiness *)
-  generalize (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_decode)).
-  generalize (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_decode)).
-  generalize (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_decode)).
-  generalize mul; generalize carry_sub; generalize carry_add.
-  intros carry_add' carry_sub' mul'.
-  intros H0 H1 H2.
-  repeat rewrite ?H2, ?H1, ?H0.
-  reflexivity.
-Qed.
-
-Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
-  Tuple.fieldwise
-    (n:=4) eq
-    (edwards_extended_carry_add_coordinates td P Q)
-    (edwards_extended_add_coordinates td P Q).
-Proof.
-  pose proof (edwards_extended_carry_add_coordinates_correct td P Q) as H0.
-  pose proof (edwards_extended_add_coordinates_correct td P Q) as H1.
-  rewrite <- H0 in H1; clear H0.
-  assert (Tuple.fieldwise
-            (fun x y => x = y)
-            (Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q))
-            (Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)))
-    by (rewrite H1; reflexivity).
-  clear H1.
-  destruct (edwards_extended_carry_add_coordinates td P Q), (edwards_extended_add_coordinates td P Q).
-  destruct_head' prod; simpl; unfold eq; trivial.
-Qed.