Some confusion in ⟨⟩ notion and Nonempty α

Stream: new members

[Shanghe Chen]

Hi! In TPIL §.Axioms and Computation. There is

noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
(h :∃ x, p x) : {x // p x} :=
choice <| let ⟨x, px⟩ := h; ⟨x, px⟩

and

theorem inahbited_of_nonempty : Nonempty α → Inhabited α
| h => choice (let ⟨a⟩ := h; ⟨⟨a⟩⟩)

Why does the first snippet use only one ⟨⟩ notation but the second requires ⟨⟨⟩⟩ ?
I think in the first that ⟨⟩ is used for constructor of the subtype {x // p x}:

variable (p : α → Prop)
variable (x : α)
variable (h : p x)
def y : {x // p x} := ⟨x, h⟩

But Nonempty not require ⟨⟩? I checked that

noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
                                        (h :∃ x, p x) : {x // p x} :=
  choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩

also works.

[Shanghe Chen]

Is there some implicit coersion define for Nonemtpy α but not Inhabited α?

[Shanghe Chen]

the definition for Nonemtpy α and Inhabited α is

class inductive Nonempty (α : Sort u) : Prop where
|intro (val : α) : Nonempty α

class Inhabited (α: Sort u) where
    default : α

May be some difference of the syntax related to this?

[Mario Carneiro]

In the second example we have a : A and are proving Nonempty (Inhabited A)

[Mario Carneiro]

This is because after applying choice the goal went from Inhabited A to Nonempty (Inhabited A)

[Mario Carneiro]

so we need to apply two constructors in a row

[Mario Carneiro]

The proof could alternatively be written as

theorem inhabited_of_nonempty : Nonempty α → Inhabited α
| h => ⟨choice (let ⟨a⟩ := h; ⟨a⟩)⟩

which is to say, unwrap the Inhabited before applying choice so that the goal is Nonempty A instead... but at that point the let is just unwrapping Nonempty and wrapping it back up so you can simplify it to just

theorem inhabited_of_nonempty : Nonempty α → Inhabited α
| h => ⟨choice h⟩

[Shanghe Chen]

Thank you for the alternative proof. It's much more cleaner. I got that there should be two constructor. I am wondering why def z works in the the following snippet where one constructor is omit

variable (p : α → Prop)
variable (x : α)
variable (h : p x)
def y : {x // p x} := ⟨x, h⟩
def u : Nonempty {x // p x} := ⟨⟨x, h⟩⟩
def z : Nonempty {x // p x} := ⟨x, h⟩ -- work too, but why one ⟨⟩ omit?
def v : Nonempty (Inhabited α) := ⟨⟨x⟩⟩
-- def w : Nonempty (Inhabited α) := ⟨x⟩ -- not work

[Shanghe Chen]

Oh

def s : Inhabited {x // p x} := ⟨x, h⟩
def t : Inhabited {x // p x} := ⟨⟨x, h⟩⟩

both work too. It should relate to soemthing about the subtype

[Mario Carneiro]

Oh but actually there is some additional magic which my post doesn't explain, in the first snippet. By similar reasoning we would expect that ⟨x, px⟩ is being used to construct Nonempty {x // p x} and hence we would need double brackets, and indeed ⟨⟨x, px⟩⟩ works. But the magic is that when you use the anonymous constructor brackets with n arguments when the constructor only has m < n, it uses the first m-1 of them for the constructor directly and recursively uses the remaining n-(m-1) as another anonymous constructor for the last argument. This is particularly useful when using ⟨ha, hb, hc, hd⟩ as shorthand syntax for ⟨ha, ⟨hb, ⟨hc, hd⟩⟩⟩ when inhabiting a ∧ b ∧ c ∧ d (which is actually a ∧ (b ∧ (c ∧ d)))

[Mario Carneiro]

In this (kind of degenerate) case we get that since ⟨x, px⟩ has 2 arguments and Nonempty expects 1, we use the first 0 of them for Nonempty, recurse with ⟨x, px⟩ to construct a {x // p x} and then pass the result as the last argument to Nonempty, i.e. we get ⟨⟨x, px⟩⟩

[Shanghe Chen]

Yeah very clean now. Thank you Mario :tada: