diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-09 16:35:17 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-09 17:46:49 -0500 |
commit | 2eb4efe2a6f5f5eab23829890ce1aa3182c51762 (patch) | |
tree | 78dd018b6f687c1994577a34d99f40ff0dce3413 /src | |
parent | c45d3843e2a89547ee8949d5239696f6c6a1eb5d (diff) |
Add fieldwise_lift_and
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Tuple.v | 17 |
1 files changed, 17 insertions, 0 deletions
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. |