Default alternative

Stream: new members

[Nicolò Cavalleri]

I want to define a map which takes certain values on a set of a type and takes garbage values on the complementary of the set. Is there a way to do this without requiring the target type to be inhabited and sending terms in the complementary of the set on the default term? I'd like to do this without requiring additional type classes

[Kevin Buzzard]

What if the set and the target type are both empty?

[Nicolò Cavalleri]

You're right, sorry, I missed an important detail. I am in the following situation: the domain is inhabited iff the codomain is.

[Nicolò Cavalleri]

The domain is the base space of a vector bundle and the codomain is the total space

[Eric Wieser]

You can always use if nonempty domain then (assume x, sorry) else false.elim sorry as your (noncomputable) implementation

[Nicolò Cavalleri]

What is the difference between inhabited and nonempty?

[Eric Wieser]

The former is in Type u, the latter is in Prop

[Eric Wieser]

docs#ite requires a prop

[Nicolò Cavalleri]

Ok thanks!

[Nicolò Cavalleri]

I can see there is nonempty_of_inhabited but is there any inhabited_of_nonempty?

[Eric Wieser]

Theres tactic#inhabit

[Eric Wieser]

But also, it's very rare to need what you're asking for. If you have h: nonempty T instead of h : inhabited T, you can use docs#classical.choice instead of docs#default.

[Nicolò Cavalleri]

Ok thanks! Also it tells me that it cannot synthesize an instance for decidable (nonempty B) B is just a Type. Is this normal?

[Nicolò Cavalleri]

I guess I'll need to do

open classical
local attribute [instance] prop_decidable

[Anne Baanen]

Exactly, or you can write open_locale classical to do so in one line.

[Anne Baanen]

Some more details: The reason we distinguish between inhabited X and nonempty X is that the former is strictly stronger intuitionistically: a term in inhabited X points to a specific element of X, while a term in nonempty X shows that it is contradictory to assume there are no elements of X at all. So going from inhabited X to X is easy, while going from nonempty X to X is not computable.

For example, for the type X of all x : ℕ such that either x = 0 and the Riemann hypothesis doesn't hold, or x = 1 and the Riemann hypothesis holds, it's very difficult to give an example of X, while it's easy to show that X cannot be empty.

[Anne Baanen]

Nicolò Cavalleri said:

Ok thanks! Also it tells me that it cannot synthesize an instance for decidable (nonempty B) B is just a Type. Is this normal?

Yes, nonempty is not in general decidable. Consider for example the type X containing all valid proofs of the Riemann hypothesis. Determining whether this type is empty is at least as hard as proving or disproving RH.

[Nicolò Cavalleri]

@Anne Baanen thank you very much for this explanation