Adding location equality.

What it says on the tin.

The problem with the lemma as it is is that we do not recover the ownership of the memory locations we used to prove that they were allocated.

BTW, how are you using this in practice? Are you just using this for frozen data structures?

I think the least verbose way to fix this problem is to use two additional (coq-level) hypotheses P -∗ l1 ↦{q1} vl1 and P -∗ l2 ↦{q2} vl2, and drop the (iris-level) hypothesis (∃ q1 vl1 q2 vl2, l1 ↦{q1} vl1 ∧ l2 ↦{q2} vl2)%I. In addition, this would lift the existentials over q1, vl1, q2 and vl2 as universals at the level of the lemma, which is easier to use (no need to call exists).

Not sure whether the current setup does this, but it would be great if the tactic could automatically figure out the proofs of P -∗ l1 ↦{q1} vl1 and P -∗ l2 ↦{q2} vl2 (this is typically just a matter of grabbing the right assumption in the context).

Given that equality on loc is decidable, I think it makes more sense to have two lemmas: One for when they are equal, and one for when they are not. That's probably going to be much easier to use than having to pick a P.

Well, P is rather easy to pick: I think WLOG you can always take your all environment. I.e., instead of iApplying the lemma, you should apply it.

I actually had some trouble proving JH's version of the lemma as stated, but I might be missing something.

(Btw, the P in the current version here in the PR, how is that ever useful?)

What about

Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ q1 vl1 q2 vl2 :
  (l1 = l2 → vl1 = vl2 → l1 ↦{q1+q2} vl1 -∗ ▷ Φ (LitV true)) →
  (l1 ≠ l2 → l1 ↦{q1} vl1 -∗ l2 ↦{q2} vl2 -∗ ▷ Φ (LitV false)) →
  (l1 ↦{q1} vl1 ∧ l2 ↦{q2} vl2)%I -∗
  WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.

(You need to replace the ∧ with a ∗.)

Sure, this would also work, but it is both a bit more complicated to prove and less practical. With the P, if you just apply the lemma, then the subgoals you get are exactly the ones you expect. I.e., you do not have to split the ownership in the case the locations are the same, etc.

Ah right I thought I needed conjunction (which I think would work, but separating conjunction is easier). Actually I don't understand any of this hassle, just assume l1 ↦{q1} vl1 * l2 ↦{q2} vl2 and also produce it and be done?

you do not have to split the ownership in the case the locations are the same, etc.

In case you know the locations are the same, you shouldn't use this lemma. You should use a lemma that doesn't do case distinction.

In case you know the locations are the same, you shouldn't use this lemma. You should use a lemma that doesn't do case distinction.

Oh... I forgot that in our model, you can compare equal locations even if they are not allocated! Then yes, indeed, we would need another lemma in the case locations are the same.

But anyway, I still think the version with P is better, wince this is the method that we are using in these lifting lemmas to make wp_op able to find the right hypotheses.

We have some things with a P and some without. I think I'd find it a little strange for wp_op to open these kinds of goals, but whatever.

Even with P, it could still open just one goal saying l1 ↦{q1} vl1 * l2 ↦{q2} vl2.

We have some things with a P and some without. I think I'd find it a little strange for wp_op to open these kinds of goals, but whatever.

When we have such a lemma without P and when the tactic has to find an hypothesis in the context, then we prove a similar P-lemma in proofmode.v (see e.g., wp_tac_read). The point is that wp_op would not open these goals, but automatically solve them.

The point is that wp_op would not open these goals, but automatically solve them.

Well, if that works (and iFrame seems like a good start), I agree it would be the best option.

Isn't it what we are already doing for wp_write and wp_read for a long time?

Maybe? ;)

added 13 commits

• 5c58585f...8d2e4096 - 11 commits from branch master
• f4cc2bf4 - Merge remote-tracking branch 'origin/master' into eq-loc
• 73722e0e - wp_eq_loc: don't throw away the mapstos

Compare with previous version

I updated wp_eq_loc as you suggested, JH. However, for wp_read and wp_write, we have dedicated tactics that take the names of the mapstos as arguments. Are you suggesting we do the same here, and not make this pat of wp_op?

added 1 commit

• bc70a7be - strengthen qp_eq_loc; add a test

Compare with previous version

added 1 commit

• 89129662 - strengthen qp_eq_loc; add a test

Compare with previous version

I added a test, showing that the wp_op version can be used. This is somewhat unexpected for a wp_op, but at least it works.

@jjourdan are you fine with merging this?

Are you suggesting we do the same here, and not make this pat of wp_op?

I don't think this is really necessary for now, given that even for wp_read and wp_write, I don't think we are using this much (I cannot find an example...).

@jjourdan are you fine with merging this?

Yes, merging.

closed

Eh, we use the wp_read tactic all the time...? We don't give the name, but then it just figures it out automatically -- which wp_op does not; it opens new goals instead.

Eh, we use the wp_read tactic all the time...?

Yeah, but we do not give the names of the hypotheses.

which wp_op does not; it opens new goals instead.

Oh... I though it didsolve the goals automatically. If its just a matter of adding ; wp_done at the end of the ltac definition, it is not really difficult to add it.