diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-24 17:09:57 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 17:09:57 -0400 |
| commit | 589faec943ccd6e55c28fddd701fd38bc0f32507 (patch) | |
| tree | 875a38a61058dce4b84c0b1ff3cb570e331af2d1 /src/Util/ListUtil.v | |
| parent | 5de065df4799cb43aba9195bcd88a5f0479884ff (diff) | |
Added rewrite hints for two ListUtil lemmas
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |