From d6148a30cc81688c6bd494c0f4d0874bbe684e55 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 11:40:15 +0200
Subject: [PATCH] Add lemmas `nil_equiv_eq`, `cons_equiv_eq`,
 `list_singleton_equiv_eq`, `app_equiv_eq`.

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

diff --git a/theories/list.v b/theories/list.v
index ef88844b..1698d68b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3456,6 +3456,19 @@ Section setoid.
   Proof.
     induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
   Qed.
+
+  Lemma nil_equiv_eq mx : mx ≡ [] ↔ mx = [].
+  Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
+  Lemma cons_equiv_eq l x k : l ≡ x :: k ↔ ∃ x' k', l = x' :: k' ∧ x' ≡ x ∧ k' ≡ k.
+  Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
+  Lemma list_singleton_equiv_eq l x : l ≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡ x.
+  Proof. rewrite cons_equiv_eq. setoid_rewrite nil_equiv_eq. naive_solver. Qed.
+  Lemma app_equiv_eq l k1 k2 :
+    l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
+  Proof.
+    split; [|intros (?&?&->&?&?); by f_equiv].
+    setoid_rewrite equiv_Forall2. rewrite Forall2_app_inv_r. naive_solver.
+  Qed.
 End setoid.
 
 (** * Properties of the [find] function *)
-- 
GitLab