failed to synthesize Decidable

Stream: lean4

[Alexandre Rademaker]

Given these simple definitions

structure Person where
  name : String
  age : Nat
 deriving Repr

instance : Ord Person where
  compare p q := compare p.age q.age

instance : LT Person where
  lt p q := LT.lt p.age q.age

def people := [
  Person.mk "Alice" 23,
  Person.mk "Bob" 25,
  Person.mk "Eve" 22]

#eval compare people[0] people[1]
#eval people[0] < people[1]  -- <-- ERROR

The error is

failed to synthesize
  Decidable (people[0] < people[1])

So ordering works as expected. Why the LT instance for Person is not enough? How to show that lt for Person is decidable?

[Daniel Weber]

docs#LT is Prop valued, which doesn't have computational content, while docs#Ord is docs#Ordering valued, which does

[Daniel Weber]

You should also use a < b instead of LT.lt a b

[Daniel Weber]

For the decidability you should be able to do (untested)

instance (a b : Person) : Decidable (a < b) := inferInstanceAs (Decidable (a.age < b.age))

[Alexandre Rademaker]

It indeed worked! Fantastic! But...

structure Person where
  name : String
  age : Nat
 deriving Repr

instance : Ord Person where
  compare p q := compare p.age q.age

instance : LT Person where
  lt a b := a.age < b.age

instance (a b : Person) : Decidable (a < b) :=
  inferInstanceAs (Decidable (a.age < b.age))

what is the difference between the syntax instance : ... where ... and instance : ... := ...? The inferInstanceAs is still confusing to me.. but I may have to think deeper.

[Kyle Miller]

where ... is the same as := { ... }

[Kyle Miller]

For example you could have written

instance : LT Person :=
  { lt a b := a.age < b.age }

though on a less-recent Lean you have to write that as

instance : LT Person :=
  { lt := fun a b => a.age < b.age }

[Alexandre Rademaker]

I was trying with ⟨ ⟩ , so it uses the structure notation.. not the constructor. Using "4.14.0-rc3"

[Kyle Miller]

Yes, for structures it's generally better to use this "structure instance notation". Using a structure's constructor directly won't make use of default field values for example, and if you use extends it exposes internal details for how the structure is represented.