diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2015-11-19 17:48:37 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2015-11-19 17:48:37 -0500 |
| commit | 545e521740d69724430909e8a1b9059b957ed13d (patch) | |
| tree | 874ebc35a1a986a40f449442755eec76f2f92a46 /src/Util/ListUtil.v | |
| parent | 4014d0b0fcdcdee4f3528c544f3f7475a3ec4a01 (diff) | |
Added base_succ precondition to BaseSystem to help prove carrying.
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 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. |