From bb30935906c666f1933f5dfacc8b4fb83885988b Mon Sep 17 00:00:00 2001 From: Marijn van Wezel <marijn.vanwezel@ru.nl> Date: Mon, 27 Jan 2025 17:22:08 +0000 Subject: [PATCH] Add lemmas about `last` and `head`: `last_app_or`, `head_app_or`, and `head_app`. --- CHANGELOG.md | 2 ++ stdpp/list.v | 15 +++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 222e13e8..ca42db36 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,8 @@ API-breaking change is listed. - Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel) - Add lemma `lookup_total_fmap`. +- Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`, + `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel) ## std++ 1.11.0 (2024-10-30) diff --git a/stdpp/list.v b/stdpp/list.v index 1b4c3ecd..64096df6 100644 --- a/stdpp/list.v +++ b/stdpp/list.v @@ -1220,6 +1220,12 @@ Proof. - by rewrite (right_id_L _ (++)). - by rewrite (assoc_L (++)), !last_snoc. Qed. +Lemma last_app_Some l1 l2 x : + last (l1 ++ l2) = Some x ↔ last l2 = Some x ∨ last l2 = None ∧ last l1 = Some x. +Proof. rewrite last_app. destruct (last l2); naive_solver. Qed. +Lemma last_app_None l1 l2 : + last (l1 ++ l2) = None ↔ last l1 = None ∧ last l2 = None. +Proof. rewrite last_app. destruct (last l2); naive_solver. Qed. Lemma last_cons x l : last (x :: l) = match last l with Some y => Some y | None => Some x end. Proof. by apply (last_app [x]). Qed. @@ -1259,6 +1265,15 @@ Proof. by destruct l. Qed. Lemma head_lookup l : head l = l !! 0. Proof. by destruct l. Qed. +Lemma head_app l1 l2 : + head (l1 ++ l2) = match head l1 with Some y => Some y | None => head l2 end. +Proof. by destruct l1. Qed. +Lemma head_app_Some l1 l2 x : + head (l1 ++ l2) = Some x ↔ head l1 = Some x ∨ head l1 = None ∧ head l2 = Some x. +Proof. rewrite head_app. destruct (head l1); naive_solver. Qed. +Lemma head_app_None l1 l2 : + head (l1 ++ l2) = None ↔ head l1 = None ∧ head l2 = None. +Proof. rewrite head_app. destruct (head l1); naive_solver. Qed. Lemma head_reverse l : head (reverse l) = last l. Proof. by rewrite <-last_reverse, reverse_involutive. Qed. Lemma head_Some_elem_of l x : -- GitLab