A small question about type class

Stream: new members

[Yuzhi LIU]

I'm currently studying the book Theorem Proving in Lean 4. After studying the chapter on typeclasses, I wanted to find some examples in Mathlib. However, the following is confusing for me. I can understand code like this:

variable {p : Prop} [Decidable p] {a b : ℤ}

But I have a little difficulty explaining what this means:

variable {r : α → β → Prop} [∀ a, DecidablePred (r a)] {s : Finset α} {t : Finset β}

I wonder if "[∀ a, DecidablePred (r a)]" is definitionally equal to "[DecidablePred (∀ a, r a)]". Also, can the latter compile? Why do we stick to the first representation?

I'd be very grateful to anyone who can help me!

[Lawrence Wu (llllvvuu)]

(deleted)

[Lawrence Wu (llllvvuu)]

(deleted)

[Lawrence Wu (llllvvuu)]

(deleted)

[Lawrence Wu (llllvvuu)]

Ah, r is a relation. Then they should both compile, but won’t be semantically equal.

[Riccardo Brasca]

DecidablePred (∀ a, r a) I think doesn't work, since r a is of type β → Prop.

[Yuzhi LIU]

Great, thanks to both of you @Lawrence Wu (llllvvuu) @Riccardo Brasca ! So what if I change my question to this:

variable {r: α → Prop} [∀ a, Decidable (r a)]

and

variable {r: α → Prop} [Decidable (∀ a, r a)]

Since now both(r a) and(∀ a, r a)have type Prop, they should both compile? Also, I didn't really get why they are not semantically equal :sob:

[Ruben Van de Velde]

I think there's a difference when alpha is infinite. If you have an algorithm that will tell you whether p n is true for any specific natural number, for example, an algorithm to check whether it's true for all natural numbers would need to check an infinite number of cases

[Ruben Van de Velde]

In the other direction, if you have an algorithm that tells you whether something is true for all numbers - if it says yes, you know the answer for your specific number; but it is says no, you don't know if it fails for your number or another one

[Yuzhi LIU]

@Ruben Van de Velde Thank you so much!

[Aaron Liu]

Yuzhi LIU said:

Great, thanks to both of you Lawrence Wu (llllvvuu) Riccardo Brasca ! So what if I change my question to this:

variable {r: α → Prop} [∀ a, Decidable (r a)]

and

variable {r: α → Prop} [Decidable (∀ a, r a)]

Since now both(r a) and(∀ a, r a)have type Prop, they should both compile? Also, I didn't really get why they are not semantically equal :sob:

the difference between "I have an algorithm to test r on any input" and "I can tell you if r is always true or if it's sometimes false"

[Riccardo Brasca]

The question is maybe why do you think they're equal.