From b54acb5b7012a8e4540e29c68d6f10f32b88009f Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 16 Feb 2018 18:14:45 +0100 Subject: add two proofs about lists --- src/Util/ListUtil.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'src/Util/ListUtil.v') 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. -- cgit v1.2.3