Weird tactic_state argument in tactics

Stream: new members

[Gareth Ma]

Hi! I have been looking at tactics for a while now (approximately an hour), and here is what I am trying to do: I am writing a tactic that proves an integer is even! So exciting. The idea is to try each integer one by one, from 0, 1, 2, ... Here's my attempt:

import data.stream.defs
import data.bool.all_any
import data.lazy_list
import tactic

open expr tactic widget

meta def prove_even_aux (n : ℕ) : tactic unit :=
do {
     `(even %%p) ← target,
     tp ← infer_type p,
     guard (tp = `(ℕ)),
     to_expr ``(%%(reflect n)) >>= existsi,
     exact_dec_trivial
   }
   --  <|> fail "???"
   <|> prove_even_aux n.succ

meta def prove_even : tactic unit := prove_even_aux 0

example : even 8 := by prove_even

It almost works, as in if I remove the <|> and directly prove with 4, then the example succeeds. However, with the code above I am getting a weird error of

type mismatch at application
  prove_even_aux n.succ
term
  n.succ
has type
  ℕ
but is expected to have type
  tactic_state

Can someone explain how this happens? It seems to me that prove_even_aux takes one ℕ argument.

[Gareth Ma]

Here's a minimal code:

meta def mwc' (n : ℕ) : tactic unit :=
do if n % 2 = 0 then return () else return (mwc' n)

[Alex J. Best]

If you want to recurse on an argument it needs to go after the colon

import data.stream.defs
import data.bool.all_any
import data.lazy_list
import tactic

open expr tactic widget

meta def prove_even_aux : Π n : ℕ, tactic unit
| n :=
do {
     `(even %%p) ← target,
     tp ← infer_type p,
     guard (tp = `(ℕ)),
     to_expr ``(%%(reflect n)) >>= existsi,
     exact_dec_trivial
   }
   --  <|> fail "???"
   <|> (prove_even_aux n.succ)

meta def prove_even : tactic unit := prove_even_aux 0

example : even 8 := by prove_even

from within prove_even_aux the type of itself has those arguments before the colon fixed essentially

[Kevin Buzzard]

This has been changed in lean 4 I think (and I'd recommend learning how to write tactics like this in lean 4 rather than lean 3)

[Gareth Ma]

Hi Kevin, I knew you would comment :joy: I just wanted to get a feel of how metaprogramming works, I will look at how it works in Lean 4 quite soon :) At least I know now that it's not as hard as I thought it is

[Gareth Ma]

Also another question, is to_expr ``(%%(reflect n)) >>= existsi the best way to do it? I essentially want to do use n but Lean refuses