Creating the natural numbers

Stream: new members

[Michael Barz]

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]

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]

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]

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]

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]

The principle is docs#conditionally_complete_linear_order

[Yakov Pechersky]

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

[Matt Diamond]

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]

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]

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

[Junyan Xu]

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]

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]

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]

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.

[Michael Barz]

Sure!

[Michael Barz]

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]

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

[Michael Barz]

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
Additional information:
/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]

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]

Needs to be minimum_of integers S a

[Ruben Van de Velde]

The error is about not passing an explicit argument

[Ruben Van de Velde]

(which you declared in the variables statement)

[Michael Barz]

Thank you so much, Ruben!

[Michael Barz]

Changing that works!

[Ruben Van de Velde]

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]

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]

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