## Stream: new members

### Topic: Creating the natural numbers

#### Michael Barz (Jul 12 2022 at 21:09):

Hello! I am new to Lean; I finished the natural number game and going through the tutorials, and I had a small question. To practice more, I'd like to try formalizing my solutions to some first year elementary number theory problem sets; the problem sets define the integers as an ordered ring obeying the well-ordering principle. I was wondering: is there any quick way of creating a Lean project, importing the ring axioms, and declaring 'Z' to be an ordered ring with the well-ordering principle? I'm guessing that Z the ring is probably defined somewhere in mathlib, but I'd like to try following the problem sets I'm formalizing as closely as possible, and hence copy their definition of Z. It feels like a sort of silly question, but all the exercises I've done so far for Lean have been about proving things about types that were already defined, and so I'm not entirely sure how to define my own integer type. Thanks for anyone who can help!

#### Mark Gerads (Jul 12 2022 at 21:13):

I don't know if this is helpful, but the definition is here: https://github.com/leanprover-community/lean/blob/9d5adc6ab80d02bb2a0fd39a786aaeb1efd6fb01/library/init/data/int/basic.lean#L15

#### Michael Barz (Jul 12 2022 at 21:26):

Thanks, Mark! I think they give an inductive definition of natural numbers, and then go on to define integers, but I was wondering if there was a quick way to declare a type 'Z' with two binary operations +, * obeying the usual ring axioms, etc.

#### Bolton Bailey (Jul 12 2022 at 21:33):

If all you want is the ring operations and you don't care about the order, then
variables (myZ : Type) [comm_ring myZ]

#### Michael Barz (Jul 12 2022 at 21:52):

Thanks Bolton! I think I will go with this approach, but one more question: if I define variables (myZ : Type) [ordered_ring myZ], how can I assert that myZ obeys the well-ordering principle? At the moment the only thought I have is to make it a theorem and say 'sorry,' but I'm guessing that's not how one adds axioms...

#### Yakov Pechersky (Jul 12 2022 at 22:01):

The principle is docs#conditionally_complete_linear_order

#### Yakov Pechersky (Jul 12 2022 at 22:02):

And lo, a proof that the Lean ints are so: docs#int.conditionally_complete_linear_order

#### Matt Diamond (Jul 12 2022 at 22:12):

in theory you could do variables (myZ : Type*) [ordered_ring myZ] [wo : is_well_order myZ (<)] but it seems like that may be _too_ minimal

#### Matt Diamond (Jul 12 2022 at 22:16):

I'm guessing that's not how one adds axioms

You can add axioms using the axiom keyword, like this:

axiom well_ordered : is_well_order myZ (<)


#### Michael Barz (Jul 12 2022 at 22:56):

Thank you all for the suggestions! I think I've gotten things set up the way I wanted. It was very helpful!

#### Junyan Xu (Jul 12 2022 at 23:32):

Do you intend Z to be the integers (ℤ) or the natural numbers (ℕ)? If the former, it's not well-ordered under (<); if the latter, it's not a comm_ring, only a comm_semiring.

#### Michael Barz (Jul 13 2022 at 00:22):

Ah, Junyan, I was using 'well-ordered' to mean that every bounded below set has a least element, but I realize that's probably not how Lean uses it! Luckily I noticed that while formalizing, but thanks for mentioning it! (Thus I went with Yakov's suggestion.)

#### Michael Barz (Jul 13 2022 at 01:03):

Sorry, one last worry I was having. I wanted to try cleaning up my terms, so I created a definition definition minimum_of (S : set integers) (m : integers) := (m ∈ S) /\ (forall s : integers, s ∈ S -> m <= s)  and then wanted to change my well ordering principle axiom to axiom wop (S : set integers) : (∀ s : integers, s ∈ S -> 0 <= s) -> (exists a : integers, minimum_of S a) However, it seems that Lean does not like me asserting minimum_of S a -- it seems OK when I say (hx : minimum_of S a) : [some proposition] but it is scared to have minimum_of S a be implied by something. Am I doing something wrong? How should I write this?

#### Kevin Buzzard (Jul 13 2022 at 02:21):

Can you post either or both of fully working code in #backticks and the precise error you get? The exact error tells you important stuff! Right now my Lean can't get past integers.

Sure!

#### Michael Barz (Jul 13 2022 at 11:57):

import algebra.ring
import algebra.order.ring

variables (integers : Type) [ordered_comm_ring integers]

definition minimum_of (S : set integers) (m : integers) := (m ∈ S) /\ (forall s : integers, s ∈ S -> m <= s)

axiom wop (S : set integers) :
(∀ s : integers, s ∈ S -> 0 <= s) -> (exists a : integers, minimum_of S a)


#### Michael Barz (Jul 13 2022 at 11:57):

Here is the relevant portion of code--I would like to declare the well-ordering principle as an axiom

#### Michael Barz (Jul 13 2022 at 11:57):

I get the error:

ailed to synthesize type class instance for
integers : Type,
_inst_1 : ordered_comm_ring integers,
S : set integers,
ᾰ : ∀ (s : integers), s ∈ S → 0 ≤ s,
a : integers
⊢ ordered_comm_ring ↥S
test.lean:9:60
type mismatch at application
minimum_of ↥S a
term
a
has type
integers
but is expected to have type
set ↥S
/Users/laptop-yp/ross_lean/ross_lean/src/test.lean:9:60: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
minimum_of ?m_1 ?m_3
has type
?m_1 → Prop
but is expected to have type
Prop


#### Michael Barz (Jul 13 2022 at 11:59):

At the moment I have just being using Lean's built-in \Z to formalize the sets, but I'm imagining this problem reflects some misunderstanding on my end of how propositions work in Lean, so hopefully someone can set me straight if anyone realizes the problem quickly.

#### Ruben Van de Velde (Jul 13 2022 at 11:59):

Needs to be minimum_of integers S a

#### Ruben Van de Velde (Jul 13 2022 at 12:00):

The error is about not passing an explicit argument

#### Ruben Van de Velde (Jul 13 2022 at 12:00):

(which you declared in the variables statement)

#### Michael Barz (Jul 13 2022 at 12:01):

Thank you so much, Ruben!

#### Michael Barz (Jul 13 2022 at 12:01):

Changing that works!

#### Ruben Van de Velde (Jul 13 2022 at 12:04):

My pleasure, it's nice to see someone with a simple enough issue that I can solve it every once in a while :)

#### Michael Barz (Jul 13 2022 at 12:08):

Also, the benefit to finally formalizing my well-ordering principle instead of using the Lean integers, is that I realize my well-ordering axiom is false as stated since I didn't posit my set be non-empty!

#### Kevin Buzzard (Jul 13 2022 at 13:53):

Michael Barz said:

Thank you so much, Ruben!

Note that your original question got no helpful responses other than "ask a better question" and your good question was answered within two minutes. There is a moral there -- not just for you! There is an art to asking good questions and the sooner someone learns it the quicker that person can learn :-)

Last updated: Dec 20 2023 at 11:08 UTC