Extra instance makes exact_dec_trivial fail

Stream: general

[Seul Baek]

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]

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]

@Mario Carneiro ?

[Simon Hudon]

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]

don't use tactics for definitions...

[Kenny Lau]

I think there's a similar issue with functions defined via nat.strong_rec_on that the kernel/VM cannot unfold proofs

[Mario Carneiro]

Never use rw or cast to construct decidable instances

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

it's stuck on a reduction of propext

[Mario Carneiro]

(example slightly unelided for clarity)