tactics as proof term misunderstanding

Stream: new members

[Fedor Pavutnitskiy]

I would like to understand the correspondence between tactics and proof terms a bit better. Consider nat.bit_val theorem :

lemma bit_val (b n) : bit b n = 2 * n + cond b 1 0 :=
by { cases b, apply bit0_val, apply bit1_val }

We can get the corresponding proof term using #print, which gives

theorem nat.bit_val : ∀ (b : bool) (n : ℕ), bit b n = 2 * n + cond b 1 0 :=
λ (b : bool) (n : ℕ), b.cases_on n.bit0_val n.bit1_val

and then if we try to use it solve the theorem

lemma my_bit_val : ∀ (b : bool) (n : ℕ), bit b n = 2 * n + cond b 1 0 := λ (b : bool) (n : ℕ), b.cases_on n.bit0_val n.bit1_val

we would get an error:

type mismatch at application
  b.cases_on _
term
  n.bit0_val
has type
  @bit0 ℕ nat.has_add n = 2 * n : Prop
but is expected to have type
  ?m_1 ff : Sort ?

Am I missing something here ? Got the same result usingset_option pp.implicit true.

[Alex J. Best]

It works if you do set_option pp.all true in this case, but unfortunately even this is not guarenteed, in Lean 3 we have the issue that the pretty printer does not always "round trip" properly and sometimes extra annotations are needed to fix things up

[Alex J. Best]

You can experiment a bit with the many pp options to try and get some more readable things that still work, e.g. set_option pp.numerals true and set_option pp.notation true gets rid of some junk

[Fedor Pavutnitskiy]

@Alex J. Best thanks for the suggestion. Is there a guaranteed way to get a proof term from tactics ?

[Alex J. Best]

Unfortunately I don't know of one, printing with pp.all true works well for not so complicated proofs, and beyond that the terms aren't very readable anyway so it seems to be ok.
There is also a tactic#show_term, which you can use from within tactic mode, but it suffers from the same issues with more complicated proofs. It is still very useful though

[Fedor Pavutnitskiy]

Thanks again. We are working on automatic proof term prediction and it would be nice to have a confident way to transform given tactics to proof terms.

[Alex J. Best]

Ah okay, if that is your use case you might want to ask in the #Machine Learning for Theorem Proving stream, there may be tools like https://github.com/jasonrute/lean_proof_recording that do what you want better than the interactive view