Commit 9765b5fe authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/map_subseteq_inv' into 'master'

Add lemma `map_subseteq_inv`.

See merge request iris/stdpp!335
parents 564dc692 6df1a647
......@@ -2646,6 +2646,15 @@ Proof.
by rewrite lookup_difference_Some, map_filter_lookup_Some.
Qed.
(** ** Misc properties about the order *)
Lemma map_subseteq_inv {A} (m1 m2 : M A) : m1 m2 m1 m2 m1 = m2.
Proof.
intros. destruct (decide (m2 m1 = )) as [Hm21|(i&x&Hi)%map_choose].
- right. by rewrite <-(map_difference_union m1 m2), Hm21, (right_id_L _ _).
- left. apply lookup_difference_Some in Hi as [??].
apply map_subset_alt; eauto.
Qed.
(** ** Setoids *)
Section setoid.
Context `{Equiv A}.
......
Supports Markdown
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