conv to focus on the function

Stream: Is there code for X?

[Joachim Breitner]

In conv mode, if I have

| f a b

I understand that left (or lhs) will focus on a, and right (or rhs) will focus on b.

How can I focus on f?

If there isn't an easy tactic for that already, is it worth adding?

[Floris van Doorn]

I don't see it (I haven't used conv much in Lean 4 yet), but that is definitely worth having!

[Riccardo Brasca]

What happens if you use the conv widget?

[Joachim Breitner]

If I used it correctly:

 Error: Not a valid conv target

[Michael Stoll]

Maybe conv => enter [0] would be a reasonable way to specify that, if it gets included in conv.

[Joachim Breitner]

Intuitively, I tried and hoped for

conv => fun

but that’s a keyword (not sure if that prevents it from working here)

[Riccardo Brasca]

Joachim Breitner said:

If I used it correctly:

 Error: Not a valid conv target

Same here.

[Mauricio Collares]

Maybe arg 1?

[Joachim Breitner]

It seems I can simply use apply congrFun:

example (P Q : Nat → Nat → Nat → Prop) (h : P = Q ) (h2 : Q 1 2 3) : P 1 2 3 := by
  conv =>
    apply congrFun
    apply congrFun
    apply congrFun
    rw [h]
  exact h2

It shows some extra

case h.h.g
PQ: Nat → Nat → Nat → Prop
h: P = Q
h2: Q 1 2 3
⊢ Nat → Nat → Nat → Prop

on the side, arising from the implicit argument {g} of congrFun, which left doesn’t – expected? Can I avoid that easily?

[Mauricio Collares]

In this case you can also write pattern P, I think (might not be practical in a real-world example)

[Joachim Breitner]

Thanks! But yeah, that won’t work in my intended use case (in a non-interactive tactic script)

[Kyle Miller]

It would make sense having a conv tactic for rewriting the function. That would mimic how simp works: it effectively

1. applies this non-existent conv tactic to create a goal to recursively simplify the function, and then it
2. applies the congr tactic to create goals for each argument, and then it recursively simplify each argument

The limitation in congr (and thus enter, left, right, etc.) is because conv is only making use of the congruence lemmas generated for step 2.

[Kyle Miller]

Here's the function where simp simplifies the function and then creates a congrFun chain.

[Joachim Breitner]

Created an RFC to ask for a function-focusing conv tactic: https://github.com/leanprover/lean4/issues/3239

[Joachim Breitner]

Also created a PR. Does someone want to sanity check it?
https://github.com/leanprover/lean4/pull/3240

[Tomas Skrivan]

I had a brief look and it looks good! The only thing I do not understand is the need for ← isDefEqGuarded rhs rhs' check but I see this kinds of stuff all over Lean code base so I'm not surprised by it.

[Tomas Skrivan]

If you are in the mood of improving conv would it be possible to modify conv such that you can enter[...] into if c then t else f statements? In particular I want to focus on either t or f.

[Kevin Buzzard]

You can't do this with congr?

[Joachim Breitner]

Or left and right? Or possibly arg 2 and arg 3?

[Tomas Skrivan]

Nope it does not work
mwe

example (x : Nat) : (if x = 3 then 1+1 else 1-1) = sorry := by
  conv =>
    lhs
    enter[4] -- only 4 works
  sorry

[Tomas Skrivan]

congr works but then you have to modify the condition and both branches

[Kyle Miller]

Interesting, if you do congr you can get into each piece (and use rfl like usual for the ones you don't want to handle), but it creates a non-conv Decidable goal as well, since we don't know the RHS condition yet.

[Kyle Miller]

That seems to be choking up enter

[Kyle Miller]

I wonder if conv should have some protocol for collecting certain goals that it should be responsible for itself, like eventually discharging this Decidable.

[Kyle Miller]

It can definitely discharge this: ideally it uses infer_instance, but if that fails it can rewrite the original Decidable to construct the instance.

[Joachim Breitner]

This should probably be reported as an issue