From d6dbed9e7530d03f632773dbef849dddac39214f Mon Sep 17 00:00:00 2001
From: Dmitry Khalanskiy <Dmitry.Khalanskiy@jetbrains.com>
Date: Tue, 21 Jan 2020 12:56:23 +0300
Subject: [PATCH] Add a stronger version of `list_core_id`.

A new lemma, `list_core_id'`, allows to infer that a list is
`CoreId` by only checking that all its elements are `CoreId`, as
opposed to the existing instance, `list_core_id`, that only works
when the list contains elements of the type where every element is
`CoreId`.
---
 theories/algebra/list.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 669500516..b40a301c5 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -296,12 +296,17 @@ Section cmra.
     by apply cmra_discrete_valid.
   Qed.
 
-  Global Instance list_core_id l : (∀ x : A, CoreId x) → CoreId l.
+  Lemma list_core_id' l : (∀ x, x ∈ l → CoreId x) → CoreId l.
   Proof.
-    intros ?; constructor; apply list_equiv_lookup=> i.
-    by rewrite list_lookup_core (core_id_core (l !! i)).
+    intros Hyp. constructor. apply list_equiv_lookup=> i.
+    rewrite list_lookup_core.
+    destruct (l !! i) eqn:E; last done.
+    by eapply Hyp, elem_of_list_lookup_2.
   Qed.
 
+  Global Instance list_core_id l : (∀ x : A, CoreId x) → CoreId l.
+  Proof. intros Hyp; by apply list_core_id'. Qed.
+
   (** Internalized properties *)
   Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
   Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-- 
GitLab