docs: add debugging tips for vcg goals

[lsf37]

Inspired by discussions on the fastpath PR and MM discussions, a minor addition to the CRefine notes in docs/ on how to debug that False-in-final-goal-after-vcg problem.

[lsf37]

This is not trying to be comprehensive, but just an improvement to the "sorry, no clue" that was there before.

[corlewis]

This looks good to me and is definitely an improvement over 'no clue'!

[michaelmcinerney]

Very helpful, thanks

[Xaphiosis]

When looking at this PR, I kept having a sneaking suspicion I had written about something related already and asked people for feedback, although I couldn't find the direct text I remembered. Turns out I did write something related and linked it on mattermost pinging the whole channel (Michael even looked at it):
https://gist.github.com/Xaphiosis/2fa2b51b65e05c3addda1576f90a31ed

This PR came out of nowhere, so what I wrote was probably not considered.

I think that a section like "Having to show unprovable subterms due to implicit False" would be useful (which was the target of my gist), and some of my examples of specific cases are more clear than they are here (the x stuff above without explicit EX). The explanation of schematic mismatches, I'm not sure whether it's any clearer, might depend on reader. By doing this as a two-step process in the guide:

  apply (rule conseqPre, vcg)
  apply (rule subset_refl)

might be more useful than the one-step version, because you can look at the failing case and see what variables the schematic depends on vs the generated goal. Etc.

Something to consider w.r.t. a "proving False" vs a "unprovable subterms" section, is that I rarely get to see a proper False. Especially in larger goals, the "why do I need to prove this thing I can't actually prove" case situation is the one I see nearly all the time. Can anyone corroborate the frequency of seeing a real False?

[lsf37]

When looking at this PR, I kept having a sneaking suspicion I had written about something related already and asked people for feedback, although I couldn't find the direct text I remembered. Turns out I did write something related and linked it on mattermost pinging the whole channel (Michael even looked at it): https://gist.github.com/Xaphiosis/2fa2b51b65e05c3addda1576f90a31ed

This PR came out of nowhere, so what I wrote was probably not considered.

Indeed, I had forgotten about this, I was just triggered by the "sorry, not better clue" that came up in a grep for a completely different task. Your overall description of the problem is much better, so we should definitely use most of that. Maybe bits of mine are still useful to add -- if not, also Ok to just throw it out, it's not like a huge amount of consideration went into mine, I just tried to put together something short that was better than "no clue".

How about making your gist a separate file under docs/, adding some bits of this PR as appropriate if there is something useful, and then replace the description in here with a link to the separate file?

[lsf37]

Something to consider w.r.t. a "proving False" vs a "unprovable subterms" section, is that I rarely get to see a proper False. Especially in larger goals, the "why do I need to prove this thing I can't actually prove" case situation is the one I see nearly all the time. Can anyone corroborate the frequency of seeing a real False?

I've seen it a few times, mostly in other people's proofs (not the entire post condition being False, but a term under a case or some quantifier), but the one you describe is much more common.

[Xaphiosis]

Suggestion of making a separate file, putting the combined crefine/ccorres proof debugging info in there, then linking to it from crefine-notes.md makes sense. Let's do that. There should be a way of combining my gist with what @lsf37 wrote up, possibly favouring whichever is the most specific/comprehensible to the content they apply to.

[lsf37]

Now updated with Raf's gist as a basis and extracted from the CRefine notes as a separate file. I also added all our recent new files to the README, which is attempting to give a table of contents.

[Xaphiosis]

Thanks for resolving this, I think the outcome looks good now, only had trivial nitpicks. Time will tell whether anyone actually goes and looks at the debugging guide, but you've certainly left enough pointers to it.

Commit-wise, given that the "add vcg debugging guide" commit moves a whole lot of the previous "add debugging tips for vcg goals", would it make sense to merge the two?

[lsf37]

Thanks for resolving this, I think the outcome looks good now, only had trivial nitpicks. Time will tell whether anyone actually goes and looks at the debugging guide, but you've certainly left enough pointers to it.

👍

Commit-wise, given that the "add vcg debugging guide" commit moves a whole lot of the previous "add debugging tips for vcg goals", would it make sense to merge the two?

Oh, yes, absolutely. I thought I had already squashed them, but it seems I did not.