conv tactic `arg`

Stream: lean4

[Shreyas Srinivas]

Inside a conv tactic: I have reached the following goal state

evenOddRec h0 h_even h_odd (2 * n)

I now enter arg @5 and lean complains that it cannot select this argument. What arguments can arg not select inside conv.

[Shreyas Srinivas]

Extra information : lean cannot seem to select arg @1 either, but arg @2, arg @3, and arg @4 work as expected.

[Shreyas Srinivas]

Here is an #mwe

import Mathlib.Data.Nat.Basic
import Mathlib.Init.Data.Nat.Bitwise

namespace Nat

@[elab_as_elim]
def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (ih : P n), P (2 * n))
    (h_odd : ∀ (n) (ih : P n), P (2 * n + 1)) (n : ℕ) : P n := by
  refine' binaryRec h0 (fun b i hi => _) n
  cases b
  · simpa [bit, bit0_val i] using h_even i hi
  · simpa [bit, bit1_val i] using h_odd i hi

@[simp]
theorem even_odd_rec_zero (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) : @evenOddRec _ h0 h_even h_odd 0 = h0 :=
  binary_rec_zero _ _

@[simp]
theorem even_odd_rec_even (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) := by
  have bit_val_zero : ∀ n, 2 * n = bit false n := by
    intro
    rw[bit_val, cond]
    simp
  conv =>
    lhs
    arg @4

end Nat

[Shreyas Srinivas]

This is not essential for the porting effort per se, hence the question in the lean4 stream instead of mathlib

[Mario Carneiro]

conv can't enter dependent arguments of a function, since the congruence lemma for the function doesn't have subgoals for those arguments

[Mario Carneiro]

Also if you want to make a lean4 MWE you should remove the mathlib imports

[Shreyas Srinivas]

Mario Carneiro said:

Also if you want to make a lean4 MWE you should remove the mathlib imports

Ah okay, the code itself comes from the port effort. Plus it seemed to work in the lean 4 playground. Sorry about that

[Mario Carneiro]

it's more about making something suitable for an example in the test suite

[Mario Carneiro]

it is also useful for minimizing the problem so that it's only about arg and not about mathlib definitions

[Shreyas Srinivas]

I see. Makes sense. I'll keep mathlib out of #mwe s

[Kevin Buzzard]

You can leave them in in #mathlib4 , it's just in this stream where they're more picky ;-)