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

Stream: new members

[Robbie]

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]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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

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

[Riccardo Brasca]

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]

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]

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 :

$$∀(a,b,c,d)⋲ℝ⁴$$

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]

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]

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

[Eric Wieser]

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]

So for instance you could write:

structure MyP where
  re : ℂ
  p : ℂ

[Robbie]

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)*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

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

[Kyle Miller]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Eric Wieser]

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

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

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

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

[Robbie]

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]

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]

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
  simp

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

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

[Kyle Miller]

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

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]

At least the number system is two-dimensional:

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

[Robbie]

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]

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]

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