elabAselim issue

Stream: lean4

[Patrick Massot]

Still working on NNG4, I try to get rid of the definitional surprises that plagued the Lean 3 version. For this purpose I don't define the game natural number as an inductive but I put axioms everywhere. However I hit elaboration issues with the induction principle.

axiom MyNat : Type

notation "ℕ" => MyNat

axiom succ : ℕ → ℕ

@[instance] axiom myOfNat (n : Nat) : OfNat ℕ n

@[instance] axiom myAddition : HAdd ℕ ℕ ℕ

@[instance] axiom myMultiplication : HMul ℕ ℕ ℕ

axiom add_zero : ∀ a : ℕ, a + 0 = a

axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)

@[elabAsElim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n

example (n : ℕ) : 0 + n = n := by
  -- apply myInduction (P := λ n => 0 + n = n) n -- works
  apply myInduction n  -- failed to elaborate eliminator

without @[elabAsElim] it gets the motive completely wrong. With the attribute there is an error. What could I try? I wouldn't mind using a completely custom elaborator but I have no idea how to do that.

[Leonardo de Moura]

The [elabAsElim] strategy requires the expected type to be available, but the apply tactic elaborates the term without an expected type (see elabTermForApply). One option is to use refine or refine'.

  refine myInduction n ?base ?ind

or

  refine' myInduction n _ _

Another option is to write a variant of apply that behaves like the refine tactics above but we doesn't force us to add the _s.

[Patrick Massot]

Thanks!

[Patrick Massot]

Now I need to figure out how to do that in a tactic (while jump to definition on refine doesn't seem to work)

[Patrick Massot]

Actually a macro is probably good enough.