Commit 7b2056c4 by Ralf Jung

### Merge branch 'ralf/lookup_union_l' into 'master'

```add lookup_union_l

See merge request iris/stdpp!292```
parents ddce76d7 a4dc90a9
 ... @@ -1988,6 +1988,9 @@ Proof. apply lookup_union_with. Qed. ... @@ -1988,6 +1988,9 @@ Proof. apply lookup_union_with. Qed. Lemma lookup_union_r {A} (m1 m2 : M A) i : Lemma lookup_union_r {A} (m1 m2 : M A) i : m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i. m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i. Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _). Qed. Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _). Qed. Lemma lookup_union_l {A} (m1 m2 : M A) i : is_Some (m1 !! i) → (m1 ∪ m2) !! i = m1 !! i. Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed. Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x : Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x : (m1 ∪ m2) !! i = Some x ↔ (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x). m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x). ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!