big_sepM2 and associated lemmas

Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.

Would like to hear your comments and also add some helpful lemmas about this big op.

added 2 commits

• a1d6944f - Simpler proof of `big_sepM2_lookup_acc`.
• 3d56865d - Add big_sepM2_lookup_{1,2}

Compare with previous version

unmarked as a Work In Progress

changed the description

I've used this operation in reloc and it seems to work out fine so far.

Thanks for this MR! This is very useful.

Could you also add the relevant instances/hints in the proofmode folder? You should check which instances we have for the normal separating big op, and which also apply to the binary version. Probably a variant of into_laterN_big_sepM and the Hint Extern 0 (envs_entails _ (big_opM _ _ _)) thing.

I see you introduced two TODOs in reloc@f66e377a. Does that mean something is still missing in this MR?

Impressive, it looks like you managed to get variants for all the lemmas for the unary variant. Looks like this was a lot of work without the proof mode ;).

Hi Robbert. Thanks for reviewing my MR.

I see you introduced two TODOs in reloc@f66e377a. Does that mean something is still missing in this MR?

One TODO is for an instance Proper (dist n ==> (=) ==> (=) ==> dist n) big_sepM2, but it only makes sense if the maps are OFEs. Not sure if it warrants inclusion here.

The other TODO is a fucky wucky and I am not sure what exactly is broken. Can you perhaps take a look at some point? Basically, when I apply big_sepM2_insert_2 it gives some weird goals.

added 1 commit

• 8d92dce3 - address some comments by @robbertkrebbers

Compare with previous version

One TODO is for an instance Proper (dist n ==> (=) ==> (=) ==> dist n) big_sepM2, but it only makes sense if the maps are OFEs. Not sure if it warrants inclusion here.

Oh, I see, that applies to the unary big op too. There we probably want to have that result in algebra/big_op even.

Now that we are working on this, I guess it makes sense to add such an instance for both the unary and binary version to this MR. And we probably also want to have it for the version on lists. For sets and multisets I don't think it makes sense, though.

The other TODO is a fucky wucky and I am not sure what exactly is broken. Can you perhaps take a look at some point? Basically, when I apply big_sepM2_insert_2 it gives some weird goals.

Will do later.

resolved all discussions

added 2 commits

• 7b9f1cb2 - Add sbi lemmas for big_sepM2.
• a5753b1b - Proofmode stuff for big_sepM2.

Compare with previous version

Could you also add the relevant instances/hints in the proofmode folder? You should check which instances we have for the normal separating big op, and which also apply to the binary version. Probably a variant of into_laterN_big_sepM and the Hint Extern 0 (envs_entails _ (big_opM _ _ _)) thing.

I've updated those two. I did a grep for big_sepM and big_opM in the proofmode folder but didn't find anything else that I had to change.