Zulip Chat Archive

Stream: new members

Topic: extracting tactics and proof terms


view this post on Zulip Michael Jendrusch (Nov 12 2018 at 10:25):

This is probably a question with a simple answer, but I'll ask it either way. Is there a way to programmatically extract the sequence of tactics used to prove a given lemma? I can get the proof term pretty easily by doing something like this:

import tactic
open tactic.interactive

namespace my_namespace

lemma my_lemma : Π n : , n + 1 > n :=
begin
  intros,
  rw gt,
  simp,
  comp_val,
end

#eval do
  env  tactic.get_env,
  ml   env.get(mk_str_name "my_namespace" "my_lemma"),
  fmt  tactic_format_expr ml.value,
  trace $ "type  : " ++ (to_string $ expr.to_raw_fmt ml.type) ++ "\n",
  trace $ "value : " ++ (to_string $ expr.to_raw_fmt ml.value) ++ "\n",
  return unit.star

end my_namespace

but I haven't had any luck extracting tactics yet. On another note, is there some function other than expr.to_raw_fmt for serializing expressions?

view this post on Zulip Mario Carneiro (Nov 12 2018 at 10:36):

No. It's not stored

view this post on Zulip Keeley Hoek (Nov 12 2018 at 10:41):

What do you mean "serializing"?

view this post on Zulip Michael Jendrusch (Nov 12 2018 at 11:29):

Serializing, as in generating some text (s-expression, JSON) or binary representation of expressions which can be read from another program. But I suppose expr.to_raw_fmtshould be enough for my purposes.


Last updated: May 08 2021 at 19:11 UTC