From a71c1681dfd5cad1903f22901712c94f7c36ebad Mon Sep 17 00:00:00 2001 From: Nicholas Hubbard Date: Wed, 15 Jan 2025 15:34:34 -0500 Subject: [PATCH] add lemma length_app_comm --- doc/changelog/01-added/75-add-length_app_comm.rst | 5 +++++ theories/Lists/List.v | 8 ++++++++ 2 files changed, 13 insertions(+) create mode 100644 doc/changelog/01-added/75-add-length_app_comm.rst diff --git a/doc/changelog/01-added/75-add-length_app_comm.rst b/doc/changelog/01-added/75-add-length_app_comm.rst new file mode 100644 index 0000000000..7ef87fdb90 --- /dev/null +++ b/doc/changelog/01-added/75-add-length_app_comm.rst @@ -0,0 +1,5 @@ +- in `List.v` + + + lemma `length_app_comm` + (`#75 `_, + by Nicholas Hubbard). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 916d97ba42..813402f2ae 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -239,6 +239,14 @@ Section Facts. intro l; induction l; simpl; auto. Qed. + Lemma length_app_comm : forall l l' : list A, length (l++l') = length (l'++l). + Proof. + intros. + repeat rewrite length_app. + rewrite Nat.add_comm. + reflexivity. + Qed. + Lemma last_length : forall (l : list A) a, length (l ++ [a]) = S (length l). Proof. intros ; rewrite length_app ; simpl.