The problem is that in this proof we go outside the Iris world (have to establish something in Coq) and come back into Iris unbounded many times times.

Oh. Hm...

My first though is: why?^^ Can't you do all that within Iris, and then only move back out once?

It might help if I can show you the proof of adequacy and we can step through it together, over a zoom call perhaps?

Sure, sounds like I could learn something. :)

However, for this MR I think we should go ahead with the unfolding lemma.

What I meant is, this lemma also does the transition from

`invGpreS`

to`invGS_gen`

. It'd be nice to split that. But I cannot think of a way to do that... the problem is getting hold of the initial`\omega ⊤`

. The entire point of the rest of the fupd API is to hide that from the user.

Exactly my point :-)

That sounds like a least fixpoint would be enough though, which can be done with the existing lemma as the step_fupd lemmas show.

Maybe I am misunderstanding the misunderstanding here but do note that these are not chained fupds which would of course be ok. The problem is that in this proof we go outside the Iris world (have to establish something in Coq) and come back into Iris unbounded many times times. The only reason why we can do this is exactly because each time we come back we know that invariants have been initialized and we have `wsat`

(`\omega`

in this alternative) with the necessary mask. It might help if I can show you the proof of adequacy and we can step through it together, over a zoom call perhaps?

These are my notes from when I ported examples and lambda-rust:

When a proof breaks, you have 3 options:

- Try to find the
`-∗`

that should be turned into a`⊢`

so that things work like before - Adjust the proof to use proof mode tactics rather than Coq tactics (in particular, replace
`apply`

by`iApply`

) - Add some
`apply bi.entails_wand`

/`apply bi.wand_entails`

to 'convert' between the old and new way of interpreting`P -∗ Q`

I would suggest something like this policy:

- If neither
`P`

nor`Q`

contain a`-∗`

, update modality, or WP, then write it as`P ⊢ Q`

. - If this is a monotonicity lemma (where the two sides of the turnstile have very symmetric structure), such as
`(P ⊢ Q) → (|==> P) ⊢ (|==> Q)`

, write it with`⊢`

. - Otherwise write it as
`P -∗ Q`

(or`P ==∗ Q`

or whatever sugar is appropriate).

I am not entirely sure about the update modality part in the first clause. But what do we even have the `P ==∗ Q`

in stdpp_scope for if we recommend people write `P ⊢ |==> Q`

instead? This policy would mean that we would write `own_update`

as `own a ==∗ own b`

, not with a `⊢`

.

FWIW, if we keep this as `own γ a ==∗ own γ a'`

then the `boxes.v`

change becomes unnecessary.

**Ralf Jung**
(e52255ba)
*
at
30 Nov 08:18
*

bump CI to Coq 8.16.1

**Ralf Jung**
(974fa2f7)
*
at
30 Nov 08:17
*

update dependencies

**Ralf Jung**
(db6cb399)
*
at
30 Nov 08:11
*

update dependencies

**Ralf Jung**
(de908f52)
*
at
29 Nov 18:15
*

update dependencies

Could we document in which cases we prefer -∗ and in which cases we prefer ⊢? Is the style guide a good place for that? Or maybe a comment about the -∗ notation in stdpp_scope?

Is there any brief advice we can give to people that need to update their development?

I'm not sure what we do with them in practice, but what I know is that we don't generally assume our BI is affine. It is affine in the goal that exhibited the regression (and `BiAffine PROP`

is required for reproducing), but I think that the `<absorb>`

modality that showed in the goal that exhibited the regression was introduced by applying a lemma that also works for non-affine BIs. It seems to me that the proof mode should still be able to deal with such cases to account for that possibility. What do you think?

Well, we need to initialize both

`£ m`

and`ω ⊤`

which only make sense under`invGS_gen`

. (Yes, I understand that they each rely on one part of it which could be split apart.) More importantly,`□ (∀ E1 E2 P, (ω E1 ∗ |={E1, E2}=> P) → |==> ◇ (ω E2 ∗ P))`

part also requires`invGS_gen`

so it makes more sense to just state the lemma as I have above. If you can come up with a simpler version of the unfolding lemma that splits the use of`invGS_gen`

we can use that instead.

What I meant is, this lemma also does the transition from `invGpreS`

to `invGS_gen`

. It'd be nice to split that. But I cannot think of a way to do that... the problem is getting hold of the initial `\omega ⊤`

. The entire point of the rest of the fupd API is to hide that from the user.

It must, as you say there is a coinductive version which should not be difficult to unravel like I did for the

`no_lc`

version. I did not know that`lc_supply`

was an implementation detail, does it not show up in the adequacy theorem!?

No, it is hidden. We should make it a `Local Definition`

in the later_credits file, probably.

We need to eliminate fupd modalities an

unboundednumber of times in the proof of the adequacy theorem.

That sounds like a least fixpoint would be enough though, which can be done with the existing lemma as the step_fupd lemmas show.

**Ralf Jung**
(c44ce4c9)
*
at
29 Nov 13:25
*

make lc_supply Local

To make sure I understand, the unfolding proposal would be to add a single new lemma

`Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} := ∀ m, ⊢ |==> ∃ `{Hws: !invGS_gen HasNoLc Σ} (ω : coPset → iProp Σ), £ m ∗ ω ⊤ ∗ □ (∀ E1 E2 P, (ω E1 ∗ |={E1, E2}=> P) → |==> ◇ (ω E2 ∗ P)).`

which should not be very hard to prove, and that is sufficient? And moreover we could actually derive

`fupd_soundness_no_lc`

from that? Yeah I think I prefer that over anything involving`fupd_to_bupd`

.^^

Yes, that's right, a single lemma like the above.

Though I think I would prefer a statement like

`(** "Unfolding" soundness stamement for no-LC fupd: This exposes that when initializing the [invGS_gen], we can provide a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update while also carrying around some frame [ω E] that tracks the current mask. We also provide a bunch of later credits for consistency, but there is no way to use them since this is a [HasNoLc] lemma. *) Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} := ∀ m, ⊢ |==> ∃ `{Hws: !invGS_gen HasNoLc Σ} (ω : coPset → iProp Σ), £ m ∗ ω ⊤ ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).`

Sure, that's the same to me :-)

The unfolding version avoids this

`fupd_to_bupd`

business entirely, if I understand correctly? That seems like a win to me. ;)

Yes, that's correct. This lemma is equivalent to the coinductive version which refers to that `fupd_to_bupd`

which would no longer be necessary if we use the unfolding version :-) If that's a win then I'm also happy with that ;-)

However I can't say I quite understand how this is entangled with actually allocating the

`invGS_gen`

, which seems to be important?

Well, we need to initialize both `£ m`

and `ω ⊤`

which only make sense under `invGS_gen`

. (Yes, I understand that they each rely on one part of it which could be split apart.) More importantly, `□ (∀ E1 E2 P, (ω E1 ∗ |={E1, E2}=> P) → |==> ◇ (ω E2 ∗ P))`

part also requires `invGS_gen`

so it makes more sense to just state the lemma as I have above. If you can come up with a simpler version of the unfolding lemma that splits the use of `invGS_gen`

we can use that instead.

Does a similar lemma exist for fupd with later credits? I know you posted one before for the coindiction, but I can't even parse that lemma, and it seems to expose private implementation details such as

`lc_supply`

, so that doesn't seem really satisfying.

It must, as you say there is a coinductive version which should not be difficult to unravel like I did for the `no_lc`

version. I did not know that `lc_supply`

was an implementation detail, does it not show up in the adequacy theorem!?

I also lack good intuition for why the existing

`fupd_soundness_no_lc`

is not strong enough... is the problem that you essentially need to eliminate "coinductively many" nested fupd (whatever that even means)? I guess that makes sense, but I have no idea how to state that nicely.

Yes, that's exactly it. I would say it as follows which might or might not be better wording! We need to eliminate fupd modalities an *unbounded* number of times in the proof of the adequacy theorem.

To make sure I understand, the unfolding proposal would be to add a single new lemma

```
Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} :=
∀ m, ⊢ |==> ∃ `{Hws: !invGS_gen HasNoLc Σ} (ω : coPset → iProp Σ),
£ m ∗ ω ⊤ ∗ □ (∀ E1 E2 P, (ω E1 ∗ |={E1, E2}=> P) → |==> ◇ (ω E2 ∗ P)).
```

which should not be very hard to prove, and that is sufficient? And moreover we could actually derive `fupd_soundness_no_lc`

from that? Yeah I think I prefer that over anything involving `fupd_to_bupd`

.^^ @robbertkrebbers what do you think?

Though I think I would prefer a statement like

```
(** "Unfolding" soundness stamement for no-LC fupd:
This exposes that when initializing the [invGS_gen], we can provide
a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
while also carrying around some frame [ω E] that tracks the current mask.
We also provide a bunch of later credits for consistency, but there is no way to use them
since this is a [HasNoLc] lemma. *)
Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} :=
∀ m, ⊢ |==> ∃ `{Hws: !invGS_gen HasNoLc Σ} (ω : coPset → iProp Σ),
£ m ∗ ω ⊤ ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).
```