From 589faec943ccd6e55c28fddd701fd38bc0f32507 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 24 Aug 2016 17:09:57 -0400 Subject: Added rewrite hints for two ListUtil lemmas --- src/Util/ListUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 1c39f22cb..2fd9befa0 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1340,6 +1340,7 @@ Proof. induction n; destruct l; boring. apply nth_error_nil_error. Qed. +Hint Rewrite @nth_error_skipn : push_nth_error. Lemma nth_default_skipn : forall {A} (l : list A) d n m, nth_default d (skipn n l) m = nth_default d l (n + m). Proof. @@ -1347,6 +1348,7 @@ cbv [nth_default]; intros. rewrite nth_error_skipn. reflexivity. Qed. +Hint Rewrite @nth_default_skipn : push_nth_default. Lemma sum_firstn_skipn : forall l n m, sum_firstn l (n + m) = (sum_firstn l n + sum_firstn (skipn n l) m)%Z. Proof. -- cgit v1.2.3