# Zulip Chat Archive

## 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.

Source: The last exercise on this Page

#### 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 withtwoterms.

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

justexplain 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