diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index b34a5e322..ddb0d973e 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -81,8 +81,10 @@ Module Export List. Proof using Type. reflexivity. Qed. + Lemma map_repeat x n : map f (List.repeat x n) = List.repeat (f x) n. + Proof. induction n; simpl List.repeat; simpl map; congruence. Qed. End Map. - Hint Rewrite @map_cons @map_nil : push_map. + Hint Rewrite @map_cons @map_nil @map_repeat : push_map. Section FlatMap. Lemma flat_map_nil {A B} (f:A->list B) : List.flat_map f (@nil A) = nil. @@ -1150,6 +1152,15 @@ Lemma map_S_seq {A} (f:nat->A) len : forall start, List.map (fun i => f (S i)) (seq start len) = List.map f (seq (S start) len). Proof. induction len as [|len IHlen]; intros; simpl; rewrite ?IHlen; reflexivity. Qed. +Lemma seq_snoc len : forall start, seq start (S len) = seq start len ++ ((start + len)%nat :: nil). +Proof. + induction len; intros. + { cbv [seq app]. autorewrite with natsimplify; reflexivity. } + { remember (S len); simpl seq. + rewrite (IHlen (S start)); subst; simpl seq. + rewrite Nat.add_succ_r; reflexivity. } +Qed. + Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop), (forall x, In x l -> P x) <-> fold_right and True (map P l). Proof. |