rw inside lambda

Stream: general

[Kenny Lau]

from my experience, simp can change things inside lambda, but rw cannot. Is there a way to bypass this and let rw change inside lambda?

[Mario Carneiro]

conv + rw

[Reid Barton]

Also see topic https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/rw.20under.20lambda/near/126107890 and the more verbose topic https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/Why.20can't.20.60rw.60.20look.20inside.20lambda.20expressions.3F/near/130212033

[Kenny Lau]

so exactly which tactics are avaiblale inside conv?

[Kevin Buzzard]

rw

[Kenny Lau]

I mean, a complete list of tactics available inside conv

[Kevin Buzzard]

There's probably a file in core which lists them. There's to_lhs, something called something like whnf and you might want to skim Patrick's docs

[Kevin Buzzard]

https://github.com/leanprover/lean/blob/master/library/init/meta/converter/interactive.lean

[Kevin Buzzard]

Maybe that's the definitive answer

[Kevin Buzzard]

Funext, change, simp and dsimp

[Kevin Buzzard]

https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

[Kevin Buzzard]

Has a couple of nice tricks

[Kenny Lau]

well I would like to be able to use apply/exact/refine inside conv

[Kenny Lau]

conv inside conv would also be useful

[Kenny Lau]

I feel like conv has a lot of potential to be the most powerful tactic ever

[Kenny Lau]

@Mario Carneiro I don't understand why there's no basic tactics (i.e. exact) inside conv

[Mario Carneiro]

conv is a different monad from tactic

[Mario Carneiro]

exact doesn't even make sense

[Kenny Lau]

I mean, why didn't we implement exact inside conv

[Kenny Lau]

conv is just a bunch of congr_arg and funext right

[Mario Carneiro]

the tactic state in the conv monad is basically ?p : X = ?m where ?p and ?m are to be determined

[Kenny Lau]

if we have a + b = c + d, and I do conv { to_lhs, congr, skip, } then the current state is a + b = a + ?m right

[Kenny Lau]

if I do exact (sorry : b = foo b) then I can tell Lean exactly that ?m should be foo b right

[Mario Carneiro]

by comparison to the regular tactic state which is just ?m : t

[Mario Carneiro]

I think update_lhs does that

[Johan Commelin]

I've never heard about that one. Sounds good!

[Johan Commelin]

Can you also zoom out in conv?

[Johan Commelin]

You zoom in with congr and funext. But I sometimes also want to zoom out again.

[Mario Carneiro]

No, zoom out doesn't make sense

[Mario Carneiro]

what is possible instead is a split lhs/rhs that produces multiple subgoals

[Mario Carneiro]

also, lhs/rhs is so passe. We need rcases patterns in conv!

[Kenny Lau]

what is update_lhs?

[Mario Carneiro]

I guess it is not an interactive command, but it is available as a conv tactic

[Mario Carneiro]

meta def update_lhs (new_lhs : expr) (h : expr) : conv unit :=
do transitivity,
   rhs >>= unify new_lhs,
   exact h,
   t ← target >>= instantiate_mvars,
   change t

[Johan Commelin]

@Mario Carneiro Why would zoom out not make sense? If I drill down into a nested sum, do some rw there, then I would want to zoom out again and play with the sum that is 1 level up.

[Mario Carneiro]

As I said, the conv monad has a state which is ?p : X = ?m. If you zoom in then ?m is assigned, so you can't return to it any more than you can rewind in a proof

[Mario Carneiro]

I think that to_lhs would make more sense as a tactic combinator, i.e. to_lhs { <conv> }, <conv>

[Mario Carneiro]

that would allow you to return to the outer context in the second part

[Kenny Lau]

also if I go deep inside using conv then all the variables have the same name and I can't even dedup

[Mario Carneiro]

note that find is actually a combinator like this inside conv, so you can use it to temporarily zoom in

[Mario Carneiro]

however, find patterns never work the way I want them to