Converting basic algebra problem into lean

Stream: new members

[Jake]

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?

[Bryan Gin-ge Chen]

Maybe:

import algebra.group_power

example (R : Type*) [group R] (x y : R) : x*x*x *y*y = x^3 * y^2 := sorry

[Jake]

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]

Most likely not in the sense you're thinking of, though #simp can do some basic stuff.

[Jake]

what does Type* mean?

[Johan Commelin]

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

[Jake]

The * in Type

[Jake]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Jake]

kk ya ill just come back to that

[Bryan Gin-ge Chen]

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

[Jake]

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

[Johan Commelin]

What does that mean?

[Johan Commelin]

You mean

def approx_eq (x y : real) := some_def

¿Or something else?

[Jake]

ya what you wrote!

[Johan Commelin]

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

[Jake]

yeah only for real numbers

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

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

[Kenny Lau]

we could also formalize "normal forms"

[Jake]

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]

so first define normal form

[Jake]

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]

that is not a normal form

[Kenny Lau]

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

[Johan Commelin]

@Jake That won't work, because x * x = x^2. If one of them is in normal form, so is the other.

[Johan Commelin]

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

[Jake]

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

[Johan Commelin]

You either need to go meta and work with expr, or you need to define a type of expressions yourself

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

ok the problems much clearer now, thank you

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Try formalising that in Lean :-)

[Jake]

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

[Reid Barton]

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