From ac80a94132cab53c40638bbea6843c0d84c15645 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jun 2018 10:37:00 -0400 Subject: Add seq_add, seq_len_0 --- src/Util/ListUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8cfb626d2..abb1395b3 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1201,6 +1201,14 @@ Proof. rewrite Nat.add_succ_r; reflexivity. } Qed. +Lemma seq_len_0 a : seq a 0 = nil. Proof. reflexivity. Qed. +Lemma seq_add start a b : seq start (a + b) = seq start a ++ seq (start + a) b. +Proof. + revert start b; induction a as [|a IHa]; cbn; intros start b. + { f_equal; omega. } + { rewrite IHa; do 3 f_equal; omega. } +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