conv navigation : Zoom out

Stream: lean4

[Shreyas Srinivas]

I have a question about navigating in conv. Suppose your goal looks like f a b c = ....
Now I use conv to zoom in on a and do some careful rewriting as follows

conv =>
   lhs
   arg 1
   --- tactics to  modify a

How do I zoom out of a so that I can do something with b for example.

[Kyle Miller]

I think you can use curly braces, so

{ arg 1
  ... }

[Shreyas Srinivas]

Kyle Miller said:

I think you can use curly braces, so

{ arg 1
  ... }

I get spurious no goals to be solved

[Kyle Miller]

Oh, I see, conv doesn't support this sort of thing as far as I can tell.

[Kyle Miller]

You can do congr (or equivalently args) instead of arg 1 and then use rfl for each argument you don't want to handle

[Kyle Miller]

example (a b c : Nat) (f : Nat → Nat → Nat → Nat) (h : a = x) (h' : b = y) : f a b c = f x y c := by
  conv =>
    lhs
    args
    { rw [h] }
    { rw [h'] }
    rfl -- or { }

[Shreyas Srinivas]

Kyle Miller said:

example (a b c : Nat) (f : Nat → Nat → Nat → Nat) (h : a = x) (h' : b = y) : f a b c = f x y c := by
  conv =>
    lhs
    args
    { rw [h] }
    { rw [h'] }
    rfl -- or { }

This works but only partially in my case. When I need to do something other than rfl in the end, I again get spurious no goals to be solved errors

[Shreyas Srinivas]

Thanks for the congr and args suggestion. It helps to a certain extent

[Shreyas Srinivas]

Although it might be a useful feature to be able to navigate one step higher in the expression tree

[Kyle Miller]

It seems like it might be useful, but I think that'd take redesigning conv mode. Right now you can't re-conv the result of a previous conv, and arg 1 works by doing congr and then rfl on every goal but number 1.

[Kyle Miller]

Another thing you could do is a sequence of convs. There's a short form enter [...] for navigation. enter [1, 1] should get you to the LHS, arg 1, for example.

[Shreyas Srinivas]

Kyle Miller said:

It seems like it might be useful, but I think that'd take redesigning conv mode. Right now you can't re-conv the result of a previous conv, and arg 1 works by doing congr and then rfl on every goal but number 1.

Currently I am working around the issue by introducing new conv blocks.

[Shreyas Srinivas]

But then the question is, for every path from the top level expression to the leaf nodes, should users have to start a new conv.

[Kyle Miller]

Oh, you know what, it turns out you can do this using nested conv:

example (a b c : Nat) (f : Nat → Nat → Nat → Nat) (h : a = x) (h' : b = y) : f a b c = f x y c := by
  conv =>
    lhs
    conv =>
      arg 1
      rw [h]
    conv =>
      arg 2
      rw [h']

[Kyle Miller]

I didn't find the documentation particularly illuminating, but the implementation seemed promising as I was reading through the source trying to uncover Lean's secrets

[Tomas Skrivan]

Yes nesting conv blocks is the way to go, it works well.

The only annoying thing I found is that sometimrs it feels a bit too verbose than a zoom out command would and nested blocks do not support conv in <pattern> => ... syntax.

[Kyle Miller]

It turns out conv in <pattern> => ... syntax is a synonym for conv => pattern <pattern>; .... It shouldn't be hard to add nested conv in as additional syntax.