prove basic things

Stream: new members

[kali]

Hello,

I am trying to learn lean and prove basic things.

I want to do the following axiom but I don't understand how to do it.
For any real a and b, a + b is a real.
axiom t: ∀ (a b : ℝ), a + b ∈ ℝ -- error

The following axiom:
Every real a admits a unique opposite -a such that -a + a = a + (-a) = 0.

The following theorem:
For any real a, -(-a) = a
I want to prove it by using the above axiom, substituting a by -a in the equation -a + a = 0 and that the opposite is unique.

Thanks for your help.

[Arien Malec]

The same file where you import the reals also gives you definitions for add which provides your closure requirement, and provides an implementation of field docs#field which provides add_left_neg

[Arien Malec]

I assume your goal is to go from the field axioms to your lemma, yes?

[Martin Dvořák]

Well, the problem is that ℝ is a type, not a set.

[Martin Dvořák]

You can be sure that (a + b) : ℝ by definition of the + operation.

[Martin Dvořák]

I am saying that a + b ∈ ℝ is a syntactic error and (a + b) : ℝ is not a proposition.

[Martin Dvořák]

As for the second question, you cannot say ∃ -a literally, but you can say, for example,

∀ a : ℝ, ∃ b : ℝ, b + a = 0 ∧ a + b = 0

which is a proposition and can easily be proved.

[Martin Dvořák]

Do you want a hint for the uniqueness of the opposite?

[Eric Wieser]

The answer is just ∃!, right?

[Martin Dvořák]

Eric Wieser said:

The answer is just ∃!, right?

This symbol scares me!

[Martin Dvořák]

I mean, here it would be the last quantifier in the prenex, so I guess I can guess its meaning right, but...

[Dean Young]

(deleted)

[kali]

@Arien Malec I know it must already exist but I would like to do it myself.
I'm just trying to formulate the mathematics of my mathematics book.
I'm just starting so I have a lot of trouble ^^
I wanted to start with geometry but after 2 days of not making any progress I decided to start with simpler things.

@Martin Dvořák I know it must already exist but I would like to do it myself.

This is what I tried to do.

definition opposit (a : ℝ) := -a
axiom add_opposit : ∀ (a : ℝ), a + opposit a = 0
axiom opposit_add : ∀ (a : ℝ), opposit a + a = 0

definition is_opposit (a b : ℝ) := a + b = 0
axiom uniq_opposit : ∀ (a b c : ℝ), is_opposit a b ∧ is_opposit b c → c = a

example : ∀ (a : ℝ), -(-a) + (-a) = 0 :=
begin
  intro a,
  apply opposit_add (-a),
end

theorem neg_neg_plus: ∀ (a : ℝ), -(-a) = a :=
begin
  intro a,
  apply uniq_opposit a (-a) (-(-a)),
  split,
    apply add_opposit,
    apply add_opposit,
end

[kali]

Lean accepts the theorem but I'm not sure it's really complete.
I know that lean already knows the basics so I don't know if it's complete or if it's just lean that knows it's true and therefore accepts it.

[Arien Malec]

I'm suggesting you are going to get farther starting from field and proving the consequences of the field axioms, rather than re-stating the axioms.

[Arien Malec]

neg_unique should be a theorem rather than an axiom, starting from field

[kali]

I'm in second grade and I don't know these things.
That's why I don't use the library, I don't understand the math on it.

I have a lot of difficulty with logic, I try to learn lean to have a support with which to improve myself.

[kali]

In my book it is an axiom, probably because the math needed to prove it is not yet available.

[kali]

Maybe I'm wrong to want to use lean

[Martin Dvořák]

I think you state and prove stuff for ℝ which is the standard model of real numbers.
You probably want to do it for an arbitrary type R that satisfies your axioms, right?

[kali]

I'm not sure I understand the question.
What I'm trying to do is only on the real numbers.
I don't know yet the mathematical objects that allow to generalize all this.
I'm already struggling with basic mathematics so I'm not trying to get into that stuff yet.

I could at least try to generalize to make it work with integers

[Martin Dvořák]

I mean, you want to make sure that you prove theorems using your axioms only, right?

[kali]

Yes, exactly.
I don't want it to work because lean is smarter than me

[Arien Malec]

I think the best path for what you want to do is the Natural Number Game: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Arien Malec]

And then Theorem Proving in Lean...

[Martin Dvořák]

Good!
Then you should avoid using ℝ because Lean might use properties of real numbers behind your back.

[kali]

I'll take a look thanks.
I am currently using theorem proving in lean

In this case I have to define the real numbers myself?
So you think that what I have done is incomplete and that lean is doing things to make it correct?

[Martin Dvořák]

Forget about the proofs for a while. What theorems do you want to prove?
I think you want to prove that if you have a structure with your axioms, then something must hold.
What your code actually proves is that if you have the real numbers ℝ with everything that the library already know about real numbers AND your axioms in addition to that, then something must hold.

[Martin Dvořák]

I think you @kali work on meaningful exercises, but you need to change the setting.

[Jireh Loreaux]

@Martin Dvořák, not really. Kali hasn't used anything from the library (except the existence of the + and - operations). So, even though it's not a "safe" way to do it, so far it's not a problem.

[Jireh Loreaux]

Let me describe how I might go about this if you don't want to use anything from the library and you just want to formalize the things from your textbook. Give me a few minutes.

[Martin Dvořák]

Jireh Loreaux said:

Martin Dvořák, not really. Kali hasn't used anything from the library (except the existence of the + and - operations. So, even though it's not a "safe" way to do it, so far it's not a problem.

Right... If you inspect the proofs, you can conclude that...

[kali]

@Martin Dvořák The theorem quoted above.
For any real a, -(-a) = a.
This is just the chapter in my book on real numbers that gives some axioms (the opposite of a real number etc) and then gives a proof of the above theorem.
Then I will try to prove all the other theorems in the book.

That's exactly it, I want to be sure that the structure is right so that I can be 100% convinced and retain.
I think that it could help me to become better in mathematics.

[kali]

@Jireh Loreaux
It's not that I'm against using the library, it would make things easier but it wouldn't really help me to improve. I would just have a black box that I don't understand but that seems to work.

If I use the already defined reals it is to use them later in exercises that require calculations and because I don't really know how to define them. :sweat_smile:
Maybe I should do something else

[kali]

Thank you for all your answers, I really appreciate it :hug:

[Arien Malec]

kali said:

In this case I have to define the real numbers myself?

Here's what I'm suggesting (though I think that NNG is a better start):

Import mathlib.data.real.basic

That gives you a basic definition of the reals and the field axioms but remarkably few theorems.

From there, you can do things like define and prove neg_unique and comm_add and add_eq_zero_iff in terms of the reals.

[Martin Dvořák]

kali said:

Martin Dvořák The theorem quoted above.
That's exactly it, I want to be sure that the structure is right so that I can be 100% convinced and retain.
I think that it could help me to become better in mathematics.

I really like your intention!
I am just saying that, in order to make it more transparent for yourself, you should do it without connection to ℝ already defined in mathlib.

[Martin Dvořák]

I suggest you @kali just wait for @Jireh Loreaux to provide you a skeleton for your exercises.

[Arien Malec]

Martin Dvořák said:

I am just saying that, in order to make it more transparent for yourself, you should do it without connection to ℝ already defined in mathlib.

The basic issue with doing this is that you have to start somewhere, and you certainly don't want to start with constructing the reals, because that's really hard. You could start with restating the field or ring axioms and then proving stuff from there, but mathlib has already done a bunch of that work for you, so why not use it?

[Jireh Loreaux]

If you want to follow as closely as possible your textbook, then something like this would work:

noncomputable theory

-- assert a type, two special elements of that type and a bianary function on that type
constant ℝ : Type
constant add : ℝ → ℝ → ℝ
constant zero : ℝ
constant one : ℝ

-- gives access to the notation `+`, `1` and `0`.
instance : has_add ℝ := ⟨add⟩
instance : has_one ℝ := ⟨one⟩
instance : has_zero ℝ := ⟨zero⟩

-- add axioms the additive identity and commutativity of addition
axiom zero_add : (∀ r : ℝ, 0 + r = r)
axiom add_zero : (∀ r : ℝ, r + 0 = r)
axiom add_comm : (∀ r s : ℝ, r + s = s + r)
axiom add_assoc : (∀ r s t : ℝ, r + s + t = r + (s + t))

-- add axiom for the existence of additive inverses
axiom exists_neg : ∀ r : ℝ, ∃ s : ℝ, r + s = 0

-- `classical.some` is how you get an element out of an existential statement, so
-- this allows us to define negation from addition the way is done in textbooks.
def neg : ℝ → ℝ := λ r, classical.some (exists_neg r)

-- this gives us access to the `-` notation for `neg`
instance : has_neg ℝ := ⟨neg⟩

-- this is a lemma which tells use the definitional property of our new function.
lemma add_neg (r : ℝ) : r + (-r) = 0 :=
classical.some_spec (exists_neg r)

lemma neg_add (r : ℝ) : (-r) + r = 0 :=
by rw [add_comm, add_neg]

lemma neg_unique (r s : ℝ) (h : r + s = 0) : s = -r :=
by rw [←zero_add s, ←neg_add r, add_assoc, h, add_zero]

lemma neg_neg (r : ℝ) : -(-r) = r := sorry

[kali]

@Arien Malec
I use import data.real.basic
When I look at it it seems to give the same thing as mathlib.data.real.basic.
Are the axioms you are talking about used by default or is it for me to use them instead of defining them?

@Martin Dvořák
I had not even tried because it seemed too complicated.
I'm going to push my limits.
constant Real : Type

[Eric Wieser]

Here's how you do it without any reference to mathlib:

class is_my_real (R : Type*) extends has_add R, has_neg R, has_zero R :=
(my_ax : ∀ a b : R, a + b = 0 ∧ b + a = 0 ↔ b = -a)

theorem my_neg_neg (R : Type*) [is_my_real R] (a : R) : -(-a) = a :=
sorry

[Jireh Loreaux]

Eric, that already assumes negation is defined and doesn't come from the existence of an additive inverse.

[Eric Wieser]

What's going on here, is that the first two lines of that code say:

We say a type R satisfies is_my_real R if:

• The + symbol is defined, consuming two Rs and producing another
• The - symbol is defined, consuming one Rs and producing another
• A 0 is defined for R
• For this R, we have a unique solution for b when a + b = 0 and b + a = 0, and that solution is the one that we chose to spell -

[Eric Wieser]

The theorem line then proceeds to prove the --a = a you wanted, and does so for anything that satisfies your axioms; that way you can be sure you didn't cheat, because the only thing you know about R is that it satisfies those axioms.

[kali]

@Jireh Loreaux Merci beaucoup !!
Thank you very much!
I will review everything to understand and move forward from here

[Martin Dvořák]

Arien Malec said:

You could start with restating the field or ring axioms and then proving stuff from there, but mathlib has already done a bunch of that work for you, so why not use it?

I suppose @kali works with a book that explicitly states all axioms which are gradually added to the theory they build.

[Jireh Loreaux]

If you use Eric's suggestion (also a good approach), just realize that there are axioms left out of what he wrote, so the result won't be provable as is. You need to add other axioms to his is_my_real (like commutativity and associativity of addition, the defining property of - as an additive inverse, etc.).

[kali]

@Arien Malec I want to do it myself.
Later I will use what has been done but I would like to understand the basics

[Jireh Loreaux]

Note that my approach likely more closely matches your textbook in style (e.g., use of axiom) and details, but it is also harder in Lean (because you need to build neg from an existential statement, etc.).

[kali]

@Eric Wieser Thanks, I think I prefer the one from @Jireh Loreaux but I will make another version from here too.

[Arien Malec]

I've realized that my approach of starting with mathlib.data.real.basic does in fact pull in a bunch of theorems.

[Arien Malec]

It's surprisingly hard to "strip down" mathlib for pedagogy.

[Eric Wieser]

(I didn't see Jireh's message when sending mine due to bad Internet, sorry!)

[kali]

@Martin Dvořák Yes, that's exactly it

@Jireh Loreaux It looks a lot like my book (even more detailed).
This is exactly what I was looking for.
I won't be able to start now because it's late and I'm going to bed, but I'm going to get right into it tomorrow

[kali]

@Arien Malec Later I will use it because it looks great but for me it is too much of a black box

[kali]

@Eric Wieser Thank you for your suggestion, I will also use it

[Eric Wieser]

Jireh Loreaux said:

Eric, that already assumes negation is defined and doesn't come from the existence of an additive inverse.

That doesn't seem to be a meaningful distinction to me. My version is just assuming that the name - is given to something arbitrary, and then adds the "that someone is the unique solution to ..." as an axiom.

[Jireh Loreaux]

Great Kali, please ping me if you get stuck and I'll be happy to help. What I would be most likely to recommend is that you use my approach above for the basics, but then once you have proven these foundational results, it might be then that you want to switch into using mathlib (by importing data.real.basic or some such). That way, you can understand exactly what's going on in your textbook, but you don't have to build literally everything from scratch.

[Kevin Buzzard]

kali said:

Arien Malec I want to do it myself.
Later I will use what has been done but I would like to understand the basics

I think you're right about wanting to understand the basics, but I'm not sure that leaping into a calculation based on a book written in the language of set theory and trying to formalise it in dependent type theory is the way to do it. Did you take a look at #tpil ? This won't help you with the real numbers but it might help you to understand more about how Lean works.

[Eric Wieser]

kali said:

Eric Wieser Thank you for your suggestion, I will also use it

I would recommend not mixing Jireh's version and mine. Pick whichever one you prefer, and once you understand what's going on you could try the other one.

[Jireh Loreaux]

Eric, right, but it just doesn't match the way things are generally presented in introductory textbooks. I'm not complaining about your version, just pointing out the distinction. Sorry if it came across wrong.

[kali]

@Jireh Loreaux That's what I'm trying to do. I intend to use mathlib of course but when it is not a black box anymore.
I'll let you know if I have any problems and either way I'll put my progress here.
Thank you

[Jireh Loreaux]

(AFK for a few hours)

[kali]

@Kevin Buzzard Yes, this is what I use to learn lean.
My problem is not only with lean but also with mathematics.
Mathlib is complicated because I have to understand lean but I don't understand the mathematics behind it.
That's why I want to start from something else.

[kali]

@Eric Wieser It was to try two different approaches and see the result according to each approach.
I'm not lazy so I don't mind trying different things. I don't feel like I'm wasting my time as long as I learn something

[kali]

Thank you all for your answers, I have to go to bed and I will continue tomorrow.
Good evening to all