failed to synthesize instance DecidableEq Point

Stream: new members

[abdullah uyu]

variable {Point : Type}
variable {collinear : Point -> Point -> Point -> Prop}

def line (a b : Point) := if a ≠ b then {c : Point // collinear a b c} else {c : Point // c = a}

I get:

failed to synthesize instance
  DecidableEq Point

So I understand that I have to tell to lean that the equality of two points is decidable. How can I do that?

[Riccardo Brasca]

Does adding [DecidableEq Point] work?

[abdullah uyu]

Oh, before the :=, of course! I'm not sure what that did, though. Does that mean that whenever I want to construct the line passing through $a$ and $b$, I also have to provide that I can decide whether if $a$ and $b$ are equal?

[Eric Wieser]

What you have looks like it would be pretty awkward to me; I think you'd have a much better time with

abbrev line (a b : Point) : Set Point := {c : Point | if a = b then c = a else collinear a b c}

[Eric Wieser]

Or:

abbrev line (a b : Point) : Set Point := {c : Point | (a = b ∧ c = a) ∨ (a ≠ b ∧ collinear a b c)}

[Eric Wieser]

Another option would be

inductive IsOnLine : Point → Point → Point → Prop where
| refl : IsOnLine a a a
| between (a b c : Point) (h : a ≠ b) (h : collinear a b c) : IsOnLine a b c

[abdullah uyu]

Well, those make a lot more sense, yes.

[abdullah uyu]

Although, with those I get : unknown identifier 'Set', is Set a lean3 thing, or do I have to import something?

[Ruben Van de Velde]

No, Set is lean 4, but you might need some imports

[abdullah uyu]

Eric Wieser said:

What you have looks like it would be pretty awkward to me; I think you'd have a much better time with

abbrev line (a b : Point) : Set Point := {c : Point | if a = b then c = a else collinear a b c}

So to use Set, I do import Mathlib.Data.Set.Basic. But the error persists, do you mean

abbrev line (a b : Point) [DecidableEq Point] : Set Point := {c : Point | if a = b then c = a else collinear a b c}

But even with that, when I try to state the theorem $a \in \operatorname{line}(a, b)$ with

theorem constructor_inside (a b : Point) [DecidableEq Point] [Membership Point Type] : a ∈ line a b := by
sorry

I get:

don't know how to synthesize implicit argument
  @line Point (?m.690 a b) a b fun a b ↦ inst¹ a b
context:
Point : Type
collinear : Point → Point → Point → Prop
a b a b : Point
inst¹ : DecidableEq Point
inst : Membership Point Type
⊢ Point → Point → Point → Prop
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

which I think is more obscure than the previous error.

[Eric Wieser]

You'd get that error anyway, it's not caused by my change. It's telling you that lean can't work out collinear

[Eric Wieser]

Eric Wieser said:

Or:

abbrev line (a b : Point) : Set Point := {c : Point | (a = b ∧ c = a) ∨ (a ≠ b ∧ collinear a b c)}

This version does not need DecidableEq

[Kyle Miller]

I wonder -- do you need whether a = b in the definition of a line? It seems like theorems will need a ≠ b assumptions anyway, so what does ensuring line a a is a single point helpful for?

[abdullah uyu]

Eric Wieser said:

You'd get that error anyway, it's not caused by my change. It's telling you that lean can't work out collinear

Yep, I realized that after I posted my response. Not sure I get what does it want from me, though.

[abdullah uyu]

Kyle Miller said:

I wonder -- do you need whether a = b in the definition of a line? It seems like theorems will need a ≠ b assumptions anyway, so what does ensuring line a a is a single point helpful for?

Maybe. I blindfold transcribed the definition in the book, for the sake of an exercise.

[abdullah uyu]

Making collinear explicit seems to solve it. But I presume there is way to tell this to Lean in an elegant way.

[Eric Wieser]

If for any P there is a canonical interpretation of "collinear", you could use

class HasCollinear (P : Type) where
   Collinear : P → P → P → Prop

export HasCollinear Collinear

variables {Point : Type} [HasCollinear P]

And then Collinear a b c will find the right version of colinearity automatically