Commit 11138688 authored by Dmitry Khalanskiy's avatar Dmitry Khalanskiy

Add `list_singletonM_included`

A lemma that allows to relate a singleton with another list.
parent 7363e2cc
......@@ -413,6 +413,20 @@ Section properties.
Lemma list_singleton_snoc l x:
{[length l := x]} l l ++ [x].
Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
Lemma list_singletonM_included i x l:
{[i := x]} l ( x', l !! i = Some x' x x').
Proof.
rewrite list_lookup_included. split.
{ move /(_ i). rewrite list_lookup_singletonM option_included_total.
naive_solver. }
intros (y&Hi&?) j. destruct (Nat.lt_total j i) as [?|[->|?]].
- rewrite list_lookup_singletonM_lt //.
destruct (lookup_lt_is_Some_2 l j) as [z Hz].
{ trans i; eauto using lookup_lt_Some. }
rewrite Hz. by apply Some_included_2, ucmra_unit_least.
- rewrite list_lookup_singletonM Hi. by apply Some_included_2.
- rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
Qed.
(* Update *)
Lemma list_singleton_updateP (P : A Prop) (Q : list A Prop) x :
......
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