From 2b4f574fe712d5f8af1bcbb8689188d56e19b3c2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Thu, 7 Jul 2016 15:58:44 -0700
Subject: Add update_nth out of bounds

---
 src/Util/ListUtil.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Util/ListUtil.v')

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.
-- 
cgit v1.2.3