Help wanted (make `ContextFreeRule.Rewrites` decidable)

Stream: general

[Martin Dvořák]

I'd like to delegate this task to somebody who (unlike me) knows what they are doing...

instance (r : ContextFreeRule T N) [DecidableEq T] [DecidableEq N] : DecidableRel r.Rewrites :=
  sorry

It should go into this place:
https://github.com/leanprover-community/mathlib4/blob/11add7feea9488bd2250bf2122566d4d92e675a2/Mathlib/Computability/ContextFreeGrammar.lean#L51

[Eric Wieser]

You need to write an algorithm to decide whether a string matches

[Eric Wieser]

I had a go at this last week, and it was harder than expected

[Eric Wieser]

The easy way out here is to prove that r.Rewrites x y (docs#ContextFreeRule.Rewrites) is the same as "there exists index of a symbol that was replaced", because lean will then generate an algorithm for you that iterates over all indices (though I think this will be O(x.length^2) due to the involvement of list indexing)