exists unique

Stream: lean4

[Aron]

Henrik Böving suggested this definition for exunique:

def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

Trying to apply it is causing problems - in this case I'm trying to translate a problem from incidence geometry to lean4.

def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

class incidence (point line: Type) (inc:point → line → Prop) :=
(one:∀ P Q, P ≠ Q → exunique (l:line) (inc P l ∧ inc Q l))

application type mismatch
  exunique l
argument
  l
has type
  line : Type
but is expected to have type
  ?m.93 → Prop : Sort (max 1 ?u.92)

[Sébastien Michelland]

The exunique quantifier does not have special syntax, so if you want to use it directly you need to write p: α → Prop directly as a function.

class incidence (point line: Type) (inc:point → line → Prop) :=
(one:∀ P Q, P ≠ Q → exunique (fun l => inc P l ∧ inc Q l))

I'm not too comfortable with notation, but this could do the trick.

syntax "∃!" term "," term: term
macro_rules
  | `(∃! $t:term, $p:term) => `(exunique (fun $t => $p))

class incidence2 (point line: Type) (inc:point → line → Prop) :=
(one:∀ P Q, P ≠ Q → ∃! (l:line), (inc P l ∧ inc Q l))