Coalesce Tuple.pointwise2 and Tuple.fieldwise

We don't need both of them.  We keep the definition of pointwise2
because it's needed for reification to work, and we keep the name of
fieldwise because it's used in more places.  This closes #137.

1 files changed, 12 insertions, 24 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 2b049d86e..7682c2d24 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -255,18 +255,6 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
   := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
 
-Fixpoint pointwise2' {n A B} (R:A -> B -> Prop) : tuple' A n -> tuple' B n -> Prop
-  := match n with
-     | 0 => R
-     | S n' => fun (x y : tuple' _ _ * _)
-               => @pointwise2' n' A B R (fst x) (fst y) /\ R (snd x) (snd y)
-     end.
-Definition pointwise2 {n A B} (R:A -> B -> Prop) : tuple A n -> tuple B n -> Prop
-  := match n with
-     | 0 => fun _ _ => True
-     | S n' => pointwise2' R
-     end.
-
 Lemma to_list'_ext {n A} (xs ys:tuple' A n) : to_list' n xs = to_list' n ys -> xs = ys.
 Proof.
   induction n; simpl in *; [cbv; congruence|]; destruct_head' prod.
@@ -472,17 +460,17 @@ Proof.
                | intro ].
 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.
+Fixpoint fieldwise' {A B} (n:nat) (R:A -> B -> Prop) : tuple' A n -> tuple' B n -> Prop
+  := match n with
+     | 0 => R
+     | S n' => fun (x y : tuple' _ _ * _)
+               => @fieldwise' A B n' R (fst x) (fst y) /\ R (snd x) (snd y)
+     end.
+Definition fieldwise {A B} (n:nat) (R:A -> B -> Prop) : tuple A n -> tuple B n -> Prop
+  := match n with
+     | 0 => fun _ _ => True
+     | S n' => fieldwise' n' R
+     end.
 
 Local Ltac Equivalence_fieldwise'_t :=
   let n := match goal with |- ?R (fieldwise' ?n _) => n end in
@@ -566,7 +554,7 @@ End fieldwise_map.
 Fixpoint fieldwiseb' {A B} (n:nat) (R:A->B->bool) (a:tuple' A n) (b:tuple' B n) {struct n} : bool.
   destruct n; simpl @tuple' in *.
   { exact (R a b). }
-  { exact (R (snd a) (snd b) && fieldwiseb' _ _ n R (fst a) (fst b))%bool. }
+  { exact (fieldwiseb' _ _ n R (fst a) (fst b) && R (snd a) (snd b))%bool. }
 Defined.
 
 Definition fieldwiseb {A B} (n:nat) (R:A->B->bool) (a:tuple A n) (b:tuple B n) : bool.