From 7246cee710e28b9c4475a564ea00c429f5b8961a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 23 May 2016 00:57:45 +0200
Subject: [PATCH] CMRA structure on lists.
Initial commit by Amin Timany.
---
theories/list.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index 5c66a5b..e0f6ede 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -983,6 +983,11 @@ Proof.
- intros [-> Hi]. revert i Hi.
induction n; intros [|?]; naive_solver auto with lia.
Qed.
+Lemma elem_of_replicate n x y : y ∈ replicate n x ↔ y = x ∧ n ≠ 0.
+Proof.
+ rewrite elem_of_list_lookup, Nat.neq_0_lt_0.
+ setoid_rewrite lookup_replicate; naive_solver eauto with lia.
+Qed.
Lemma lookup_replicate_1 n x y i :
replicate n x !! i = Some y → y = x ∧ i < n.
Proof. by rewrite lookup_replicate. Qed.
--
GitLab