diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-10 10:05:00 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-10 10:05:00 -0400 |
commit | e9aa3df50d5679fb20993b169bb345ee81ff0e07 (patch) | |
tree | 1ef952b1ea43e1aa68e0fefeb9d5e94a7392332e /src/Util/ListUtil.v | |
parent | 8a834573a5997e7d069f438470d212bc8fa0a05e (diff) |
Add some natutil and listutil lemmas
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 1713d22ab..efaea107d 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2175,3 +2175,33 @@ Proof. all: inversion H0; clear H0; subst. all: f_equal; eauto using or_introl. Qed. + +Lemma push_f_list_rect {P P'} (f : P -> P') {A} Pnil Pcons Pcons' ls + (Hcons : forall x xs rec, f (Pcons x xs rec) + = Pcons' x xs (f rec)) + : f (list_rect (fun _ : list A => P) Pnil Pcons ls) + = list_rect + (fun _ => _) + (f Pnil) + Pcons' + ls. +Proof. + induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ]. + rewrite Hcons, IHxs; reflexivity. +Qed. + +Lemma eq_app_list_rect {A} (ls1 ls2 : list A) + : List.app ls1 ls2 = list_rect _ ls2 (fun x _ rec => x :: rec) ls1. +Proof. revert ls2; induction ls1, ls2; cbn; f_equal; eauto. Qed. +Lemma eq_flat_map_list_rect {A B} f (ls : list A) + : @flat_map A B f ls = list_rect _ nil (fun x _ rec => f x ++ rec) ls. +Proof. induction ls; cbn; eauto. Qed. +Lemma eq_partition_list_rect {A} f (ls : list A) + : @partition A f ls = list_rect _ (nil, nil) (fun x _ '(a, b) => bool_rect (fun _ => _) (x :: a, b) (a, x :: b) (f x)) ls. +Proof. induction ls; cbn; eauto. Qed. +Lemma eq_fold_right_list_rect {A B} f v (ls : list _) + : @fold_right A B f v ls = list_rect _ v (fun x _ rec => f x rec) ls. +Proof. induction ls; cbn; eauto. Qed. +Lemma eq_map_list_rect {A B} f (ls : list _) + : @List.map A B f ls = list_rect _ nil (fun x _ rec => f x :: rec) ls. +Proof. induction ls; cbn; eauto. Qed. |