From a28518301baf9c30f3c8bddb4cc79c65fc5bdd7b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 31 Aug 2023 16:53:21 -0700 Subject: [PATCH] Add some minor results about single-step behavior of nth_error --- .../11-standard-library/17998-nth-error.rst | 5 ++++ theories/Lists/List.v | 28 +++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 doc/changelog/11-standard-library/17998-nth-error.rst diff --git a/doc/changelog/11-standard-library/17998-nth-error.rst b/doc/changelog/11-standard-library/17998-nth-error.rst new file mode 100644 index 000000000000..d640188ecc0f --- /dev/null +++ b/doc/changelog/11-standard-library/17998-nth-error.rst @@ -0,0 +1,5 @@ +- **Added:** + ``unfold_nth_error``, ``nth_error_nil``, ``nth_error_cons``, ``nth_error_O``, + ``nth_error_S`` to ``Coq.Lists.List`` + (`#17998 `_, + by Jason Gross). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 6c50131c4f71..17da9e98aa44 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -615,6 +615,34 @@ Section Elts. intro n. exact (Hnth (S n)). Qed. + Lemma unfold_nth_error l n + : nth_error l n + = match n, l with + | O, x :: _ => Some x + | S n, _ :: l => nth_error l n + | _, _ => None + end. + Proof. destruct n; reflexivity. Qed. + + Lemma nth_error_nil n : nth_error nil n = None. + Proof. destruct n; reflexivity. Qed. + + Lemma nth_error_cons x xs n + : nth_error (x :: xs) n + = match n with + | O => Some x + | S n => nth_error xs n + end. + Proof. apply unfold_nth_error. Qed. + + Lemma nth_error_O l + : nth_error l O = hd_error l. + Proof. destruct l; reflexivity. Qed. + + Lemma nth_error_S l n + : nth_error l (S n) = nth_error (tl l) n. + Proof. destruct l; rewrite ?nth_error_nil; reflexivity. Qed. + (** Results directly relating [nth] and [nth_error] *) Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A),