simpNF issues in Computability.RegularExpressions !4#2306

Stream: mathlib4

[Arien Malec]

In !4#2306, if I lint at line 99 after comp_def, I'm told that I'm able to simplify the definition of a large number of methods that were all created as a side effect of the inductive definition...

[Arien Malec]

I'm also told that matches' can simplify matches'._eq_4, which seems unhelpful.

[Arien Malec]

I also get the strangest possible path for simp for matches'_add, so I think that's safe to nolint.

[Arien Malec]

It's also very confusing how simpNF is saying that it can "prove" matches' which is a def

[Arien Malec]

OK, I used this trick to nolint the generated declarations: https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/nolinting.20generated.20decls/near/328300300

But I can't stop simpNF from complaining about matches' despite a nolint

[Arien Malec]

OK, attribute [nolint simpNF] matches'._eq_4 does it...

[Arien Malec]

Here is how simpNF proposed to "prove" the + branch of this def

def matches' : RegularExpression α → Language α
  | 0 => 0
  | 1 => 1
  | char a => {[a]}
  | P + Q => P.matches' + Q.matches'
  | P * Q => P.matches' * Q.matches'
  | star P => P.matches'∗

simp only [matches', add_eq_sup, ge_iff_le, le_eq_subset, sup_eq_union]

[Arien Malec]

I highlight add_eq_sup, which is defined on IdemSemiring α

[Arien Malec]

WHICH RegularExpression IS NOT....

[Arien Malec]

and the rest that are defined on Set which RegularExpression isn't. (And also simpNF wants to prove matches' by matches'). Something is wrong here.

[Gabriel Ebner]

Arien Malec said:

I also get the strangest possible path for simp for matches'_add, so I think that's safe to nolint.

nolint is bad here because the problem is still there. I'd just remove the @[simp] on matches'_add.

[Gabriel Ebner]

Looking at the file, the best solution is to remove the @[simp] on def matches', because that does something different than in Lean 3.

[Gabriel Ebner]

And now the generated simp lemmas reference plus a b instead of a + b which is not in simp nf.

[Gabriel Ebner]

Arien Malec said:

I highlight add_eq_sup, which is defined on IdemSemiring α

WHICH RegularExpression IS NOT....

This is not about regular expressions, this is about languages. And the way simp works here is indeed super unfortunate. It rewrites (a + b : Language A) first to a ⊔ b and then to a ∪ b.

[Gabriel Ebner]

I guess that's because we haven't merged !4#2307 yet.

[Arien Malec]

Ahhh. Yes, super unfortunate.

Removing @[simp] from matches' addresses things... Thanks!

[Arien Malec]

Sadly, this PR wasn't merged & after some changes to Language and the PR for NFA caused a merge conflict, needed to merge with master, which caused the PR to go from green to red, I assume because of the changes to Language?

I can get the failing proofs in matches'_map to work by removing map from the simp only but now run into issues with recursion, which previously Lean had no issues with...

[Arien Malec]

The only branch that Lean complains about is the R + S branch, which makes me think it's a side effect of the issues above?

[Eric Wieser]

I think my lean 3 refactor of docs#language will help here, #18451

[Arien Malec]

will cross tag -- thanks!