diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 16:33:14 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 16:33:21 -0700 |
| commit | 6bcf94ac9f14950f140e00df78fd5cfd4bedb5bb (patch) | |
| tree | 8b6f5338d23d7af9082c65a42cccbbc6a5c6e744 | |
| parent | 3040eaa1c13725824fef2f8e7541fbf8540ee216 (diff) | |
Add a lemma about sum_firstn
| -rw-r--r-- | src/Util/ListUtil.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 49535da38..8b92ef4fa 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -23,6 +23,7 @@ Create HintDb pull_firstn discriminated. Create HintDb push_firstn discriminated. Create HintDb pull_update_nth discriminated. Create HintDb push_update_nth discriminated. +Create HintDb znonzero discriminated. Hint Rewrite @app_length @@ -1105,6 +1106,12 @@ Qed. Hint Rewrite @sum_firstn_succ_cons : simpl_sum_firstn. +Lemma sum_firstn_nil : forall i, + sum_firstn nil i = 0%Z. +Proof. destruct i; reflexivity. Qed. + +Hint Rewrite @sum_firstn_nil : 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. @@ -1118,6 +1125,17 @@ Proof. intros; erewrite sum_firstn_succ by eassumption; omega. Qed. +Lemma sum_firstn_nonnegative : forall n l, (forall x, In x l -> 0 <= x)%Z + -> (0 <= sum_firstn l n)%Z. +Proof. + induction n as [|n IHn]; destruct l as [|? l]; autorewrite with simpl_sum_firstn; simpl; try omega. + { specialize (IHn l). + destruct n; simpl; autorewrite with simpl_sum_firstn simpl_nth_default in *; + intuition. } +Qed. + +Hint Resolve sum_firstn_nonnegative : znonzero. + Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, nth_default d (map2 f ls1 ls2) i = if lt_dec i (min (length ls1) (length ls2)) |