Closed chaudhuri closed 10 months ago
This is not completely fixed. Negative instances of prop
can be hidden with polymorphic types.
I managed to minimize the script and the proof I found, the idea is still based on Russel's paradox in naive set theory (hence the names):
Kind set type.
Type naive (set -> prop) -> set.
Define nomember_of_itself : set -> prop by
nomember_of_itself (naive S) := S (naive S) -> false.
Theorem nomember_of_itself : nomember_of_itself (naive nomember_of_itself) -> false.
intros. case H1. backchain H2.
Theorem oops: false.
assert (nomember_of_itself (naive nomember_of_itself) -> false) -> false.
intros. backchain H1. apply H1 to nomember_of_itself.
(Edit: tested in commit #74770b6d1dff51084c3ec5d73b86d9293047bfaf, and as expected also this shortened proof no longer works there, unless prop is hidden inside polymorphism.)
No, it still works if you have Type naive (set -> A) -> set
.
As I understand it, @gnadathur97's suggestion is to instead prevent definitions such as nomember_of_itself
because it has a parameter S
whose type contains prop
.
For now I will just add a warning for this kind of definition. Preventing such definitions will break some existing examples that use "higher-order" definitions that were used as a shortcut to a decent module system in Abella.
I'm pleased to hear that the solution will be to generate warnings somewhere along the way: it's nice to be able to experiment with parameters that contain prop.
The new version just emits a warning and lists all the higher-order parameters. Not yet sure which scenarios are definitely errors and which are in some kind of grey area.
Closing this. Please comment if you discover anything else strange.
This is a slightly edited summary of an email from @gnadathur97: