tactic.result

Stream: metaprogramming / tactics

[Fabian Glöckle]

Hi, I need help in figuring out how to retrieve the (partial) proof term produced by some tactics. Consider the following mwe:

import tactic
open tactic

def example_lemma : 1 = 1 := by tidy

#print example_lemma
-- def example_lemma : 1 = 1 := eq.refl 1

meta def tidy_test : tactic unit :=
do
  mv ← mk_meta_var `(1=1),
  tactic.set_goals [mv],
  tactic.get_goals >>= list.mmap infer_type >>= trace,
  -- [1 = 1]
  tactic.result >>= infer_type >>= trace,
  -- true
  tactic.tidy.core >>= trace,
  -- [refl]
  tactic.result >>= infer_type >>= trace,
  -- true
  pure ()

#eval tidy_test

example_lemma shows that tidy is able to find the refl proof of 1 = 1. When I manually set this as the proof goal and call tactic.tidy.core, tactic.get_goals will report the correct goal and tactic.tidy.core it is able to produce the correct tactic, but tactic.result still contains a mvar of type true as if set_goals had never been called.

How does one correctly set goals in tactic mode, call tactics and retrieve the partial proof term constructed by the tactics? Thanks in advance!

[Scott Morrison]

I think you aren't interested in tactic.result. Instead just look at the metavariable mv you constructed. After running the tactic on your synthetic goal, you can call instantiate_mvars mv and it should contain (the expr corresponding to) the term constructed by the tactic.

[Scott Morrison]

tactic.result isn't fooled by your pretend goals. :-)

[Fabian Glöckle]

I see! That works, thank you :)