rewrite_search

Stream: general

[Scott Morrison]

Hi @Keeley Hoek, I think I'm getting "XXX" is not a valid rewrite lemma! errors which I shouldn't be. I think in this case the problem is you need to unfold a step before the lemma looks right. Can we make rewrite_search more forgiving?

[Scott Morrison]

There are examples in my branch <https://github.com/semorrison/monoidal-categories-reboot/tree/monoidal_functor.comp> of @Michael Jendrusch's new monoidal categories development.

[Keeley Hoek]

@Scott Morrison I can't see anything there which doesn't compile (on the monoidal_functor.comp branch), am I meant to try to remove the sorrys?

[Keeley Hoek]

Nonetheless, off a fuzzy memory of something like this happening to me with projections or local variables or something, I've made a total shot in the dark and hopefully whnf'd the problem away

[Scott Morrison]

Hmm, doesn't seem to have helped. Here's the problem: <https://github.com/semorrison/monoidal-categories-reboot/blob/monoidal_functor.comp/src/monoidal_categories_reboot/monoidal_category.lean#L52>

[Keeley Hoek]

Gotcha, I'll take a look

[Keeley Hoek]

ok I've just turned it the checks off for now. Does anyone know how to do something similar to #reduce, but to an expr in tactic-mode?

[Keeley Hoek]

I'd just like to unfold some definitions, to be able to tell certain things (e.g. of type monoidal_category.associator_naturality') are secretly just equalities

[Keeley Hoek]

I thought whnf maybe did this? Is there a problem if the expression being passed is after binders?

[Keeley Hoek]

ah, I see I want dsimp

[Keeley Hoek]

Hmm... it seems to unfold projections when I pass in arguments, but it doesn't deduce their type

[Scott Morrison]

Per the discussion in the maintainers' meeting this morning, I've located the rewrite_search branch, merged master, and got it compiling again. General challenge: understand what's in there, and work out a route to PR it into mathlib. :-)

[Bryan Gin-ge Chen]

I guess we could start by PRing everything not under tactic/rewrite_search that hasn't already been PR'd? Assuming the meta/expr and tactic/core changes are already in PRs, it looks like that's just two new files under data/array.