Commit d6dbed9e authored by Dmitry Khalanskiy's avatar Dmitry Khalanskiy

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`.
parent 446bc644
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment