Golf: context-free languages are not closed under compl...

Stream: new members

[Martin Dvořák]

Eric Wieser said:

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

Thanks a lot!!

https://github.com/madvorak/grammars/commit/eeca448ca5b22a8a53683e9464d81ec9438a9d78

[Notification Bot]

Martin Dvořák has marked this topic as resolved.

[Martin Dvořák]

PS: Maybe these three lines can be turned into one?

have nny := nnyCF_of_CF_i_CF,
push_neg at nny,
rcases nny with ⟨T, L₁, L₂, ⟨hL₁, hL₂⟩, hyp_neg⟩,

[Notification Bot]

Martin Dvořák has marked this topic as unresolved.

[Eric Rodriguez]

I doubt it, that push_neg is doing a lott of work

[Eric Rodriguez]

I wonder if nnyCF_of_CF_i_CF should be the push_neg'd version from the start, though

[Martin Dvořák]

Eric Rodriguez said:

I wonder if nnyCF_of_CF_i_CF should be the push_neg'd version from the start, though

For building on top of it, yes. For presentation of the results, no.

[Martin Dvořák]

Eric Rodriguez said:

I doubt it, that push_neg is doing a lott of work

Maybe there is something like the following (incorrect code)?

rcases (push_neg_result { nnyCF_of_CF_i_CF }) with ⟨T, L₁, L₂, ⟨hL₁, hL₂⟩, hyp_neg⟩,

[Martin Dvořák]

Eric Rodriguez said:

I wonder if nnyCF_of_CF_i_CF should be the push_neg'd version from the start, though

I could even state the theorem for the concrete counterexample. But I like it better when it stays abstract on the outside.

[Martin Dvořák]

This is another obvious candidate for refactoring:
https://github.com/madvorak/grammars/blob/eeca448ca5b22a8a53683e9464d81ec9438a9d78/src/context_free/closure_properties/binary/CF_intersection_CF.lean#L1441
However, I feel less like changing this one.

[Martin Dvořák]

Martin Dvořák said:

This is another obvious candidate for refactoring:
https://github.com/madvorak/grammars/blob/eeca448ca5b22a8a53683e9464d81ec9438a9d78/src/context_free/closure_properties/binary/CF_intersection_CF.lean#L1441
However, I feel less like changing this one.

I golfed it a little bit anyways. Ignore that one.