# 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