From 0c687b54156b415684a78ae6d702f5efc41aca87 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Jul 2016 14:49:11 -0700 Subject: Add useful tactics and util lemmas --- src/Util/ListUtil.v | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8260058f1..8823a177e 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -633,11 +633,6 @@ Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs). reflexivity. Qed. -Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. -Proof. - destruct a; omega. -Qed. - Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs). Proof. auto. @@ -976,6 +971,14 @@ Qed. Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn. +Lemma sum_firstn_0 : forall xs, + sum_firstn xs 0 = 0%Z. +Proof. + destruct xs; reflexivity. +Qed. + +Hint Rewrite @sum_firstn_0 : simpl_sum_firstn. + Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> sum_firstn l (S i) = (x + sum_firstn l i)%Z. -- cgit v1.2.3