dec_trivial

Stream: metaprogramming / tactics

[Markus Himmel]

Hi, I tried to understand how dec_trivial works. I read the corrsponding section in TPIL, but there are still some things I don't understand. In particular, I don't understand how by tactic.triv differs from trivial, and why things like whether the statement is an example or a lemma and @ notation seem to affect whether a proof works, as illustrated by these examples:

example : 0 ≠ 1 := dec_trivial -- works
example : 0 ≠ 1 := of_as_true (by tactic.triv) -- works
example : 0 ≠ 1 := of_as_true trivial -- fails
lemma a : 0 ≠ 1 := of_as_true trivial -- works
lemma b : 0 ≠ 1 := @of_as_true _ _ trivial -- fails
lemma c : 0 ≠ 1 := @of_as_true _ _ (by tactic.triv) -- works

Could anyone explain what's happening here?

[Simon Hudon]

The difference here is how Lean elaborates the terms. By the time trivial is being elaborated, we haven't done the reduction of the decidable instance yet. But with by, elaboration is done differently. I think @Gabriel Ebner might be more able to fill in the details of the elaboration process

[Gabriel Ebner]

Yes, tactics are first put in a list and then executed later. In particular, we try to synthesize type-class instances first.