## 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