blob: 260a7a4d508eafb0cde16c6e6cb3888207b0d211 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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.
|
