From d5006369495a4e79c4db011d8fdb334b266381f2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 1 Apr 2017 22:39:58 -0400
Subject: 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.
---
 src/Util/Tuple.v | 36 ++++++++++++------------------------
 1 file changed, 12 insertions(+), 24 deletions(-)

(limited to 'src/Util/Tuple.v')

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.
-- 
cgit v1.2.3