Uncurry memory.

This has 2 advantages:
1- There is no need for a setoid relation over memories, the representaiton is canonical.
2- The lookup function for cells is total (it does no longer return an option)

All in all, the size of the proofs reduces significantly.

theories/thread.v

@@ -259,7 +259,7 @@ Section Thread.
       → c.(gb).(sc) ⊑ 𝓢f
       → let cf := (mkCFG c.(lc) (mkGB 𝓢f c.(gb).(na) Mf))
         in wf cf
-      → ∃ c', tau_pf_step thread_step cf c' ∧ c'.(lc).(prm) ≡ ∅.
+      → ∃ c', tau_pf_step thread_step cf c' ∧ c'.(lc).(prm) = ∅.
 
 End Thread.
 

[Hai Dang]

In gpfsl, I have a CMRA for memories, treating them as maps from loc to cell. Have a look at history.v there, namely histUR, to_hist, and to_hist_insert_alloc.

It seems that I need gmap_uncurry (gmap_curry m) = m, where m: K1 -> K2 -> A for some of the lemmas, but I still haven't got through this lemma, which doesn't seem to hold because it doesn't have leibniz equality.

[Hai Dang]

I've solved this in the merge request robbertkrebbers/coq-stdpp!9.