From 4f64644c8ae6ee539526575d8634e512058c4813 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Nov 2017 10:07:25 -0500 Subject: Add fieldwise_map_from_list_iff --- src/Util/Tuple.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index d762e73b9..fc216c29f 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -682,6 +682,20 @@ Proof. apply IHn; auto. Qed. +Lemma fieldwise_map_from_list_iff + {T0 T T'} R ls {n} pf1 pf2 (f : T0 -> T) (g : T0 -> T') + : ((fieldwise R (map f (from_list n ls pf1)) + (map g (from_list n ls pf2))) + <-> List.Forall (fun x => R (f x) (g x)) ls). +Proof. + split; intro H; revert H; revert dependent n; + (induction ls as [|x xs IHxs]; intro n; [ | specialize (IHxs (pred n)) ]); + destruct n as [|[|n]]; try destruct xs; simpl in *; auto; + try congruence; intros; destruct_head'_and; eauto. + { inversion H; auto. } + { inversion H; auto. } +Qed. + Fixpoint eta_tuple'_dep {T n} : forall (P : tuple' T n -> Type), (forall ts : tuple' T n, P ts) -> forall ts : tuple' T n, P ts := match n with -- cgit v1.2.3