From ad47c9438762b80b177c6e71c7c19e013636f18a Mon Sep 17 00:00:00 2001 From: Kimaya Bedarkar <kbedarka@mpi-sws.org> Date: Wed, 19 Feb 2025 15:16:08 +0100 Subject: [PATCH 1/2] add app nil lemmas --- CHANGELOG.md | 1 + stdpp/list.v | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 32d2f14c..c5932530 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ API-breaking change is listed. `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler) - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`: `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar) +- Add `app_nil_r_rev` and `app_nil_l_rev` lemmas. (by Kimaya Bedarkar) The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). diff --git a/stdpp/list.v b/stdpp/list.v index 4a96bd88..e91baab9 100644 --- a/stdpp/list.v +++ b/stdpp/list.v @@ -501,6 +501,10 @@ Proof. intro. apply app_nil_r. Qed. Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = []. Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed. +Lemma app_nil_l_rev l1 l2 : l1 ++ l2 = [] → l1 = []. +Proof. by rewrite app_nil; intros [-> _]. Qed. +Lemma app_nil_r_rev l1 l2 : l1 ++ l2 = [] → l2 = []. +Proof. by rewrite app_nil; intros [_ ->]. Qed. Lemma app_singleton l1 l2 x : l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = []. Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed. -- GitLab From ea16e18f5a6a757b64b105e90e6f344ca2959b3b Mon Sep 17 00:00:00 2001 From: Kimaya Bedarkar <kbedarka@mpi-sws.org> Date: Wed, 19 Feb 2025 16:00:53 +0100 Subject: [PATCH 2/2] change naming --- CHANGELOG.md | 2 +- stdpp/list.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c5932530..cde49afa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,7 +13,7 @@ API-breaking change is listed. `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler) - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`: `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar) -- Add `app_nil_r_rev` and `app_nil_l_rev` lemmas. (by Kimaya Bedarkar) +- Add `app_nil_r_inv` and `app_nil_l_inv` lemmas. (by Kimaya Bedarkar) The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). diff --git a/stdpp/list.v b/stdpp/list.v index e91baab9..9f9d0dad 100644 --- a/stdpp/list.v +++ b/stdpp/list.v @@ -501,9 +501,9 @@ Proof. intro. apply app_nil_r. Qed. Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = []. Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed. -Lemma app_nil_l_rev l1 l2 : l1 ++ l2 = [] → l1 = []. +Lemma app_nil_l_inv l1 l2 : l1 ++ l2 = [] → l1 = []. Proof. by rewrite app_nil; intros [-> _]. Qed. -Lemma app_nil_r_rev l1 l2 : l1 ++ l2 = [] → l2 = []. +Lemma app_nil_r_inv l1 l2 : l1 ++ l2 = [] → l2 = []. Proof. by rewrite app_nil; intros [_ ->]. Qed. Lemma app_singleton l1 l2 x : l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = []. -- GitLab