From 545e521740d69724430909e8a1b9059b957ed13d Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 19 Nov 2015 17:48:37 -0500 Subject: Added base_succ precondition to BaseSystem to help prove carrying. --- 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 7f5bea670..ba1d8326a 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -223,6 +223,14 @@ Proof. induction n; destruct xs; nth_tac. Qed. +Lemma In_nth_error_value : forall {T} xs (x:T), + In x xs -> exists n, nth_error xs n = Some x. +Proof. + induction xs; nth_tac; break_or_hyp. + - exists 0; reflexivity. + - edestruct IHxs; eauto. exists (S x0). eauto. +Qed. + Lemma nth_value_index : forall {T} i xs (x:T), nth_error xs i = Some x -> In i (seq 0 (length xs)). Proof. -- cgit v1.2.3