From 818788035fb8130dca0aaf6a2ef78678ec437245 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Nov 2017 16:07:03 -0500 Subject: Add fieldwise_eq_iff --- src/Util/Tuple.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index fc216c29f..10f431990 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -567,6 +567,18 @@ Section fieldwise_map. Proof. rewrite fieldwise_map_eq; reflexivity. Qed. End fieldwise_map. +Lemma fieldwise'_eq_iff {A n} x y : fieldwise' (@eq A) x y <-> @eq (tuple' A n) x y. +Proof. + induction n as [|n IHn]; [ reflexivity | ]. + simpl; rewrite IHn; split; [ destruct x, y | ]; simpl; intuition (subst; auto). +Qed. + +Lemma fieldwise_eq_iff {A n} x y : fieldwise (@eq A) x y <-> @eq (tuple A n) x y. +Proof. + destruct n; [ destruct x, y | apply fieldwise'_eq_iff ]; simpl. + tauto. +Qed. + 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). } -- cgit v1.2.3