add corres_cases method

[lsf37]

Add safe datatype case distinction for corres -- wpc turns out to be insufficient even after generalisation of the helper predicate.

• corres_cases_left: case distinction on abstract monad
• corres_cases_right: case distinction on concrete monad
• corres_cases: case distinction first of abstract/concrete monad
• corres_cases_both: simultaneous (quadratic) case distinction on both sides, with safe elimination of trivially contradictory cases

Main intended benefit is less thinking about safety of schematics, fewer mentions of goal parameter names, and fewer manual guard instantiations.

The PR also removes the old defunct wpc setup for corres and changes a few proofs in refine/ARM to demonstrate how the method is intended to be used.

[Xaphiosis]

I am happy with the methods and the improvement they provide. Nice! I also like that they manage to do what they do concisely. If I tried to to it, it could've ended up an over-engineered mess. This approach ends up very neat.

I do have some difficulty following some of the textual descriptions, and wonder if I'm too ignorant to be the target audience, or whether the descriptions could become easier. A few Englishisms snuck in there as well.

[lsf37]

(updated with Raf's review feedback)

[Xaphiosis]

Last typos, otherwise I'm happy with it, the explanations are now ones I can follow. Thank you!

[corlewis]

Very cool work, the examples demonstrating the reduced need for manual instantiation are particularly encouraging.

My only remaining confusion is why wpc seems to work in crefine. Do we just avoid the cases where the guards don't depend on the bound variable being split? If so that suggests we might want something very similar to this for ccorres as well.

[lsf37]

My only remaining confusion is why wpc seems to work in crefine. Do we just avoid the cases where the guards don't depend on the bound variable being split? If so that suggests we might want something very similar to this for ccorres as well.

I was thinking that the problem doesn't occur in ccorres, because we don't have a normal rv thing going on on the C side, and I thought that eliminates the problem. But a) we do have things like symbolic execution, and b) that actually makes the problem worse, because the abstract guard will depend on abstract goal parameters, and the C guard will not, which is exactly the case I'm trying to solve.

So I think you're right and we should probably be doing the same thing for ccorres. Do we have cases where wpc mysteriously doesn't work on ccorres? (because that's probably because of exactly this issue).

[lsf37]

I'll leave ccorres for another time, but I think Corey is right and it would probably benefit from the same treatment, which means we can likely reduce wpc to just single-guard cases which should make it a bit simpler again.

Doing ccorres properly is going to be slightly annoying, because for corres the abstract and concrete guard are interchangeable, so the same processing rules work for them. But for ccorres the type determines which one is concrete and which one is abstract. On the other hand, I don't think we want to do cases on the C side anyway, so maybe it's not so bad.

All of this now gives me ideas that we could include a thing for if .. then .. else in corres_cases as well. Hm. Tempting.

[corlewis]

So I think you're right and we should probably be doing the same thing for ccorres. Do we have cases where wpc mysteriously doesn't work on ccorres? (because that's probably because of exactly this issue).

I don't know about one with wpc, but I have definitely had cases in ccorres where I wanted to split a concrete IF .. THEN .. ELSE .. and the abstract precondition didn't have the required bound variable.

[lsf37]

So I think you're right and we should probably be doing the same thing for ccorres. Do we have cases where wpc mysteriously doesn't work on ccorres? (because that's probably because of exactly this issue).

I don't know about one with wpc, but I have definitely had cases in ccorres where I wanted to split a concrete IF .. THEN .. ELSE .. and the abstract precondition didn't have the required bound variable.

Right, that's another case we should treat. I should probably start collecting these in an issue.