Weird interaction of `by` and application

Stream: general

[Jannis Limperg]

I would have expected by exact t to be roughly equivalent to t, but it seems like it's decidedly not:

#check (by exact nat.add) nat.zero nat.zero

/-
1:12: type mismatch at application
  interactive.executor.execute_explicit tactic
    (has_bind.seq (tactic.save_info {line := 1, column := 11})
       (tactic.istep 1 11 1 11 (tactic.interactive.exact ``(nat.add))))
    0
term
  0
has type
  ℕ
but is expected to have type
  tactic_state
-/

Apparently the nat.zero is interpreted as an argument to the tactic within the by?

[Kevin Buzzard]

nat.plus does not exist as far as I know -- is this the actual issue?

[Gabriel Ebner]

Hmm, not even this works:

#check (by exact nat.add : _) nat.zero nat.zero
/-
function expected at
  ?m_1
term has type
  ?m_1
-/

[Jannis Limperg]

Kevin Buzzard said:

nat.plus does not exist as far as I know -- is this the actual issue?

No unfortunately. I've updated the example with nat.add; same effect.

[Floris van Doorn]

This is not too surprising to me. Placeholders cannot occur in places of functions, since it's hard to figure out what the type of the function is.

example (f : ℕ → ℕ) : _ nat.zero = f 0 :=
rfl
-- error: placeholders '_' cannot be used where a function is expected

In the above example, the _ could have type ℕ → ℕ but also something like Π (n : ℕ), @nat.rec (λ _, Type) ℕ (λ _ _, bool) n.
In the same way I'm not surprised that replacing the placeholder by a tactic also fails, but a nicer error message would be nice:

example (f : ℕ → ℕ) : (by exact f) nat.zero = f 0 := rfl
example (f : ℕ → ℕ) : f 0 = f 0 := (by reflexivity) 0
-- an improved error message would be: tactics cannot be used where a function is expected

[Floris van Doorn]

Floris van Doorn said:

Π (n : ℕ), @nat.rec (λ _, Type) ℕ (λ _ _, bool) n

For the non-type theorists, here is a more understandable example:

noncomputable theory
constant f : ℕ → ℕ

def P : ℕ → Type
| 0     := ℕ
| (n+1) := bool

def g : Π n, P n
| 0     := f 0
| (n+1) := tt

example : g 0 = f 0 := rfl

Note that g has a different type than f, but g 0 and f 0 are (definitionally) equal.

[Gabriel Ebner]

Floris van Doorn said:

This is not too surprising to me.

There are two bugs here:

1. That it doesn't work. This is indeed not surprising, and will give an error in Lean 4 ("expected type not known").
2. That the arguments are just added to the tactic and then elaborated as a normal term. This is the surprising part, but I don't think I'm motivated to fix it. The reason why this happens is because tactics blocks are stored as "annotations". Annotations are also used for show-from, have-from, etc. These are then stripped from functions during elaboration:

    while (is_annotation(fn))
        fn = get_annotation_arg(fn);

[Gabriel Ebner]

This is what I mean by surprising:

meta def hmmm : tactic unit := λ s, (by exact 0) s
#check by hmmm -- 0

[Mario Carneiro]

wait, that's triply surprising because you didn't say hmm := `[exact 0], you said hmm := by exact 0 (after eta reduction)