Zulip Chat Archive

Stream: general

Topic: Extra instance makes exact_dec_trivial fail


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Feb 18 2019 at 19:55):

@Mario Carneiro ?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Feb 18 2019 at 20:28):

don't use tactics for definitions...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 19 2019 at 00:37):

Never use rw or cast to construct decidable instances

view this post on Zulip Mario Carneiro (Feb 19 2019 at 00:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 :-/.

view this post on Zulip 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 _)

view this post on Zulip Mario Carneiro (Feb 19 2019 at 00:43):

it's stuck on a reduction of propext

view this post on Zulip Mario Carneiro (Feb 19 2019 at 00:43):

(example slightly unelided for clarity)


Last updated: May 14 2021 at 13:24 UTC