# Zulip Chat Archive

## Stream: general

### Topic: Extra instance makes exact_dec_trivial fail

#### Seul Baek (Feb 18 2019 at 19:47):

Here's a simple proof by `exact_dec_trivial`

:

import data.list.basic def foo (n : nat) : Prop := n = 0 instance : decidable_pred foo := begin intro n, simp [foo], apply_instance end example : ∀ n ∈ [0], foo n := by tactic.exact_dec_trivial

The proof succeeds because the instance `decidable_forall_mem {p : α → Prop} [decidable_pred p] (l : list α) : decidable (∀ x ∈ l, p x)`

is available. Although not necessary, having an extra instance of this type does not affect the proof:

import data.list.basic def foo (n : nat) : Prop := n = 0 instance : decidable_pred foo := begin intro n, simp [foo], apply_instance end instance bar {α} {p : α → Prop} [decidable_pred p] (l : list α) : decidable (∀ x ∈ l, p x) := decidable_of_iff _ list.all_iff_forall_prop example : ∀ n ∈ [0], foo n := by tactic.exact_dec_trivial

But if you add a slightly different instance of the same type:

import data.list.basic def foo (n : nat) : Prop := n = 0 instance : decidable_pred foo := begin intro n, simp [foo], apply_instance end instance baz {α} {p : α → Prop} [decidable_pred p] (l : list α) : decidable (∀ x ∈ l, p x) := begin cases l, apply decidable.is_true, intros x h, cases h, rw list.forall_mem_cons, apply and.decidable, end example : ∀ n ∈ [0], foo n := by tactic.exact_dec_trivial

Then `exact_dec_trivial`

doesn't work anymore. What's the difference between `bar`

and `baz`

that causes this?

#### Simon Hudon (Feb 18 2019 at 19:55):

If you set the option `pp.proofs`

to true and `#print baz`

, you're going to see a proof term. Part of it is:

eq.mpr (baz._proof_2 l_hd l_tl) and.decidable

I'm wondering if, with `baz._proof_2`

being opaque, `eq.mpr`

can't unfold it to do recursion on it.

#### Simon Hudon (Feb 18 2019 at 19:55):

@Mario Carneiro ?

#### Simon Hudon (Feb 18 2019 at 19:58):

Actually, now that I look more closely at `baz._proof_2`

, I see that it refers to `propext`

which is an axiom it cannot use for computation.

#### Kenny Lau (Feb 18 2019 at 20:28):

don't use tactics for definitions...

#### Kenny Lau (Feb 18 2019 at 20:29):

I think there's a similar issue with functions defined via `nat.strong_rec_on`

that the kernel/VM cannot unfold proofs

#### Mario Carneiro (Feb 19 2019 at 00:37):

Never use `rw`

or `cast`

to construct `decidable`

instances

#### Mario Carneiro (Feb 19 2019 at 00:37):

use `decidable_of_iff`

instead (you can then prove the iff statement however you want)

#### Mario Carneiro (Feb 19 2019 at 00:38):

This is important because `decidable_of_iff`

does not use `cast`

to get from one type to another, it pattern matches on one and uses the iff statement to get to the other

#### Mario Carneiro (Feb 19 2019 at 00:39):

If you use `rw`

, it will cast across `propext`

and the resulting term will get stuck in reduction, even when it should be provable

#### Moses Schönfinkel (Feb 19 2019 at 00:40):

This should be pinned or some such, these are impossible to debug for me. The last advice I got wrt. looking into `#reduce`

was to put a breakpoint in C++ code :-/.

#### Mario Carneiro (Feb 19 2019 at 00:42):

here's the important part of the example:

set_option pp.implicit true #reduce @baz _ foo _ [0] -- @eq.rec Type (decidable (0 = 0 ∧ ∀ (x : ℕ), false → x = 0)) (λ (_x : Type), _x) -- (@is_true (0 = 0 ∧ ∀ (x : ℕ), false → x = 0) _) -- (decidable (∀ (x : ℕ), x = 0 ∨ false → x = 0)) -- (propext _)

#### Mario Carneiro (Feb 19 2019 at 00:43):

it's stuck on a reduction of `propext`

#### Mario Carneiro (Feb 19 2019 at 00:43):

(example slightly unelided for clarity)

Last updated: May 14 2021 at 13:24 UTC