From 3040eaa1c13725824fef2f8e7541fbf8540ee216 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:12:46 -0700 Subject: Add a ListUtil lemma --- 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 3006dd799..49535da38 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1097,6 +1097,14 @@ Qed. Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn. +Lemma sum_firstn_succ_cons : forall x xs i, + sum_firstn (x :: xs) (S i) = (x + sum_firstn xs i)%Z. +Proof. + unfold sum_firstn; simpl; reflexivity. +Qed. + +Hint Rewrite @sum_firstn_succ_cons : simpl_sum_firstn. + Lemma sum_firstn_succ_default_rev : forall l i, sum_firstn l i = (sum_firstn l (S i) - nth_default 0 l i)%Z. Proof. -- cgit v1.2.3