From b848550e4e6a44280ac8052a9b870dd168fbd417 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 9 Oct 2018 12:28:04 -0400 Subject: Add ListUtil.ForallIn --- src/Util/ListUtil/ForallIn.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/Util/ListUtil/ForallIn.v (limited to 'src/Util') diff --git a/src/Util/ListUtil/ForallIn.v b/src/Util/ListUtil/ForallIn.v new file mode 100644 index 000000000..260a7a4d5 --- /dev/null +++ b/src/Util/ListUtil/ForallIn.v @@ -0,0 +1,34 @@ +Require Import Coq.Lists.List. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.DestructHead. + +Lemma fold_right_impl_Proper {A} {P Q : A -> Prop} ls (concl1 concl2 : Prop) + (Hconcl : concl1 -> concl2) + (HPQ : forall a, In a ls -> Q a -> P a) +: fold_right (fun a (concl : Prop) => P a -> concl) concl1 ls + -> fold_right (fun a (concl : Prop) => Q a -> concl) concl2 ls. +Proof. induction ls as [|x xs IHxs]; cbn [fold_right In] in *; intuition. Qed. + +Lemma forall_In_existT {A P} {Q : forall a : A, P a -> Prop} ls + : fold_right + (fun xp (concl : Prop) + => Q (projT1 xp) (projT2 xp) -> concl) + (forall x p, In (@existT A P x p) ls -> Q x p) + ls. +Proof. + induction ls as [|x xs IHxs]; cbn [fold_right In]; intros; + destruct_head' False; destruct_head'_or. + eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (subst; eauto). +Qed. + +Lemma forall_In_pair_existT {A A' P P'} {Q : forall (a : A) (a' : A'), P a -> P' a' -> Prop} ls + : fold_right + (fun xp_x'p' (concl : Prop) + => Q (projT1 (fst xp_x'p')) (projT1 (snd xp_x'p')) (projT2 (fst xp_x'p')) (projT2 (snd xp_x'p')) -> concl) + (forall x p x' p', In (@existT A P x p, @existT A' P' x' p') ls -> Q x x' p p') + ls. +Proof. + induction ls as [|x xs IHxs]; cbn [fold_right In]; intros; + destruct_head' False; destruct_head'_prod; destruct_head'_or; intros. + eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto). +Qed. -- cgit v1.2.3