Dorian Lesbre (809926b5) at 11 Dec 21:01
Merge branch 'rm_NPeano' into 'master'
... and 268 more commits
Dorian Lesbre (b3de63c4) at 28 Sep 14:01
It looks good to me, and my downstream code still compiles with this new version.
That was my reasoning as well. Another point in favor of the notation is that, given ∘
is standard for composition, it removes any confusion about the order of arguments. I struggled with that a bit before introducing it.
Done
Dorian Lesbre (0f7f6619) at 18 Apr 18:32
Dorian Lesbre (a99f68e9) at 29 Mar 09:06
Forgot to name stuff
map_compose
operator for finite map compositionm ∘ₘ n
for map_compose m n
This is arguably a niche operator we might not want to include. If you think that is the case feel free to close without merging.
I'm submitting in case someone else would have a use for it, since this
is now fairly complete (although it could use some compatibility lemmas with insert
).
Dorian Lesbre (504d165a) at 29 Mar 08:39
Merge branch 'ralf/list' into 'master'
... and 19 more commits
Dorian Lesbre (d07dd6dd) at 27 Mar 15:07
Map compose singletons
Dorian Lesbre (0b504217) at 27 Mar 08:14
Map assoc
Ok, with this in mind I change the MR a bit:
sepM
variant of the lemmalist_to_map
lemmas and sepM
variantbig_sepL2_fst_snd
using a list of pairs instead of two list (thus removing the length equality hypothesis)Dorian Lesbre (5d3533ab) at 23 Mar 13:32
Utf8 + disjoint hint
Well we already have the dual for that one: iris/algebra/big_op.v#L355
(* FIXME: This lemma could be generalized from [≡] to [=], but that breaks
[setoid_rewrite] in the proof of [big_sepS_sepS]. See Coq issue #14349. *)
Lemma big_opM_map_to_list f m :
([^o map] k↦x ∈ m, f k x) ≡ [^o list] xk ∈ map_to_list m, f (xk.1) (xk.2).
Proof. rewrite big_opM_unseal. apply big_opL_proper'; [|done]. by intros ? [??]. Qed.
Hmm, I guess that could work as well, its essentially the dual lemma where instead of going
[∗ map] k↦v ∈ m, φ k v ⊣⊢ [∗ list] k;v ∈ (map_to_list m).*1;(map_to_list m).*2, φ k v.
we state it as
[∗ map] k↦v ∈ list_to_map (zip lk lv), φ k v ⊣⊢ [∗ list] k;v ∈ lk;lv, φ k v.
I needed it in cerise. We reprensent memory as a map addr -> word
but often represent program as just a list of word
which would later be placed in a section of memory.
The first results in lemmas that look like big_sepM
and the second big_sepL2
, so I needed a way to glue the two together. Specifically I had a few lemmas of the shape
∀ lk lv, [∗ list] k;w ∈ lk;lv, φ k v ={E}=∗ [∗ list] k;w ∈ lk;lv, ψ k v
which I wanted to use on my maps. Thanks to the quantification on list, order really didn't matter.
Simple lemma to convert [∗ map] k↦v ∈ m, φ k v
into [∗ list] k;v ∈ lk;lv, φ k v
.