Fix compilation with Coq 8.10

This fix looks good to me. Relying on evars, in the way as originally done here, is very fragile and should be avoided. Thanks.

merged

mentioned in commit c3731793

Ah, I just had a fix done here literally seconds ago. :/ Bad timing.^^ But thanks for helping, Tej. :)

Relying on evars, in the way as originally done here, is very fragile and should be avoided. Thanks.

I think there's a bug here if we have to repeat the initial value of the ghost variable. That's just not a nice proof.

The problem is that the first subgoal is the validity, where one has to establish ✓ ?evar. So, at that point, it will just fail. Then in a latter goal, it will resolve the evar. Apparently, in more recent versions of Coq, it will backtrack to the first goal.

IMHO, evars should only used if they can be solved in subgoal order. Here they cannot, unless you're going through shenanigans of manually solving subgoals in different order (which AFAIK your initial proof was doing).

If you want to have a truly short proof that doesn't mention there value, here you go:

  Lemma ghost_var_alloc_strong a (P : gname → Prop) :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∧ ghost_var γ 1 a.
  Proof. intros. by iApply own_alloc_strong. Qed.

You need to use ∧ instead of ∗, since own_alloc_strong also uses ∧. Being consistent in that regard is probably better anyway. It may be considered a feature that the apply actually enforces consistency.

IMHO, evars should only used if they can be solved in subgoal order. Here they cannot, unless you're going through shenanigans of manually solving subgoals in different order (which AFAIK your initial proof was doing).

Looks like we value different things in a proof. I don't care much for how long it is, but I care about information content, so I find a slightly longer script that avoids repeating something better. Note that my proof wasn't fragile, it controlled the order of goal resolution precisely to handle the fact that ✓ ?evar can only be resolved after the main goal is done. There are no "shenanigans" about that, just straight-forward Coq proving. It is your by eauto that made it fragile, as witnessed by the fact that this failed on Coq 8.10.

You need to use ∧ instead of ∗, since own_alloc_strong also uses ∧. Being consistent in that regard is probably better anyway. It may be considered a feature that the apply actually enforces consistency.

That is a neat proof -- though if we want to be consistent, both should be *. We usually only ever use /\ when we truly want overlapping resources.

I do care about being able to maintain proofs. Have you ever tried debugging Coq proofs where the way evars are resolved depends on the goal order? It's really confusing. I expect that goals can be solved in goal order.

I do care about being able to maintain proofs.

So do I.

Have you ever tried debugging Coq proofs where the way evars are resolved depends on the goal order?

Yeah I do that all the time... it's not confusing at all IMO, given that the last first etc already show in which order the goals should be resolved. Debugging my proof is as simple as stepping to after the last first in the Coq script, and seeing what things look like, and then stepping forward.

I find such a proof much easier to debug and maintain than some of your proofs that do 5 reasoning steps in a single rewrite or in one large chain of nested ; and [...]. Those I find truly impossible to fix when they break, I have to take them entirely apart and do each step in a separate tactic and they end up twice as long.

I expect that goals can be solved in goal order.

Yes and they can! After last first, the goals are in the order needed to resolve the evars.

Or maybe you mean "solved in the lemma statement order". Basically, you seem to say "never use last first". I don't entirely understand why, but I now recall you saying this before. Given that I never ran into confusion with last first but keep running into confusion with your extremely condensed proofs, I do not entirely understand where your preference is coming from.

That is a neat proof -- though if we want to be consistent, both should be *. We usually only ever use /\ when we truly want overlapping resources.

Then we need to change that stuff in own. Most code in there predates the proof mode, hence it uses ∧. If you want to update that, go for it.

!508 (merged)

mentioned in merge request !488 (merged)

Fix compilation with Coq 8.10

Merge request reports

Activity