Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: dec_trivial


Markus Himmel (Jul 15 2020 at 13:40):

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 (Jul 15 2020 at 14:24):

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 (Jul 20 2020 at 08:15):

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


Last updated: Dec 20 2023 at 11:08 UTC