Commit a485dd7d authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'jh/lookup_gmap_uncurry_empty' into 'master'

Add lemma lookup_gmap_uncurry_empty

See merge request robbertkrebbers/coq-stdpp!8
parents 8ff30e0f 13c7d213
......@@ -168,6 +168,19 @@ Section curry_uncurry.
- by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
Lemma lookup_gmap_uncurry_None (m : gmap (K1 * K2) A) i :
gmap_uncurry m !! i = None ( j, m !! (i, j) = None).
apply (map_fold_ind (λ mr m, mr !! i = None ( j, m !! (i, j) = None)));
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
- split; [by rewrite lookup_partial_alter|].
intros Hi. specialize (Hi j'). by rewrite lookup_insert in Hi.
- rewrite lookup_partial_alter_ne, IH; [|done]. apply forall_proper.
intros j. rewrite lookup_insert_ne; [done|congruence].
Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
gmap_curry (gmap_uncurry m) = m.
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