inductive type with anonymous constructors

Stream: new members

[Vaibhav Karve]

I want to translate the following English sentence into Lean:
"An extended bool is either a value called extra or a boolean value".

Normally I would do it by typing

inductive extended_bool : Type
| extra   : extended_bool
| boolean : bool → extended_bool

However, this means that when working with extended bool, I always need to destruct it and include the boolean constructor for the boolean case. Can I save myself some work by having an "anonymous" constructor? Is this considered bad coding practice?

[Mario Carneiro]

That looks like option bool to me

[Mario Carneiro]

Anonymous constructors unfortunately only work for types with one constructor

[Vaibhav Karve]

But even with option, don't I have to use some and none? I wanted some way to say "if it is not extra, then it must be boolean, so I am not going to write it."

Another example might be bool ⊕ nat. Is there a way for me to define functions on this type without constantly making references to sum.inl and sum.inr? As in, can Lean infer the definition of the function simply from the type of the arguments?

[Patrick Massot]

You can define a coercion from bool to extended_bool

[Patrick Massot]

def ebool := option bool

instance : has_coe bool ebool := ⟨λ b, some b⟩

variable f : ebool → ebool

#check f tt
#check f none

[Patrick Massot]

Is that what you want?

[Patrick Massot]

In case this is not clear, option bool without wrapping it already gives you that.

[Mario Carneiro]

option actually already has such a coercion

[Mario Carneiro]

(oops, patrick already said this)

[Mario Carneiro]

This will work in cases like bool ⊕ nat, with type based dispatch, but it won't work in patterns (i.e. pattern matching requires explicit inl and inr). But I don't think it is good style, and the option coe is rarely used in mathlib

[Vaibhav Karve]

@Patrick Massot yes, that is what I was looking for. That's a cool trick with has_coe.
@Mario Carneiro Yes, I can see how this can lead to smelly code. I'll try and avoid this kind of usage in practice.

For the case of bool ⊕ nat, do I still need explicit coercion? I am not sure I understand what you mean by type-based-dispatch. So far I have:

def ebool := bool ⊕ nat

def f : ebool → nat   -- throws an error
| tt := 1
| ff := 0
| n  := n

How can I define that f properly?

[Mario Carneiro]

like I said, it won't work in patterns

[Mario Carneiro]

def ebool := bool ⊕ nat

instance coe_l : has_coe bool ebool := ⟨sum.inl⟩
instance coe_r : has_coe nat ebool := ⟨sum.inr⟩

example : ebool := tt
example : ebool := ff
example (n : nat) : ebool := n

[Mario Carneiro]

Oh, it looks like this works too:

def f : ebool → nat
| tt := 1
| ff := 0
| (n : ℕ) := n

[Vaibhav Karve]

Oh, that's just perfect! Thanks. :+1: