diff options
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 081ef54b5..e162c2daf 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -107,6 +107,9 @@ Module Export List. End FlatMap. Hint Rewrite @flat_map_cons @flat_map_nil : push_flat_map. + Lemma rev_cons {A} x ls : @rev A (x :: ls) = rev ls ++ [x]. Proof. reflexivity. Qed. + Hint Rewrite @rev_cons : list. + Section FoldRight. Context {A B} (f:B->A->A). Lemma fold_right_nil : forall {A B} (f:B->A->A) a, @@ -115,8 +118,14 @@ Module Export List. Lemma fold_right_cons : forall a b bs, fold_right f a (b::bs) = f b (fold_right f a bs). Proof. reflexivity. Qed. + Lemma fold_right_snoc a x ls: + @fold_right A B f a (ls ++ [x]) = fold_right f (f x a) ls. + Proof. + rewrite <-(rev_involutive ls), <-rev_cons. + rewrite !fold_left_rev_right; reflexivity. + Qed. End FoldRight. - Hint Rewrite @fold_right_nil @fold_right_cons : simpl_fold_right push_fold_right. + Hint Rewrite @fold_right_nil @fold_right_cons @fold_right_snoc : simpl_fold_right push_fold_right. Section Partition. Lemma partition_nil {A} (f:A->_) : partition f nil = (nil, nil). @@ -1869,3 +1878,10 @@ Ltac expand_lists _ := | _ => idtac end; subst v; reflexivity ]. + +Lemma list_rect_to_match A (P:list A -> Type) (Pnil: P nil) (PS: forall a tl, P (a :: tl)) ls : + @list_rect A P Pnil (fun a tl _ => PS a tl) ls = match ls with + | cons a tl => PS a tl + | nil => Pnil + end. +Proof. destruct ls; reflexivity. Qed. |