From 2eb4efe2a6f5f5eab23829890ce1aa3182c51762 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 9 Nov 2017 16:35:17 -0500
Subject: Add fieldwise_lift_and

---
 src/Util/Tuple.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

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

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 72feea5ea..8742b3a2b 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1043,6 +1043,23 @@ Proof.
   { repeat (intros [] || intro); auto. }
 Qed.
 
+Lemma fieldwise'_lift_and {n A B R1 R2} x y
+  : (@fieldwise' A B n R1 x y /\ @fieldwise' A B n R2 x y)
+    <-> (@fieldwise' A B n (fun a b => R1 a b /\ R2 a b) x y).
+Proof.
+  induction n as [|n IHn]; intros.
+  { compute; intros; subst; auto. }
+  { simpl; rewrite <- IHn; tauto. }
+Qed.
+
+Lemma fieldwise_lift_and {n A B R1 R2} x y
+  : (@fieldwise A B n R1 x y /\ @fieldwise A B n R2 x y)
+    <-> (@fieldwise A B n (fun a b => R1 a b /\ R2 a b) x y).
+Proof.
+  destruct n; [ compute; tauto | apply fieldwise'_lift_and ].
+Qed.
+
+
 Global Instance fieldwise'_Proper
   : forall {n A B}, Proper (pointwise_relation _ (pointwise_relation _ impl) ==> eq ==> eq ==> impl) (@fieldwise' A B n) | 10.
 Proof.
-- 
cgit v1.2.3