diff options
| author | Hugo Herbelin | 2019-09-05 08:47:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-05 08:47:12 +0200 |
| commit | 110e87a2bee21c112f7fc4291e5a7b7e5180217b (patch) | |
| tree | ec42c401b0d787cc0b21e882a203b2c12a5f6c08 | |
| parent | 0f5f1b22db69fcb179dbcd656a7cb0e62b24dd6e (diff) | |
| parent | 4297c81eaa43ae43bc4fc31ca19c695539b26b42 (diff) | |
Merge PR #10731: Ocfnash/stdlib additions
Ack-by: Zimmi48
Reviewed-by: herbelin
| -rw-r--r-- | doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst | 8 | ||||
| -rw-r--r-- | theories/Lists/List.v | 24 |
2 files changed, 27 insertions, 5 deletions
diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst index f68b2aaaa2..864c4e6a7e 100644 --- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -1,4 +1,6 @@ -- New lemmas on :g:`combine`, :g:`filter`, and :g:`nodup` functions on lists. The lemma - :g:`filter_app` was moved to the :g:`List` module. +- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the + :g:`List` module. - See `#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash. + See `#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index f45317ba50..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 *) (*****************) @@ -1234,11 +1254,11 @@ End Fold_Right_Recursor. destruct (f x); simpl; now rewrite IH. Qed. - Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool), + Lemma concat_filter_map : forall (l : list (list A)), concat (map filter l) = filter (concat l). Proof. induction l as [| v l IHl]; [auto|]. - simpl. rewrite (IHl f). rewrite filter_app. reflexivity. + simpl. rewrite IHl. rewrite filter_app. reflexivity. Qed. (** [find] *) |