Classes and instances

Stream: new members

[Roy Shmueli]

Hi, I'm trying to learn the use of classes in lean3. But I get a "failed to synthesize" error.

import algebra.order.field.basic

noncomputable theory

constant R : Type

@[instance] axiom P_is_poset : linear_ordered_field R

namespace my

def Icc (a b : R) : set R := {x | a ≤ x ∧ x ≤ b}

@[class] def has_max (A : set R) := ∃ b : R, b ∈ A ∧ ∀ x ∈ A, x ≤ b
def max (A : set R) [h : has_max A] := classical.some h

instance icc_has_max {a b : R} (h : a < b) : has_max (Icc a b) := sorry

@[simp] lemma icc_max {a b : R} (h : a < b) : max (Icc a b) = b := sorry
-- failed to synthesize type class instance for

example : has_max (Icc 0 1) := sorry

end my

I tried defining Icc in the following way

def Icc {a b : P} (h : a < b) := ...

But then simple props such as has_max (Icc 0 1) becomes complicated to write.

I was wondering what do you think is the best way to fix this?

[Yaël Dillies]

You cut the error right before the interesting bit!

[Yaël Dillies]

What is the line after "failed to synthesize typeclass instance for"?

[Yaël Dillies]

But here I know the answer directly: Your icc_has_max instance can't be used by typeclass inference (the mechanism that finds the instances) because it has an argument a < b which is not a class.

[Yaël Dillies]

There are two solutions: Either make < a class (bad idea, I can tell you), or replace (h : a < b) by [fact (a < b)] where docs#fact wraps any proposition you want into a typeclass.

[Roy Shmueli]

Thank you, it was exactly what I was looking for.
About the error, my vs code displays only that part of the error message, is it a bug?
image.png

[Kevin Buzzard]

Your VS Code is displaying all of the error message right there in the right hand pane. The key part you didn't tell us was has_max (Icc a b) (but Yael worked this out anyway)

[Kevin Buzzard]

A much better way to put the assumption that R is a linearly ordered field into the system is variable [linear_ordered_field R] BTW