diff options
| -rw-r--r-- | theories/Lists/List.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 88c47b9744..38723e291f 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -536,6 +536,26 @@ Section Elts. simpl in *. apply IHn. auto with arith. Qed. + (** Results directly relating [nth] and [nth_error] *) + + Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A), + nth_error l n = Some x -> nth n l d = x. + Proof. + intros l n x d H. + apply nth_error_split in H. destruct H as [l1 [l2 [H H']]]. + subst. rewrite app_nth2; [|auto]. + rewrite Nat.sub_diag. reflexivity. + Qed. + + Lemma nth_error_nth' : forall (l : list A) (n : nat) (d : A), + n < length l -> nth_error l n = Some (nth n l d). + Proof. + intros l n d H. + apply nth_split with (d:=d) in H. destruct H as [l1 [l2 [H H']]]. + subst. rewrite H. rewrite nth_error_app2; [|auto]. + rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. + Qed. + (*****************) (** ** Remove *) (*****************) |