LE Prop vs Bool

Stream: new members

[Burkhardt Renz]

I' am confused:

#check 2 ≤ 3 -- Prop
#eval [1, 3, 5].filter (· ≤ 3) -- [1, 3]

but

def myle [LE α] : α → α → Bool :=
    λ x y => x ≤ y

is a type mismatch

type mismatch
  x ≤ y
has type
  Prop : Type
but is expected to have type
  Bool : Type

I thought that LE is Decidable and therefore Prop is automatically coerced to Bool if needed??

[Eric Wieser]

Burkhardt Renz said:

I thought that LE is Decidable

In general it's not. Your first example only shows it is decidable on Nat.

[suhr]

def myle [LE α][DecidableLE α] : α → α → Bool :=
  λ x y => x ≤ y

[Burkhardt Renz]

Which type class should I use, when I want to compare Nats, Ints, Strings and so on?

With

def myle [LE α] [DecidableLE α] : α → α → Bool :=
    λ x y => x ≤ y

I get

invalid binder annotation, type is not a class instance
  ?m.5185

[Ruben Van de Velde]

Try turning on autoImplicit errors

[Eric Wieser]

(set_option autoImplicit false)

[Burkhardt Renz]

I didn't manage to define the function using typeclass LE

My solution now:

def myle {α : Type} [Ord α] : α → α → Bool :=
    λ x y => if Ordering.isLE (compare x y) then true else false

What do you think about that approach?

[Aaron Liu]

It's fine, but you won't be able to compare Floats.

#synth Ord Float

[Ruben Van de Velde]

What is your goal?

[Burkhardt Renz]

My goal is a version of Quicksort that works for all reasonable types, not just Int or Nat
I have a version of Quicksort for Int together with a proof of termination.

[Kevin Buzzard]

Then why not just assume DecidableLE?

[Aaron Liu]

That's docs#DecidableLE

[Aaron Liu]

You can also try writing decide explicitly

[Burkhardt Renz]

`DecidableLe':

def myle [DecidableLe α] : α → α → Bool :=
  λ x y => x ≤ y

error:

invalid binder annotation, type is not a class instance
  ?m.6720

[Aaron Liu]

Your code from above is working fine for me. Can you try putting set_option autoImplicit false at the top of the file, right after all the imports?

Burkhardt Renz said:

With

def myle [LE α] [DecidableLE α] : α → α → Bool :=
    λ x y => x ≤ y

I get

invalid binder annotation, type is not a class instance
  ?m.5185

[Kevin Buzzard]

Sorry, DecidableLE not DecidableLe. You've run into the autoImplicit footgun.

[Eric Wieser]

Eric Wieser said:

(set_option autoImplicit false)

Please add this line to your code that we suggested earlier

[Burkhardt Renz]

I tried with

set_option autoImplicit false

but I get the same error message

I use Lean Version 4.15.0

In Lean 4 Web there is no error message. I try to update Lean.

[Eric Wieser]

Yes, your lean version is probably the issue

[Eric Wieser]

Burkhardt Renz said:

but I get the same error message

Are you sure? I would expect a different error message

[Kevin Buzzard]

@Burkhardt Renz can you please post a #mwe so we are all on the same page?

[Aaron Liu]

It looks like DecidableLE was only added 2 months ago. You can use DecidableRel (LE.le : α → α → Prop) instead.

[Burkhardt Renz]

Sorry for the trouble, and thanks for your help

In the future I will check first on Lean 4 Web!

I updated Lean to Lake version 5.0.0-93d4ae6 (Lean version 4.17.0-rc1)and th problem is gone. I even don't need the autoImplicit option:

def myle {α : Type} [LE α] [DecidableLE α] : α → α → Bool :=
    λ x y => x ≤ y

#eval myle 2 3 -- true
#eval myle 'a' 'z' -- true
#eval myle "aa" "aaa" -- true
#eval myle "b" "aaa" -- false
#eval myle 5.0 4.2 --.false
`` `

[Kevin Buzzard]

The autoImplicit option is just to prevent people from getting confusing errors if they make typos :-)