tuple tooling

1 files changed, 80 insertions, 0 deletions

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