## Stream: new members

### Topic: an exercise in documentation

#### Trapped Beast (Jun 28 2023 at 07:53):

I'm new to Lean and I'm a bit confused when I come across an exercise while reading the official documentation of Lean 4. :sob: :sob:
Here is the exercise:
Using the analogy between types and arithmetic, write a function that turns multiplication by two into a sum. In other words, it should have type Bool × α → α ⊕ α.
What puzzles me the most is why there is a Bool in the type.

#### Notification Bot (Jun 28 2023 at 07:54):

Trapped Beast has marked this topic as resolved.

#### Notification Bot (Jun 28 2023 at 07:55):

Trapped Beast has marked this topic as unresolved.

#### Scott Morrison (Jun 28 2023 at 08:20):

Bool is a type with two terms.

#### Scott Morrison (Jun 28 2023 at 08:21):

(Mesopotamian shepherds discovered decategorification (=replacing things with their isomorphism classes, aka counting), but categorification (=coming up with an interesting element from the isomorphism class, aka as deciding that Bool is the best type with two terms) remains difficult.)

#### Notification Bot (Jun 28 2023 at 08:22):

2 messages were moved here from #new members > Minkowski space and hyperbolic geometry by Johan Commelin.

#### Trapped Beast (Jul 02 2023 at 07:38):

Scott Morrison said:

Bool is a type with two terms.

I understand a little bit, but can you give a specific answer to this question? Thank you so much. :rose:

#### Mario Carneiro (Jul 02 2023 at 07:51):

what is the question?

#### Mario Carneiro (Jul 02 2023 at 07:52):

do you understand what the possible terms of Bool × α are? And the possible terms of α ⊕ α?

#### Trapped Beast (Jul 06 2023 at 13:07):

Mario Carneiro said:

what is the question?

The question is ：Using the analogy between types and arithmetic, write a function that turns multiplication by two into a sum. In other words, it should have type Bool × α → α ⊕ α.

#### Trapped Beast (Jul 06 2023 at 13:14):

Mario Carneiro said:

do you understand what the possible terms of Bool × α are? And the possible terms of α ⊕ α?

Yes，I think I have understood the concept of prod and sum type.

#### Trapped Beast (Jul 06 2023 at 13:19):

Mario Carneiro said:

what is the question?

Can you just give me a meaningful function whose type is Bool × α → α ⊕ α? Thanks a lot.

#### Johan Commelin (Jul 06 2023 at 13:21):

Can you just explain what you have tried so far?

#### Johan Commelin (Jul 06 2023 at 13:21):

How do you define a function in Lean?

#### Mario Carneiro (Jul 06 2023 at 13:23):

Trapped Beast said:

Mario Carneiro said:

do you understand what the possible terms of Bool × α are? And the possible terms of α ⊕ α?

Yes，I think I have understood the concept of prod and sum type.

That wasn't the question. Suppose a : α. Can you give something whose type is Bool × α?

#### Trapped Beast (Jul 06 2023 at 13:25):

Johan Commelin said:

Can you just explain what you have tried so far?

There is a similar question in the document: Using the analogy between types and arithmetic, write a function that distributes products over sums. In other words, it should have type α × (β ⊕ γ) → (α × β) ⊕ (α × γ).

My definition is as follows：
def mulToSum {α β γ : Type} (ori : α × (β ⊕ γ)) : (α × β) ⊕ (α × γ) :=
match ori with
| (a,Sum.inl b) => Sum.inl (a,b)
| (a,Sum.inr c) => Sum.inr (a,c)

I just can't image a function whose type is Bool × α → α ⊕ α.

#### Johan Commelin (Jul 06 2023 at 13:29):

Why don't you try writing a similar match expression?

#### Johan Commelin (Jul 06 2023 at 13:30):

Please post your best attempt at writing that function. You can use #backticks (check this link :wink:) to format code on zulip.

#### Trapped Beast (Jul 06 2023 at 13:35):

I tried the following:

def mulIsSum {α:Type} (mul:Bool) (val:α) : α ⊕ α :=
match mul with
| true => Sum.inl val
| false => Sum.inr val


But unlike α × (β ⊕ γ) → (α × β) ⊕ (α × γ), I couldn't find a realistic example for this function.Especially,how can such a function represent "turns multiplication by two into a sum"?

#### Johan Commelin (Jul 06 2023 at 13:36):

This isn't exactly the type that you were given in the question...

#### Johan Commelin (Jul 06 2023 at 13:38):

Do you see how α × (β ⊕ γ) → (α × β) ⊕ (α × γ) looks very similar to a * (b + c) = (a * b) + (a * c)?

In the same way Bool × α → α ⊕ α looks very similar to 2 * a = a + a.

#### Matthew Ballard (Jul 06 2023 at 13:38):

Compare Bool to Unit ⊕ Unit

#### Johan Commelin (Jul 06 2023 at 13:38):

That's all that this question is trying to teach you.

#### Trapped Beast (Jul 06 2023 at 13:39):

Johan Commelin said:

This isn't exactly the type that you were given in the question...

Ah, I was wrong. Sorry for wasting your time. :sob:

#### Trapped Beast (Jul 06 2023 at 13:51):

Johan Commelin said:

Do you see how α × (β ⊕ γ) → (α × β) ⊕ (α × γ) looks very similar to a * (b + c) = (a * b) + (a * c)?

In the same way Bool × α → α ⊕ α looks very similar to 2 * a = a + a.

Thanks again, I understand this time.

Last updated: Dec 20 2023 at 11:08 UTC