Demo lemmas from WPFix confuse the sledgehammer

[talsewell]

Reported by a student in the UNSW COMP4161 class:

When in a session that uses autocorres, the sledgehammer produces this nonsense outcome:

Sledgehammering...
vampire found a proof...
Derived "False" from these facts alone: demo1

That demo lemma was only ever written to try to explain what WPFix does. It looks like vampire (maybe without types) is somehow confused by it and think it is contradictory.

Anyway, it would be good to remove the names from these demo lemmas, or move them into a demo theory, or otherwise prevent them being seen by find_theorems, sledgehammer, etc.

[lsf37]

Hm, in the end this is a sledgehammer bug. The lemma isn't contradictory, so the translation is losing too much information.

But I do agree that we should remove the trigger. Are you sure that removing the name makes it invisible to sledgehammer? If not, maybe we can move it into an experiment context or otherwise discard it as a lemma if a separate Demo theory doesn't make sense. We do have the separate Demo theories for most setups, so that's probably the easiest way to go here, it's just a bit awkward in the Monads session itself.

[talsewell]

Aha, I was sure there was something like experiment, thanks for reminding me of its name. I think any of these would fix the problem, and using experiment might be the simplest.

[lsf37]

You're right, experiment works fine for these: #832

[ordinarymath]

Hm, in the end this is a sledgehammer bug. The lemma isn't contradictory, so the translation is losing too much information.

But I do agree that we should remove the trigger. Are you sure that removing the name makes it invisible to sledgehammer? If not, maybe we can move it into an experiment context or otherwise discard it as a lemma if a separate Demo theory doesn't make sense. We do have the separate Demo theories for most setups, so that's probably the easiest way to go here, it's just a bit awkward in the Monads session itself.

Sorry for commenting on a closed issue but would like to inform that the no_atp attribute is the way of blacklisting lemmas from sledgehammer. Might be useful if it occurs for a lemma you cant delete.