# Zulip Chat Archive

## Stream: new members

### Topic: Converting basic algebra problem into lean

#### Jake (May 14 2020 at 03:48):

I want to convert some algebra problems into a lean theorem. Here's one for example: Write x*x*x*y*y in exponential notation. How could i formulate this in lean?

#### Bryan Gin-ge Chen (May 14 2020 at 03:53):

Maybe:

```
import algebra.group_power
example (R : Type*) [group R] (x y : R) : x*x*x *y*y = x^3 * y^2 := sorry
```

#### Jake (May 14 2020 at 03:57):

are there algebra simplification features in lean? like say i had a more complicated example with all kinds of operations (including trig functions and rational expressions). Or could i just test for equality numerically somehow?

#### Bryan Gin-ge Chen (May 14 2020 at 03:59):

Most likely not in the sense you're thinking of, though `#simp`

can do some basic stuff.

#### Jake (May 14 2020 at 04:03):

what does Type* mean?

#### Johan Commelin (May 14 2020 at 04:05):

@Jake Are you asking about the `Type`

in `Type*`

or the `*`

in `Type*`

, or both?

#### Jake (May 14 2020 at 04:06):

The * in Type

#### Jake (May 14 2020 at 04:06):

Im on chapter 4 of hitchhikers and did the natural number game and havent seen that

#### Johan Commelin (May 14 2020 at 04:07):

@Jake It means `Type u`

for a fresh new universe `u`

.

#### Johan Commelin (May 14 2020 at 04:07):

Have you read about universes already? If not, just ignore it.

#### Jake (May 14 2020 at 04:07):

kk ya ill just come back to that

#### Bryan Gin-ge Chen (May 14 2020 at 04:08):

There's a brief discussion in 11.1 of Hitchhiker's guide. But I agree with Johan.

#### Jake (May 14 2020 at 04:13):

in theory i can make my own equality type class that tests for equality numerically?

#### Johan Commelin (May 14 2020 at 04:14):

What does that mean?

#### Johan Commelin (May 14 2020 at 04:15):

You mean

```
def approx_eq (x y : real) := some_def
```

¿Or something else?

#### Jake (May 14 2020 at 04:15):

ya what you wrote!

#### Johan Commelin (May 14 2020 at 04:16):

Because this only makes sense for real numbers (and a couple of other types) but not something general.

#### Jake (May 14 2020 at 04:16):

yeah only for real numbers

#### Mario Carneiro (May 14 2020 at 04:44):

Not really, because you can't evaluate elements of type `real`

#### Mario Carneiro (May 14 2020 at 04:46):

If you made a `float`

type (that isn't really `real`

) with floating point approximations of real numbers then you could define `approx_eq`

on that

#### Kevin Buzzard (May 14 2020 at 06:44):

@Jake here's a way of formalising the question which doesn't give the answer away:

```
import algebra.group_power
example (R : Type*) [group R] (x y : R) :
∃ a b : ℕ, x*x*x*y*y = x^a * y^b := sorry
```

As for not having seen stuff, yeah, we're working on it. There is still not enough teaching material for beginners. Hopefully by July this will have changed.

#### Jake (May 14 2020 at 06:52):

Yes that's more what i had in mind, thank you! Looking forward to new learning material

#### Kenny Lau (May 14 2020 at 06:55):

we could also formalize "normal forms"

#### Jake (May 14 2020 at 07:14):

right @Kenny Lau the problem im really trying to solve here is show the existence of an expression that is equal to the expression you started with and is in the proper normal form

#### Kenny Lau (May 14 2020 at 07:15):

so first define normal form

#### Jake (May 14 2020 at 07:18):

for that specific example id need the normal form to be some predicate that returns true for x^a y^b or y^b x^a, and false otherwise

#### Kenny Lau (May 14 2020 at 07:18):

that is not a normal form

#### Kenny Lau (May 14 2020 at 07:18):

because x^a y^b = y^b x^a

#### Johan Commelin (May 14 2020 at 07:19):

@Jake That won't work, because `x * x = x^2`

. If one of them is in normal form, so is the other.

#### Johan Commelin (May 14 2020 at 07:20):

You are caring about syntax, so you can't work with actual terms of type `real`

or whatever.

#### Jake (May 14 2020 at 07:20):

right sorry normal form is not the correct term for what im describing

#### Johan Commelin (May 14 2020 at 07:20):

You either need to go `meta`

and work with `expr`

, or you need to define a type of expressions yourself

#### Johan Commelin (May 14 2020 at 07:21):

But I'm not sure if this is really what you should want to do.

#### Johan Commelin (May 14 2020 at 07:21):

Because it's a lot of work, and I'm not sure what you would gain.

#### Johan Commelin (May 14 2020 at 07:22):

If you are interested in automatically reorganising expressions in the theory of commutative rings, you can look at what the `ring`

tactic does. It puts expressions in some normal form, and then tries to prove equalities.

#### Kenny Lau (May 14 2020 at 07:22):

```
import algebra.group_power
universe u
inductive normal_form : Type
| mk (a b : ℕ)
def normal_form.eval {α : Type u} [monoid α] (x y : α) : normal_form → α
| (normal_form.mk a b) := x^a * y^b
example (R : Type u) [group R] (x y : R) :
∃ n : normal_form, x*x*x*y*y = n.eval x y :=
⟨normal_form.mk 3 2, by unfold normal_form.eval; simp only [pow_succ, pow_two, mul_assoc]⟩
```

#### Jake (May 14 2020 at 07:28):

ok the problems much clearer now, thank you

#### Mario Carneiro (May 14 2020 at 07:30):

@Jake What is wrong with Kevin Buzzard's version of the statement?

#### Mario Carneiro (May 14 2020 at 07:31):

I don't think you need to be formalizing normal forms for this question

#### Kevin Buzzard (May 14 2020 at 07:31):

There is a general phenomenon, which I am only too aware of, where there are "questions" given to mathematicians which are hard to formalise in the sense that the question is not well-specified. We all know the "underlying meaning" of the question here, but there are several ways to formalise it, and people are just playing with these ideas I guess.

#### Kevin Buzzard (May 14 2020 at 07:32):

"For which $n$ are all groups of order $n$ abelian?" is one of my favourites.

#### Kevin Buzzard (May 14 2020 at 07:32):

Try formalising that in Lean :-)

#### Jake (May 14 2020 at 07:32):

theres nothing wrong for this particular question, im just trying build a mental model of how this would generalize to other problems

#### Reid Barton (May 14 2020 at 08:28):

Johan Commelin said:

Jake It means

`Type u`

for a fresh new universe`u`

.

Probably too subtle for this thread, but as far as I can tell it actually just means `Type _`

.

Last updated: May 08 2021 at 19:11 UTC