Zulip Chat Archive

Stream: new members

Topic: Golf: context-free languages are not closed under complement


Martin Dvořák (Dec 20 2022 at 11:13):

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 (Dec 20 2022 at 12:24):

Line 26 can be

intro hv; finish

and then then rest isn't needed

Martin Dvořák (Dec 20 2022 at 12:33):

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

Martin Dvořák (Dec 20 2022 at 12:35):

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

Eric Wieser (Dec 20 2022 at 12:37):

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


Last updated: Dec 20 2023 at 11:08 UTC