From 40d861469b348a58d550fdb331e974faa747e2ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 12:02:57 +0200
Subject: [PATCH] Add lemmas for `head` similar to those for `tail`.

---
 theories/list.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index f6ab979b..a87d5349 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1117,6 +1117,25 @@ Lemma last_reverse l : last (reverse l) = head l.
 Proof. destruct l as [|x l]; simpl; by rewrite ?reverse_cons, ?last_snoc. Qed.
 
 (** ** Properties of the [head] function *)
+Lemma head_nil : head [] =@{option A} None.
+Proof. done. Qed.
+Lemma head_cons x l : head (x :: l) = Some x.
+Proof. done. Qed.
+
+Lemma head_None l : head l = None ↔ l = [].
+Proof. split; [|by intros ->]. by destruct l. Qed.
+Lemma head_is_Some l : is_Some (head l) ↔ l ≠ [].
+Proof. rewrite <-not_eq_None_Some, head_None. naive_solver. Qed.
+
+Lemma head_snoc x l :
+  head (l ++ [x]) = match head l with Some y => Some y | None => Some x end.
+Proof. by destruct l. Qed.
+Lemma head_snoc_snoc x1 x2 l :
+  head (l ++ [x1; x2]) = head (l ++ [x1]).
+Proof. by destruct l. Qed.
+Lemma head_lookup l : head l = l !! 0.
+Proof. by destruct l. Qed.
+
 Lemma head_reverse l : head (reverse l) = last l.
 Proof. by rewrite <-last_reverse, reverse_involutive. Qed.
 
-- 
GitLab