easy decidability q

Stream: general

[Kevin Buzzard]

Is this provable:

import data.multiset
example (C : multiset ℕ) : decidable (∃ a : ℕ, a ≥ 4 ∧ a ∈ C) := sorry

and if so, is there a cheap proof? I tried doing it by hand and ended up with a horrible heq goal :-/

[Kenny Lau]

yes it is provable

[Kenny Lau]

might want to destruct C

[Simon Hudon]

Isn't membership in multisets decidable? You combine that fact with decidability of existentials on finite ranges

[Kevin Buzzard]

If I use lists I end up with

C1 C2 : list ℕ,
Crel : setoid.r C1 C2
⊢ eq.rec
      (list.rec (is_false _)
         (λ (n : ℕ) (L : list ℕ),
            decidable.rec
              (λ (D : ¬∃ (a : ℕ), a ≥ 4 ∧ a ∈ ↑L),
                 dite (3 < n) (λ (h : 3 < n), is_true _) (λ (h : ¬3 < n), is_false _))
              (λ (D : ∃ (a : ℕ), a ≥ 4 ∧ a ∈ ↑L), is_true _))
         C1)
      _ =
    list.rec (is_false _)
      (λ (n : ℕ) (L : list ℕ),
         decidable.rec
           (λ (D : ¬∃ (a : ℕ), a ≥ 4 ∧ a ∈ ↑L),
              dite (3 < n) (λ (h : 3 < n), is_true _) (λ (h : ¬3 < n), is_false _))
           (λ (D : ∃ (a : ℕ), a ≥ 4 ∧ a ∈ ↑L), is_true _))
      C2

[Kevin Buzzard]

If I use multiset.rec I end up with

a a' : ℕ,
m : multiset ℕ,
b : decidable (∃ (a : ℕ), a ≥ 4 ∧ a ∈ m)
⊢ decidable.rec
      (λ (H : ¬∃ (a : ℕ), a ≥ 4 ∧ a ∈ a' :: m),
         dite (3 < a) (λ (h : 3 < a), is_true _) (λ (h : ¬3 < a), is_false _))
      (λ (H : ∃ (a : ℕ), a ≥ 4 ∧ a ∈ a' :: m), is_true _)
      (decidable.rec
         (λ (H : ¬∃ (a : ℕ), a ≥ 4 ∧ a ∈ m),
            dite (3 < a') (λ (h : 3 < a'), is_true _) (λ (h : ¬3 < a'), is_false _))
         (λ (H : ∃ (a : ℕ), a ≥ 4 ∧ a ∈ m), is_true _)
         b) ==
    decidable.rec
      (λ (H : ¬∃ (a_1 : ℕ), a_1 ≥ 4 ∧ a_1 ∈ a :: m),
         dite (3 < a') (λ (h : 3 < a'), is_true _) (λ (h : ¬3 < a'), is_false _))
      (λ (H : ∃ (a_1 : ℕ), a_1 ≥ 4 ∧ a_1 ∈ a :: m), is_true _)
      (decidable.rec
         (λ (H : ¬∃ (a : ℕ), a ≥ 4 ∧ a ∈ m),
            dite (3 < a) (λ (h : 3 < a), is_true _) (λ (h : ¬3 < a), is_false _))
         (λ (H : ∃ (a : ℕ), a ≥ 4 ∧ a ∈ m), is_true _)
         b)

[Kevin Buzzard]

I assume I'm doing something wrong.

[Kenny Lau]

I think there might be some lemmas that one could use

[Kenny Lau]

bounded existential

[Kevin Buzzard]

Isn't membership in multisets decidable? You combine that fact with decidability of existentials on finite ranges

example (D : multiset ℕ) (d : ℕ) : decidable (d ∈ D) := by apply_instance works

[Kenny Lau]

@Kevin Buzzard shouldn't you be watching the world cup?

[Kevin Buzzard]

Oh, has it started?

[Kenny Lau]

:o

[Kenny Lau]

it's already 67 minutes

[Simon Hudon]

You can try this:

instance {α : Sort*} (P : α → Prop) (C : multiset α) : decidable (∃ a ∈ C, P a) :=
sorry

example (C : multiset ℕ) : decidable (∃ a : ℕ, a ≥ 4 ∧ a ∈ C) :=
suffices this : decidable (∃ a ∈ C, a ≥ 4),
by { resetI, apply @decidable_of_iff _ _ _ this, apply exists_congr, intro, tauto },
by { apply_instance }

[Kenny Lau]

well you want P to be decidable

[Simon Hudon]

Yes, that's right

[Kevin Buzzard]

I don't understand how to use this code. If I comment out the instance then there's an error in the final apply_instance but if I look at what needs to be proved at that point it seems to be decidable (∃ (a : ℕ) (H : a ∈ C), a ≥ 4) which is exactly my question I think?

[Simon Hudon]

Ok, one second I'm filling in that instance

[Chris Hughes]

Add this before Simon'd code

instance decidable_exists_multiset {α : Type*} (s : multiset α) (p : α → Prop) [decidable_pred p] :
  decidable (∃ x ∈ s, p x) := quotient.rec_on s
list.decidable_exists_mem (λ a b h, subsingleton.elim _ _)

[Simon Hudon]

Nice! that's better than what I have

[Simon Hudon]

It would be worth pushing to mathlib I think along with a finset counterpart and decidable universals for both

[Chris Hughes]

Will do.

[Simon Hudon]

Thanks!

[Kevin Buzzard]

Thanks to both of you! I cannot believe how much trouble Ellen's dots and boxes project is causing me :-)

[Simon Hudon]

What's that project?

[Kevin Buzzard]

She's formalizing some of the theory of dots and boxes