missing Decidable instances

Stream: mathlib4

[Yury G. Kudryashov]

I've just noticed that we don't have Lean 4 versions of at least the following Decidable instances:

• docs#list.decidable_ball
• docs#list.decidable_bex
• decidability for Subset on Lists (not in mathlib3 either).

The easiest way to prove them is to use docs4#List.all_iff_forall_prop. Is this the right place or they should proved in a way that can be moved to Std?

[Mario Carneiro]

I thought these were in std already

[Mario Carneiro]

docs4#List.decidableBEx, docs4#List.decidableBAll

[Mario Carneiro]

The easiest way to prove them is to use docs4#List.all_iff_forall_prop. Is this the right place or they should proved in a way that can be moved to Std?

List.all_iff_forall_prop can definitely be moved to std

[Yury G. Kudryashov]

How do I make PRs to Std?

[Yury G. Kudryashov]

I want to add Decidable for Subset on Lists.

[Mario Carneiro]

it's a normal github project

[Mario Carneiro]

PR from a fork

[Andrej Bauer]

Is there already a way to convince the machine that ∀(k : Fin n), p k is decidable if p : Fin n → Prop is decidable? If not, what's the idiomatic way to go about it? Add an instance of Decidable (having instances for compound expressions looks scary to me)?

[Eric Wieser]

That instance should already be in mathlib

[Eric Wieser]

@loogle Decidable, Fintype, "forall"

[Eric Wieser]

@loogle Decidable, Fintype, "forall"

[loogle]

:search: Fintype.decidableForallFintype

[Andrej Bauer]

import Lean
theorem foo : ∀ (k : Fin 6), k = k := by decide

gives me failed to synthesize Decidable (∀ (k : Fin 6), k = k). So I am doing something wrong, a missing import perhaps?

[Sebastien Gouezel]

As you can see in the link given by loogle, the instance you want to use is defined in Mathlib.Data.Fintype.Basic, so you should import this file.

[Kevin Buzzard]

If in doubt, import Mathlib

[Eric Wieser]

import Lean is fairly useless; this means roughly "I am going to augment the lean compiler/syntax in some way", not "I am going to write a program/proof in lean"

[Eric Wieser]

(for which import Std/import Mathlib are respectively reasonable choices)

[Andrej Bauer]

Kevin Buzzard said:

If in doubt, import Mathlib

Still getting used to the difference between import Lean and import Mathlib.

[Antoine Chambert-Loir]

Kevin Buzzard said:

If in doubt, import Mathlib

What does it cost (in terms of speed or energy) to do so?

[Kevin Buzzard]

In lean 3 -- a lot. In lean 4 very little.