Zulip Chat Archive

Stream: new members

Topic: Can I add custom math set to lean 4 with custom propreties ?

Robbie (Dec 04 2023 at 20:19):

Here is my question,
So basically i'm a new born in lean community and i would like to know if there is any solution to define other sets than N Z Q R C ....
I don't talk here about subset like [0,8] wich is in R but more about creating another set where i can define what does work and what ddoes not....
Thanks in advance :grinning:

Shreyas Srinivas (Dec 04 2023 at 20:27):

This is probably a #new members question. Further, I am not sure what you mean precisely. Mathlib's Set a type lets you define a set of elements of type a for any a in set builder form (i.e. elements of the type that satisfy a property). N, Z, R, Q, and C are actually types in lean, not sets themselves, though you can define sets that contain all elements of that type as def ℕ_set : Set ℕ := { x : ℕ | True}. There is also a separate ZFC set API. I think if you specify what you want more precisely in pen and paper math (using the latex feature in zulip) I could give a better answer.

Notification Bot (Dec 04 2023 at 20:27):

This topic was moved here from #lean4 > Can I add custom math set to lean 4 with custom propreties ? by Riccardo Brasca.

Riccardo Brasca (Dec 04 2023 at 20:28):

Hi, and welcome! I've moved you're question to the "new members" stream.

Riccardo Brasca (Dec 04 2023 at 20:29):

Can you make your question a little more precise? Anyway the short answer is that you can do in Lean everything you can do with pen and paper, so maybe you can give an example of what you mean.

Robbie (Dec 04 2023 at 21:31):

(Sorry for the wrong channel...)
So here are more explanations :big_smile: ,

I created, on paper, a set wich could be larger than C by introducing the letter p as a "non variable" in the set P, like i in the complex, so for that to work, we defined any number in this set as q =Z1 + z2*p or q=(a+b*i)+(c+d*i)*p, with z1, z2 in C and a,b,c,d in R (and Z1=a+b*i; z2=(c+d*i)*p. To make things easier and to make sure that starting with that 'axiom', all our demonstrations are 'valid' we wanted to use lean to prove them, because starting with that we tried to elaborate a little more bu we really need help with a math proof assistant to make sure we are not going in a bad direction ...

(So to summarize all of that, I want to recreate a such P set in Lean)

Did I provide enough infos ?
In any case, thank you for your quick answers.

qP(a,b,c,d)R4z1,Z2Cq=(a+bi)+(c+di)p ∀q⋲ℙ ∀(a,b,c,d)⋲ℝ⁴ ∀z1,Z2⋲ℂ q= (a+bi) + (c+di)p

Riccardo Brasca (Dec 04 2023 at 21:44):

You should try to write down a precise mathematical definition of the set you want. When you say "y introducing the letter p as a "non variable" in the set P" it is not clear what you mean.

Kyle Miller (Dec 04 2023 at 21:51):

I think Robbie means adjoining an element to the complex numbers subject to some relations (though I don't see a relation on this element p, but presumably p^2 = c for some constant c?)

Robbie (Dec 04 2023 at 21:52):

I mean that's it's not like you introduce x in the reals, where you can give any values that you want to it unless it's in ℝ.
In the complex, you can't say i=8 or i=pi, that's the same for p, I don't know the right mathematical word for that..

And the definition of the Set P is not more complex than that :


Set P = {q: P | q = (a+b*i)+(c+d*i)*p }

I know my idea can be a little bit weird but anyways I was wondering if it was possible in Lean and as everything is possible nowadays :joy:

Riccardo Brasca (Dec 04 2023 at 21:59):

What you describe looks like considering the polynomials over the reals, maybe with some relations (the complex numbers can be introduced in this way for example). Anyway before formalizing something you need to have a very precise definition on paper. Lean is very very picky about that.

Riccardo Brasca (Dec 04 2023 at 22:00):

Or maybe even just pairs of complex numbers, but again, you have to make it precise on paper.

Eric Wieser (Dec 04 2023 at 22:03):

Pairs of complex numbers seem to at least biject with what's being asked for here. What does multiplication mean for this "set", if anything?

Eric Wieser (Dec 04 2023 at 22:07):

So for instance you could write:

structure MyP where
  re : 
  p : 

Robbie (Dec 04 2023 at 22:13):

Well it's difficult to write a precise definition when I myself don't even know ... :joy:
Yeah I know, I start things not necessarily the right way.

Could you give me maybe a list of things I have to formalise before starting to create it in Lean ?

My goal for now is to add together q and q' when both of them are in ℙ.

On paper i wrote :

q+q=((a+a)+(b+b)i)+((c+c)+(d+d)i)pq+q' = ((a+a')+(b+b')*i)+((c+c')+(d+d')*i)*p


For multiplications things were getting overcontrolled since i had to define what pp is, I chose to define it as p and so for all n in N pⁿ=p
That means that like for addition, with multiplications i have

qq=[(a+bi)+(c+di)p][(a+bi)+(c+di)p]q*q' = [(a+bi)+(c+di)p] [(a'+b'i)+(c'+d'i)p]

Kyle Miller (Dec 04 2023 at 22:32):

This is known as C[p]/(p2p)\mathbb{C}[p]/(p^2-p), "adjoining a new element pp to C\mathbb{C} modulo the relation p2p=0p^2-p=0"

Kyle Miller (Dec 04 2023 at 22:34):

There's a ring isomorphism between this and C2\mathbb{C}^2, where you send qC[p]/(p2p)q\in \mathbb{C}[p]/(p^2-p) to the pair (q(0),q(1))(q(0), q(1)), where I am defining q(x)q(x) to mean "substitute p=xp=x in qq".

Kyle Miller (Dec 04 2023 at 22:35):

The way you do addition and multiplication on C2\mathbb{C}^2 for this to make sense is componentwise addition and multiplication.

Eric Wieser (Dec 04 2023 at 22:36):

... which happens to be precisely the multiplication that Mathlib puts on ℂ × ℂ already! (so you can write abbrev P := ℂ × ℂ and it will just work)

Julian Berman (Dec 04 2023 at 22:36):

@Robbie what are you trying to do with and/or prove about what you've defined? Or why have you defined your new thing? Is it to play around? Or do you have some purpose? Or just learning?

Kyle Miller (Dec 04 2023 at 22:37):

(Something I assumed in the analysis is that ip=pi. If you do ip=-pi then you'd get something different. I'm not sure what -- if you instead had p^2=-1 that would be the quaternions.)

Eric Wieser (Dec 04 2023 at 22:40):

(And if you had ip=pi but p^2 = 0 that would be DualNumber ℂ)

Robbie (Dec 04 2023 at 22:40):

It's basically to play with maths aha
And i wanted to put that set : P between C and the hypercomplex which i dont know a single thing about
So yeah i*p=p*i

Kyle Miller (Dec 04 2023 at 22:43):

It's hard to play with Lean making new number systems unless you know some ring theory and can state what you want in terms of ring theory. Mathlib has stuff about adjoining elements to rings.

Kyle Miller (Dec 04 2023 at 22:43):

Anyway, given your rules, I can cook up a number system after having applied the theory and simplified the situation.

import Mathlib

abbrev P :=  × 
def p : P := (0, 1)

def ofC (c : ) : P := (c, c)

example : p * p = p := by
  unfold p

example (a b a' b' : ) :
    (ofC a + ofC b * p) + (ofC a' + ofC b' * p) = ofC (a + a') + ofC (b + b') * p := by
  simp [ofC, p]

example (a b a' b' : ) :
    (ofC a + ofC b * p) * (ofC a' + ofC b' * p)
      = ofC (a * a') + ofC (b * a' + a * b' + b * b') * p := by
  simp [ofC, p]

Kyle Miller (Dec 04 2023 at 22:44):

(This ofC function is a map from the complex numbers to your new P type. There are ways to make it so you don't have to explicitly write it, but I didn't do that here.)

Kyle Miller (Dec 04 2023 at 22:45):

I only proved the addition and multiplication rules seem to be right for P, but I didn't show that P is the most general number system with these properties.

Kyle Miller (Dec 04 2023 at 22:46):

At least the number system is two-dimensional:

example : FiniteDimensional.finrank  P = 2 := by simp

Robbie (Dec 04 2023 at 22:50):

Oh ! Thank you for all of that stuff to study aha. Also, what are the simp and ring tactics ? My Lean does not recognize them
(Sorry for all of my questions but afterall i'm in the newbie channel :sob:)

Kyle Miller (Dec 04 2023 at 23:04):

Here are a lot of learning resources: https://leanprover-community.github.io/learn.html

The book Mathematics in Lean is a mathematics-oriented introduction, and it talks about simp and ring.

Kyle Miller (Dec 04 2023 at 23:05):

I haven't read Heather's book yet, but there's also The Mechanics of Proof

Last updated: Dec 20 2023 at 11:08 UTC