From 1de1e5111e6056efdb31a86b054862f9f8e52240 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Aug 2018 15:25:51 -0400 Subject: Add some util lemmas --- src/Util/ListUtil/FoldBool.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util/ListUtil') diff --git a/src/Util/ListUtil/FoldBool.v b/src/Util/ListUtil/FoldBool.v index 6cfe6734a..b69081cab 100644 --- a/src/Util/ListUtil/FoldBool.v +++ b/src/Util/ListUtil/FoldBool.v @@ -43,3 +43,15 @@ Proof. revert ls2; induction ls1, ls2; cbn; try reflexivity. apply f_equal2; eauto. Qed. + +Lemma fold_andb_map_iff A B R ls1 ls2 + : (@fold_andb_map A B R ls1 ls2 = true) + <-> (length ls1 = length ls2 + /\ (forall v, List.In v (List.combine ls1 ls2) -> R (fst v) (snd v) = true)). +Proof. + revert ls2; induction ls1 as [|x xs IHxs], ls2 as [|y ys]; cbn; try solve [ intuition (congruence || auto) ]; []. + rewrite Bool.andb_true_iff, IHxs. + split; intros [H0 H1]; split; auto; + intuition (congruence || (subst; auto)). + apply (H1 (_, _)); auto. +Qed. -- cgit v1.2.3