an exercise in documentation

Stream: new members

[Trapped Beast]

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]

Trapped Beast has marked this topic as resolved.

[Notification Bot]

Trapped Beast has marked this topic as unresolved.

[Scott Morrison]

Bool is a type with two terms.

[Scott Morrison]

(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]

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

[Trapped Beast]

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]

what is the question?

[Mario Carneiro]

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

[Trapped Beast]

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]

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]

Mario Carneiro said:

what is the question?

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

[Johan Commelin]

Can you just explain what you have tried so far?

[Johan Commelin]

How do you define a function in Lean?

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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

[Trapped Beast]

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]

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

[Johan Commelin]

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]

Compare Bool to Unit ⊕ Unit

[Johan Commelin]

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

[Trapped Beast]

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]

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.