Zulip Chat Archive

Stream: new members

Topic: Converting basic algebra problem into lean


view this post on Zulip Jake (May 14 2020 at 03:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Jake (May 14 2020 at 04:03):

what does Type* mean?

view this post on Zulip Johan Commelin (May 14 2020 at 04:05):

@Jake Are you asking about the Type in Type* or the * in Type*, or both?

view this post on Zulip Jake (May 14 2020 at 04:06):

The * in Type

view this post on Zulip Jake (May 14 2020 at 04:06):

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

view this post on Zulip Johan Commelin (May 14 2020 at 04:07):

@Jake It means Type u for a fresh new universe u.

view this post on Zulip Johan Commelin (May 14 2020 at 04:07):

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

view this post on Zulip Jake (May 14 2020 at 04:07):

kk ya ill just come back to that

view this post on Zulip 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.

view this post on Zulip Jake (May 14 2020 at 04:13):

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

view this post on Zulip Johan Commelin (May 14 2020 at 04:14):

What does that mean?

view this post on Zulip Johan Commelin (May 14 2020 at 04:15):

You mean

def approx_eq (x y : real) := some_def

¿Or something else?

view this post on Zulip Jake (May 14 2020 at 04:15):

ya what you wrote!

view this post on Zulip 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.

view this post on Zulip Jake (May 14 2020 at 04:16):

yeah only for real numbers

view this post on Zulip Mario Carneiro (May 14 2020 at 04:44):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jake (May 14 2020 at 06:52):

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

view this post on Zulip Kenny Lau (May 14 2020 at 06:55):

we could also formalize "normal forms"

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 14 2020 at 07:15):

so first define normal form

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 14 2020 at 07:18):

that is not a normal form

view this post on Zulip Kenny Lau (May 14 2020 at 07:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jake (May 14 2020 at 07:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 14 2020 at 07:21):

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

view this post on Zulip Johan Commelin (May 14 2020 at 07:21):

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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Jake (May 14 2020 at 07:28):

ok the problems much clearer now, thank you

view this post on Zulip Mario Carneiro (May 14 2020 at 07:30):

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

view this post on Zulip Mario Carneiro (May 14 2020 at 07:31):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 14 2020 at 07:32):

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

view this post on Zulip Kevin Buzzard (May 14 2020 at 07:32):

Try formalising that in Lean :-)

view this post on Zulip 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

view this post on Zulip 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