rewrite entire

Stream: general

[Scott Morrison]

Hi all, this is a follow-up to my difficulties with the occs configuration for rw. I'm still not there writing a "please find _all_ the possible rewrites" function.

Something that would be really helpful for me would be a "rewrite entire" function, that takes r:expr and e:expr, where r is some rewrite rule, and tells me whether it can rewrite the entirety of e using it (that is, not rewriting a subexpression).

[Scott Morrison]

I'm pretty confident I can implement that myself, but I think it may exist already, or be even easier than I'm anticipating, so I thought I'd ask here.

[Simon Hudon]

I haven't seen it anywhere

[Simon Hudon]

To be clear, r may be forall x y z, E = F and that tactic would unify E with the parameter e. Is that accurate?

[Scott Morrison]

Yes, that's exactly what I want.

[Scott Morrison]

Ok, I can do it myself easily enough.

[Mario Carneiro]

I think simp_lemmas will do that

[Scott Morrison]

@Mario Carneiro, the documentation for simp_lemmas talks about simplification lemmas. Can I ignore that and
attempt to use it with arbitrary rewrite rules? And it won't attempt to look in subexpressions, just rewrite the entire thing?

[Scott Morrison]

I guess I can read the implementation of simp_lemmas.rewrite myself... :-)

[Mario Carneiro]

Pretty sure it doesn't look in subexpressions, since it is intended for use with ext_simplify_core which does the subexpression traversal itself

[Scott Morrison]

Ah, I see.

[Scott Morrison]

okay, I will give that a go.

[Scott Morrison]

Do we have an analogue of mk_eq_symm that traverses through binders?

[Scott Morrison]

e.g. turning the expr λ a : A, λ b : B, f a b = g a b into λ a : A, λ b : B, g a b = f a b?

[Scott Morrison]

expr.lean is spectacularly unhelpful about the arguments of expr.elet. One can glean from it that the four expr arguments of elet ought to be called n, g, e, f, in that order, but not much more. Is there somewhere these things are written down?

[Scott Morrison]

Oh... I was asking for the wrong thing, and I don't think I know how to do it. Suppose I have an expr which is just the name of a equation lemma; how can I get the eq.symm version of that lemma?

[Scott Morrison]

I'm guessing I need to ... infer the type of my expression, and then while the type is Pi, replace the expression with a lambda wrapped around it, and then when there are no more Pis use mk_eq_symm?