13
$\begingroup$

In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes are very similar - you can instantiate either of them given an element of the type. In what situations do you use one over the other?

$\endgroup$
4
  • 3
    $\begingroup$ I find the Lean terminology confusing. In my world it is: nonempty A means $A \to \emptyset$; inhabited A means $\exists x \in A . \top$; and pointed means $\Sigma_{A : \mathsf{Type}} A$, or in fibered form pointed A means $A$. $\endgroup$ Apr 16, 2022 at 7:25
  • 1
    $\begingroup$ @Andrej Bauer, Lean calls $A → ∅$ is_empty A, which seems like the opposite of the meaning you're suggesting. Do you really use "nonempty" to mean "has no elements"? $\endgroup$
    – Eric
    Apr 16, 2022 at 7:51
  • 2
    $\begingroup$ Ah yes, sorry about that, I've just returned from England. I should have $(A \to \emptyset) \to \emptyset$, or equivalently $\neg\neg \exists x \in A . \top$. $\endgroup$ Apr 16, 2022 at 8:01
  • $\begingroup$ @Guy Coder: the relevant lines of the files you link to (both Lean 3, just different versions of it) are equivalent if not identical, so the distinction isn't important. $\endgroup$
    – Eric
    Apr 16, 2022 at 19:22

1 Answer 1

15
$\begingroup$

The difference between nonempty and inhabited is that nonempty A : Prop but inhabited A : Sort (max 1 u) (if A : Sort u). This makes inhabited A isomorphic as a type to A, while nonempty A is the propositional truncation of A, equivalent to ∃ x : A, true. To extract a value from inhabited A is inhabited.default, but extracting a value from a proof of nonempty A is the axiom of choice and is noncomputable.

Generally, you should use nonempty A if you only need the "mere fact" that A is not empty, while inhabited A is used if you need to access a specific default value for totalizing a function or so. Mathlib has a linter to ensure that you don't use inhabited in place of nonempty for proving theorems unless you need it in the statement of the theorem.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.