Make Starling warn the user if one of the views is unsatisfiable

[septract]

Unsatisfiable views are a persistent problem when developing Starling+GH proofs - it'd be useful to raise a warning (or fail the proof?)

This would mean injecting P=>false procedures for each defining view, then requiring that each of them fails. This would require basically running GRASShopper in two directions, one to falsify these and one to validate the rest, which is a bit messy. It's also messy because GRASShopper doesn't have an 'expect failure' mode for a proof term.

[MattWindsor91]

Would this be in terms of a check to see that:

• any defining views that are contradictory under SMT are constrained specifically to false (fairly easy check to add but wouldn't catch many GRASShopper-level problems unless it got kicked into a deferred check and even then I'm unsure of the best encoding);
• all terms have a non-contradictory postcondition under SMT (this would throw up too many false positives I think);
• if we inject P=>false procedures for each defining view, that each of them fails (this would require basically running GRASShopper in two directions, one to falsify these and one to validate the rest, which is a bit messy);
• something else?

[septract]

Yeah, the third one. Let me edit the issue to make this clear.