From 6bcf94ac9f14950f140e00df78fd5cfd4bedb5bb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:33:14 -0700 Subject: Add a lemma about sum_firstn --- src/Util/ListUtil.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) 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)) -- cgit v1.2.3