diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-07 15:58:44 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-07 15:58:44 -0700 |
| commit | 2b4f574fe712d5f8af1bcbb8689188d56e19b3c2 (patch) | |
| tree | 55a014a439223052a2a8ca77dda21b0d18337789 /src/Util/ListUtil.v | |
| parent | eb6e7494ed0f6891d0033563a6ba4d7c70585614 (diff) | |
Add update_nth out of bounds
Diffstat (limited to 'src/Util/ListUtil.v')
| -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 432c841f4..483cd4417 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -898,6 +898,14 @@ Proof. omega. Qed. +Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs. +Proof. + induction n; destruct xs; simpl; try congruence; try omega; intros. + rewrite IHn by omega; reflexivity. +Qed. + +Hint Rewrite @update_nth_out_of_bounds using omega : simpl_update_nth. + Lemma update_nth_nth_default : forall {A} (d:A) n f l i, (0 <= i < length l)%nat -> nth_default d (update_nth n f l) i = if (eq_nat_dec i n) then f (nth_default d l i) else nth_default d l i. |