diff options
author | Jason Gross <jagro@google.com> | 2016-07-18 16:12:46 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-18 16:12:46 -0700 |
commit | 3040eaa1c13725824fef2f8e7541fbf8540ee216 (patch) | |
tree | 9c4ed102a083673b187da6357991198a5da6ea36 | |
parent | 526a60b8dcee4bcec55e50a7b6056b9c9090d73d (diff) |
Add a ListUtil lemma
-rw-r--r-- | src/Util/ListUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |