3
$\begingroup$

I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then complained

The following `inhabited` instances should be `nonempty`. argument 2: [_inst_3 : inhabited ι]

I can change the types as suggested, but what do I do with the arbitrary ι expression in my proofs?

$\endgroup$

2 Answers 2

10
$\begingroup$

What you're seeing here is the behavior of the inhabited_nonempty linter:

import tactic

lemma foo {α} [inhabited α] : ∃ x : α, x = x :=
begin
  exact ⟨default, rfl⟩
end

#lint only inhabited_nonempty
/- Checking 1 declarations (plus 1 automatically generated ones) in the current file with 1 linters -/

/- The `inhabited_nonempty` linter reports: -/
/- USES OF `inhabited` SHOULD BE REPLACED WITH `nonempty`. -/

You can use the inhabit tactic to solve this problem

import tactic

lemma foo {α} [nonempty α] : ∃ x : α, x = x :=
begin
  inhabit α,
  exact ⟨default, rfl⟩
end

#lint only inhabited_nonempty  -- All linting checks passed!

Note this has the advantage over classical.arbitrary of not introducing the axiom of choice:

#print axioms foo  -- no axioms

while being less cumbersome than the nonempty.elim ‹nonempty α› $ λ a, suggested in the other answer.

$\endgroup$
0
6
$\begingroup$

The most convenient option is classical.arbitrary (or nonempty.some if your nonempty α is an explicit ssumption rather than an instance one).

Note that this is exactly the axiom of choice. If your target is Prop, you can get away without using choice by writing something like nonempty.elim ‹nonempty α› $ λ a, the_rest_of_your_proof, which is arguably a bit cumbersome.

$\endgroup$

Your Answer

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

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