Golf: context-free languages are not closed under complement

Stream: new members

[Martin Dvořák]

I have a golfing request.
I proved that context-free languages aren't closed under complement.
https://github.com/madvorak/grammars/blob/main/src/context_free/closure_properties/unary/complement_CF.lean
The file is over 50 lines long, despite of the fact that the proof is basically just De Morgan.

I have theorem CF_of_CF_u_CF saying that context-free languages are closed under union.
I have theorem nnyCF_of_CF_i_CF saying that context-free languages aren't closed under intersection.
It immediately follows that (theorem nnyCF_of_complement_CF which I prove in this file) aren't closed under complement.
Maybe there is a one-line proof that will do the same.

[David Renshaw]

Line 26 can be

intro hv; finish

and then then rest isn't needed

[Martin Dvořák]

Unfortunately, that increases the verification time from 130 ms to 4688 ms. Could you please golf a proof term instead?

[Martin Dvořák]

Just yesterday, I was refactoring some finish lines away, in order to speed up verification.

[Eric Wieser]

rwa [language.add_def, set.compl_union, compl_compl, compl_compl] at contra, closes the goal on line 24