# 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: May 09 2021 at 22:13 UTC