5 files changed, 83 insertions, 45 deletions
diff --git a/_CoqProject b/_CoqProject
index 21aca1390..1fefae2d4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,11 +39,11 @@ src/Specific/GF1305.v
 src/Specific/GF25519.v
 src/Tactics/VerdiTactics.v
 src/Util/CaseUtil.v
-src/Util/Fieldwise.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
 src/Util/NumTheoryUtil.v
 src/Util/Tactics.v
+src/Util/Tuple.v
 src/Util/WordUtil.v
 src/Util/ZUtil.v
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index e6ec7ab86..f9a866acb 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -6,7 +6,7 @@ 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.
+Require Import Crypto.Util.Tuple.
 
 Module E.
   Import Group Ring Field CompleteEdwardsCurve.E.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 4a352c738..fe0e732a8 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -6,7 +6,7 @@ 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.
+Require Import Crypto.Util.Tuple.
 
 Module Extended.
   Section ExtendedCoordinates.
diff --git a/src/Util/Fieldwise.v b/src/Util/Fieldwise.v
deleted file mode 100644
index f2f0b5acb..000000000
--- a/src/Util/Fieldwise.v
+++ /dev/null
@@ -1,42 +0,0 @@
-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
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
new file mode 100644
index 000000000..de1af2a95
--- /dev/null
+++ b/src/Util/Tuple.v
@@ -0,0 +1,80 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+
+Fixpoint tuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (tuple' T n' * T)%type
+  end.
+
+Definition tuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => tuple' T n'
+  end.
+
+Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
+  match n with
+  | 0 => fun x => (x::nil)%list
+  | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
+  end.
+
+Definition to_list {T} (n:nat) : tuple T n -> list T :=
+  match n with
+  | 0 => fun _ => nil
+  | S n' => fun xs : tuple T (S n') => to_list' n' xs
+  end.
+
+Fixpoint from_list' {T} (x:T) (xs:list T) : tuple' T (length xs) :=
+  match xs with
+  | nil => x
+  | (y :: xs')%list => (from_list' y xs', x)
+  end.
+
+Definition from_list {T} (xs:list T) : tuple T (length xs) :=
+  match xs as l return (tuple T (length l)) with
+  | nil => tt
+  | (t :: xs')%list => from_list' t xs'
+  end.
+
+Lemma to_list_from_list : forall {T} (xs:list T), to_list (length xs) (from_list xs) = xs.
+Proof.
+  destruct xs; auto; simpl.
+  generalize dependent t.
+  induction xs; auto; simpl; intros; f_equal; auto.
+Qed.
+
+Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n.
+Proof.
+  destruct n; auto; intros; simpl in *.
+  induction n; auto; intros; simpl in *.
+  destruct xs; simpl in *; eauto.
+Qed.
+
+Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {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 A n) (b:tuple B n) : 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