R golfing

Stream: general

[Daniel Weber]

Following previous discussion, I'm starting this thread to talk about constructing $\mathbb{R}$ from minimal assumptions (rules, scoring, etc.)
cc @Johan Commelin

[Daniel Weber]

Here are some relevant questions:

• What imports are allowed? Some options are no imports whatsoever, only core Lean (stuff in https://github.com/leanprover/lean4/), and some limited part of Mathlib.
• How are solutions scored? Some options are bytes, characters, and lines of code, with lines limited to at most 100 characters.
• What is the target? Some options are Mathlib's ConditionallyCompleteLinearOrderedField, the minimal axioms form the previous thread.

Should we have this template? Is there anything else required?

class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

[Johan Commelin]

I think ConditionallyCompleteLinearOrderedField is a good target. And if a construction wants to use your minimal axioms to get there, that is of course totally fine (and probably a good idea).

[Johan Commelin]

I'm inclined to score using by counting words. Because that doesn't punish whitespace formatting and the use of readable names.

[Johan Commelin]

About imports: everything that you import counts towards your score.

[Daniel Weber]

Johan Commelin said:

I'm inclined to score using by counting words. Because that doesn't punish whitespace formatting and the use of readable names.

How do you want to count non-word tokens? (notation, :=, etc.)

[Daniel Weber]

Johan Commelin said:

I think ConditionallyCompleteLinearOrderedField is a good target. And if a construction wants to use your minimal axioms to get there, that is of course totally fine (and probably a good idea).

Do you want to require using Mathlib's definition, or can one just copy the relevant parts? That still requires defining a large part of the algebraic and order hierarchy

[Daniel Weber]

I think something minimal which doesn't require any setup would be better — Mathlib's docs#ConditionallyCompleteLinearOrderedField requires you to have $\mathbb{Q}$, for example, for ratCast, which I don't think we should require

[Johan Commelin]

Ok, we could build a tiny project independent of mathlib where we define ConditionallyCompleteLinearOrderedField, and separately something that shows that this new definition is equivalent to the one in mathlib.

[Johan Commelin]

I was thinking of counting using (roughly) wc -w.

[Daniel Weber]

Johan Commelin said:

I was thinking of counting using (roughly) wc -w.

This still incentivizes not having whitespaces

[Daniel Weber]

Johan Commelin said:

About imports: everything that you import counts towards your score.

Does this include Init? Do we want to use prelude?

[Johan Commelin]

Daniel Weber said:

Johan Commelin said:

I was thinking of counting using (roughly) wc -w.

This still incentivizes not having whitespaces

Yes, hence the "(roughly)". We could have a first pass where a regex adds a whenever it finds a word boundary \w.

[Johan Commelin]

Daniel Weber said:

Johan Commelin said:

About imports: everything that you import counts towards your score.

Does this include Init? Do we want to use prelude?

Let's not use prelude. And yes, we can just count Init. All participants will get a constant added to their score if we do that. So it doesn't really matter, right?

[Daniel Weber]

Johan Commelin said:

Daniel Weber said:

Johan Commelin said:

About imports: everything that you import counts towards your score.

Does this include Init? Do we want to use prelude?

Let's not use prelude. And yes, we can just count Init. All participants will get a constant added to their score if we do that. So it doesn't really matter, right?

It would've mattered if we allowed using perlude, as you could then avoid some of it (or do it more efficiently)

[Daniel Weber]

Johan Commelin said:

I was thinking of counting using (roughly) wc -w.

I don't think I agree with this, as it allows encoding data weirdly without it counting. However, readability is an advantage. Perhaps just request submitted both ungolfed code (with long names and whitespaces) and golfed code?

[Markus Himmel]

Another option could be to measure the compresssed size of the proof script. See for example the discussion in section 2 of https://www.cs.ru.nl/~freek/factor/factor.pdf.

[Johan Commelin]

Yeah, that's probably a better way!

[Daniel Weber]

Markus Himmel said:

Another option could be to measure the compresssed size of the proof script. See for example the discussion in section 2 of https://www.cs.ru.nl/~freek/factor/factor.pdf.

I think this still incentivizes avoiding whitespaces and long names, as you won't have to compress them. It also benefits writing long be repetitive code, which may not be what we want

[Johan Commelin]

Yeah, but I think it will probably be negligible. And we can still do the regex pass that adds whitespace at word boundaries.

[Edward van de Meent]

You could measure by the sum total sizeOf of the Expressions used in declarations in the proof, maybe?

[Edward van de Meent]

i think we can write a linter for that? maybe?

[Daniel Weber]

Would that cooperate with tactics?

[Edward van de Meent]

i suspect you won't be able to track tactics used, only the terms resulting from the tactics

[Edward van de Meent]

i'd say that's a feature

[Daniel Weber]

Is that what we want to measure, though? I don't think that measures proof complexity accurately

[Edward van de Meent]

i think that when simp does a lot of things, it is no longer a simple proof

[Edward van de Meent]

so counting the actual proofs used seems appropriate to me

[Edward van de Meent]

you may be able to hide a lot of complexity of proof behind aesop too

[Edward van de Meent]

although of course another question would be if the import is worth it?

[Damiano Testa]

Tactics are not usually optimized to produce short proof terms, so measuring the ouput of a tactic may not yield a reasonable estimate of how difficult a proof really is.

[Damiano Testa]

For instance, if you did not have ring, you might use a calc proof to chain a couple of rewrites and produce a much smaller proof term instead.

[Damiano Testa]

I would consider

• the latter to be a better measure of complexity than the former, but
• the former to be more maintainable and better style than the latter.

[Damiano Testa]

E.g., compare these proofs:

import Mathlib.Tactic.Ring

/--
info: Try this: exact Mathlib.Tactic.Ring.of_eq
  (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf a) (Mathlib.Tactic.Ring.atom_pf b)
    (Mathlib.Tactic.Ring.add_pf_add_lt (a ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_zero_add (b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
  (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf b) (Mathlib.Tactic.Ring.atom_pf a)
    (Mathlib.Tactic.Ring.add_pf_add_gt (a ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
-/
#guard_msgs in
example {a b : Int} : a + b = b + a := by
  show_term ring

/--
info: Try this: exact Eq.mpr (id (congrArg (fun _a => _a = b + a) (add_comm a b))) (Eq.refl (b + a))
-/
#guard_msgs in
example {a b : Int} : a + b = b + a := by
  show_term rw [add_comm]

[Daniel Weber]

/poll What do we want to count? (feel free to suggest other things)
Term size
Lean source size

[Kevin Buzzard]

I think that counting Lean source size is a terrible idea because it will encourage obfuscation which will benefit nobody in the long run.

[Daniel Weber]

On the other hand counting term size will result in all proofs being written in term mode, which also isn't very helpful

[Daniel Weber]

I feel like counting Lean source size while scoring in a way that allows meaningful names and whitespaces would probably be more useful

[Damiano Testa]

I have not really measured this in any example, but an option would be to measure the number of leaves/nodes in the syntax tree of every command. That would automatically ignore whitespace and length of names of variables and would be close to a measure of "what you actually typed".

[Edward van de Meent]

you'd still get a penalty to certain kinds of notation, no? bracketing becomes expensive...

[Edward van de Meent]

maybe if you ignore all atoms...

[Kevin Buzzard]

I guess this discussion is just a demonstration of the general principle that when a measure becomes a target, it ceases to be a measure and just distorts things.

[Kevin Buzzard]

Perhaps a good solution is to just try various different experiments to see how one can build the reals and then simply see what you learn from the different constructions, rather than arbitrarily wondering which one is the "shortest". In fact from the above discussion the concept of "shortness" seems be an almost meaningless criterion.

[Dean Young]

Can you try this idea for me? I was really hoping to get it done but I don't have the time.

• Construct preorder L with undrlying set Nat × Nat where Ord : L.Obj × L.Obj → Prop is defined by sending x to (x.fst).fst * (x.snd).snd ≤ (x.fst).snd * (x.snd).fst

• Construct the completion NonnegativeExtendedReals : Type of this preorder using the two element partial order 𝕊 on Bool with 0 ≤ 0, 0 ≤ 1, 1 ≤ 1. This is the (complete) partial order of extended real numbers, which is the same as the preorder of preorder maps from L to 𝕊.

• Construct an order preserving bijection with https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Data/Real/ENNReal.lean#L83-L84

• Construct ℝ using NonnegativeExtendedReals : Type as sequences f : Nat → NonnegativeExtendedReals with ∀(n : Nat),f n < ∞ and ∀(n: Nat), ((f n) + 1) = (f (n+1))

[Aaron Liu]

@E. Dean Young How do you get ℝ from sequences ℕ → ℝ≥0∞? I don't quite follow.

[Dean Young]

@*Aaron Liu Sorry, I was wrong there.

Ok so maybe instead one could use pairs of nonnegative real numbers.

[Dean Young]

At first I fixed it to pairs of nonnegative real numbers, but then I decided I was "inverting the action of Nat by addition", or "inverting the successor". I like that better since it gives me thoughts of the action the integers and the exact sequence from the integers to the real numbers to the circle.

[Dean Young]

So, pairs (x,n) where x is a nonnegative real number and n a natural number, with an equivalence relation.

[Dean Young]

One could also count with respect to l². The idea here is convenient for defining the norm on Rn.

[Daniel Weber]

E. Dean Young said:

One could also count with respect to l². The idea here is convenient for defining the norm on Rn.

What does this mean?

[Daniel Weber]

I got the nonnegative rationals fairly shortly, to try Kevin Buzzard's approach from #new members > Has anyone published/written a \Z, \Q or \R game? @ 💬 :

def lift₂ {s : β → β → Prop} {r : α → α → Prop} (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)
    (hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) :=
  Quot.lift (λa↦Quot.lift (f a) (hr a)) (funext<|Quot.ind λb↦hs · · b ·)

@[simp]
theorem Quotient.eq {r : Setoid α} {x y : α} : Quotient.mk r x = Quotient.mk r y ↔ r.1 x y :=
  ⟨Quotient.exact,exact?%⟩

theorem aux1 (ha : 0 < a) : a * b ≤ a * c ↔ b ≤ c := ⟨exact?%, exact?%⟩

set_option hygiene false
set_option tactic.hygienic false

macro"a"h:term,*:tactic=>`(tactic|($[apply $h];*))
macro"i"h:term,*:tactic=>`(tactic|a $[($h).ind],*)

macro"p":tactic=>`(tactic|(simp_all +contextual [Nat.mul_comm,Nat.mul_add,Nat.mul_assoc,Nat.mul_left_comm,Nat.mul_sub_left_distrib,Nat.mul_eq_zero,Nat.add_comm,Nat.add_assoc,Nat.add_left_comm,Quotient.eq,Nat.mul_le_mul_left,aux1,Nat.mul_le_mul_right,Nat.le_antisymm,Nat.add_le_add_iff_right];try intros;try omega))
macro"p":term=>`(by p)

syntax"k"term,*:term
macro_rules|`(k$a:term,*)=>`(by i $a,*;p)

/-- Defining ℚ≥0, the nonnegative rational numbers -/
abbrev Q:=@Quotient (Nat×{b//0<b}) ⟨λ⟨a,b,_⟩⟨c,d,_⟩↦a*d=b*c,p,p,by p;a Nat.mul_right_cancel b_1;p;simp [a_6,←a_7,←Nat.mul_assoc]⟩
macro"&"e:term:99:term=>`((Quotient.mk _ $e :Q))
instance:Add Q:=⟨lift₂ (λ⟨a,b,h⟩⟨c,d,h⟩↦&⟨a*d+b*c,b*d,p⟩) p p⟩
@[simp]theorem v:&⟨a,b,h⟩+&⟨c,d,i⟩=&⟨a*d+b*c,b*d,p⟩:=rfl
instance:Mul Q:=⟨lift₂ (λ⟨a,b,h⟩⟨c,d,h⟩↦&⟨a*c,b*d,p⟩) p p⟩
@[simp]theorem m:&⟨a,b,h⟩*&⟨c,d,i⟩=&⟨a*c,b*d,p⟩ := rfl
instance:Sub Q:=⟨lift₂ (λ⟨a,b,h⟩⟨c,d,h⟩↦&⟨a*d-b*c,b*d,p⟩) p p⟩
@[simp]theorem s:&⟨a,b,h⟩-&⟨c,d,i⟩=&⟨a*d-b*c,b*d,p⟩ := rfl
instance:Zero Q:=⟨&⟨0,1,p⟩⟩
@[simp]theorem z:(0:Q)=&⟨0,1,p⟩ := rfl
instance:OfNat Q 1:=⟨&⟨1,1,p⟩⟩
@[simp]theorem o:(1:Q)=&⟨1,1,p⟩ := rfl
instance l':LE Q:=⟨λa b↦a-b=0⟩
@[simp]theorem l:&⟨a,b,h⟩≤&⟨c,d,i⟩↔a*d≤b*c:=by rw[l'];p
instance L':LT Q:=⟨λ a b↦a≤b∧¬b≤a⟩
@[simp]theorem L:&⟨a,b,h⟩<&⟨c,d,i⟩↔a*d<b*c:=by rw[L'];p
def inv:Q→Q:=Quot.lift (λ⟨a,b,_⟩↦if h:a>0then&⟨b,a,h⟩else 0)<|by p;split<;>split<;>p;have:=Nat.mul_le_mul_left a_1 ‹0<a_2›;p
@[simp]theorem i: inv (&⟨a,b,h⟩)=if h:a>0then&⟨b,a,h⟩else 0:=rfl
variable(a b c d:Q)
theorem add_comm:a+b=b+a:=k a,b
theorem add_assoc:a+b+c=a+(b+c):=k a,b,c
theorem mul_comm:a*b=b*a:=k a,b
theorem mul_assoc:a*b*c=a*(b*c):=k a,b,c
theorem mul_add:a*(b+c)=a*b+a*c:=k a,b,c
theorem sub_self:a-a=0:=k a
theorem add_sub:a+b-b=a:=k a,b
theorem le_refl:a≤a:=k a
theorem le_trans:a≤b→b≤c→a≤c:=by i a,b,c;p;a Nat.le_of_mul_le_mul_left _ b_2;p;a Nat.le_trans (Nat.mul_le_mul_left a_2 a_7);have:=Nat.mul_le_mul_right a_6 a_8;p
theorem le_antisymm:a≤b→b≤a→a=b:=k a,b
theorem le_total:a≤b∨b≤a:=k a,b
theorem add_zero:a+0=a:=k a
theorem mul_zero:a*0=0:=k a
theorem mul_one:a*1=a:=k a
theorem add_le_add_left:a≤b→c+a≤c+b:=k a,b,c
theorem le_of_add_le_add_left:c+a≤c+b→a≤b:=k a,b,c
theorem zero_ne_one:(0:Q)≠1:=p
theorem zero_le_one:(0:Q)≤1:=p
theorem mul_le_mul_left:a≤b→c*a≤c*b:=k a,b,c
theorem mul_lt_mul_of_pos_left:a<b→0<c→c*a<c*b:=k a,b,c
@[simp]theorem inv_zero:inv 0=0:=p
theorem inv_mul:a≠0→a*inv a=1:=by i a;p;split;p

[Kevin Buzzard]

This code is exactly an example of why I think "let's try and minimise total character count" is a terrible idea and I honestly would encourage people to think about whether we want to encourage more generation of this artificially compressed nonsense just because of some stupid target.

[Kevin Buzzard]

I think the question should be "let's write code normally and then have a look at how long it is and draw some broad conclusions" as opposed to "let's have a competition to see how few characters we can squeeze a development into and then draw a conclusion which has very little value and has resulted in the generation of a bunch of horrible code"

[Kevin Buzzard]

macro"&"e:term:99:term=>`((Quotient.mk _ $e :Q))
...
@[simp]theorem o:(1:Q)=&⟨1,1,p⟩ := rfl

Do we really want to see this sort of thing when studying what is an interesting question? It's only a matter of time before we define some random non-ASCII character to mean theorem if we go down this route.

[Damiano Testa]

At least, the code should follow Mathlib's style guidelines and naming conventions.

[Damiano Testa]

If "ready for Mathlib" were a serious definition, I would probably vote for that!

[Vlad Tsyrklevich]

Kevin Buzzard said:

It's only a matter of time before we define some random non-ASCII character to mean theorem

This is a good idea

[Vlad Tsyrklevich]

Committing atrocities feels like 90% of the fun of code golf

[Vlad Tsyrklevich]

I think this is a matter of personal taste. I've always enjoyed the International Obfuscated C Code Contest (IOCCC) for this reason.

[Daniel Weber]

Kevin Buzzard said:

I think the question should be "let's write code normally and then have a look at how long it is and draw some broad conclusions" as opposed to "let's have a competition to see how few characters we can squeeze a development into and then draw a conclusion which has very little value and has resulted in the generation of a bunch of horrible code"

My purpose in this is not to draw conclusion about the mathematics, it's to have fun by trying the push the limits of the language. I think that seeing and experimenting with abusing the language can teach you a lot about regular usage of the language

[Daniel Weber]

From a mathematical perspective I believe code golf also gives goals that aren't the usual goals when exploring mathematics, which can push developments in strange and interesting ways

[Johan Commelin]

I also conjecture that we can still get a pretty good answer to the mathematically interesting questions even if the code is golfed.

[Kevin Buzzard]

Well if this is supposed to be "the point" then sure just do what you like :-) I had thought the point was to generate some interesting formalizations of various ways of making the real numbers, but right now I fear that they're all going to be unreadable rather than something I can show to students. But I had not understood that the question was actually motivation for all this code golf silliness.

[Johan Commelin]

One persons silliness, is another persons delight (-;

[Kevin Buzzard]

Yes that's my conclusion on reading this thread!

[Johan Commelin]

You should talk to Kolmogorov (-;

[Johan Commelin]

The patron saint of code golfers

[Kim Morrison]

It's a pity that an actually interesting question "how to construct the reals cheaply" would be wasted as a code golfing game. My vote is definitely with Kevin --- let's do this in as little code as possible, but following Mathlib style guides and naming.

[Johan Commelin]

We have two sets $\R_m$ and $\R_g$:

• $\R_g$ consists of all constructions of $\R$ and is partially ordered by length of the construction
• $\R_m$ consists of all constructions of $\R$ that follow Mathlib style guides and conventions, and is partially ordered by the length of the construction

There is a natural "golfing function" from $\R_m$ to $\R_g$.

Conjecture:

For any two elements $c_1 \le c_2$ of $\R_g$, there exists a lift $m_1 \in \R_m$ of $c_1$ that is smaller than all lifts of $c_2$.

[Johan Commelin]

In other words, I think we can run both challenges, and they will be practically equivalent.

[Ruben Van de Velde]

Sets or types?

[Daniel Weber]

As a mathematical statement I definitely don't think that's true, but I mostly agree with the idea

[Johan Commelin]

I'm quite sure counterexamples to my conjecture exist. One reason to make the conjecture is that I would love to see a counterexample (-;

[Daniel Weber]

There's a fair chance there's no provable counterexample due to Chaitin's incompleteness theorem, although I don't know how that's affected by Lean not being Turing-Complete

[Edward van de Meent]

huh? lean is not turing complete? whatever gave you that idea?

[Daniel Weber]

If you don't use partial/unsafe/axiom you can only run programs that you can prove termination for using Lean's axiom

[Edward van de Meent]

right, but we can use partial/unsafe/axiom

[Daniel Weber]

I was implicitly thinking about the fragment without them, I guess

[Edward van de Meent]

i suspect lean's macro system might be turing complete, actually

[Daniel Weber]

That makes sense, you can probably implement lambda calculus using them

[Niels Voss]

Would the solution be required to live in Type, or can it be in something like Type 1? I suspect taking a subtype of the Surreals might save some space because it avoids the need to define the rationals

[Niels Voss]

It might even be interesting to see what the shortest definition of a type equivalent to the reals, where the proof of equivalence isn't counted

[Yakov Pechersky]

What does "type equivalent to the reals" mean, if there is no proof obligation to show equivalence? Is there an obligation to construct the Field instance?

[Yakov Pechersky]

Because if there isn't, then here is an infinite family of reals (see #13965):

import Mathlib.Order.Fin.Basic
import Mathlib.Order.SuccPred.Archimedean
import Mathlib.Tactic.Ring

open Order

/-- A possibly infinite sequence of digits in `Fin (b + 1)`, which
can represent a number system like the reals.
It is constrained to not end in an infinite string of the top digit. -/
structure DigitExpansion (Z : Type*) [LT Z] (b : ℕ) where
  /-- The digit sequence, such that `b` is the base - 1. -/
  toFun : Z → Fin (b + 1)
  /-- The constraint that the sequence does not trail end infinitely at the top digit. -/
  bounded' : ¬∃ i₀, ∀ i > i₀, toFun i = b

namespace DigitExpansion

instance funLike (Z : Type*) [LT Z] (b : ℕ) : FunLike (DigitExpansion Z b) Z (Fin (b + 1))
    where
  coe := DigitExpansion.toFun
  coe_injective' := by rintro ⟨⟩ ⟨⟩; simp

variable (Z : Type*) [LinearOrder Z] [SuccOrder Z] [NoMaxOrder Z] [PredOrder Z] [NoMinOrder Z]
    [IsSuccArchimedean Z] (b : ℕ) [hb : NeZero b]

instance {Z : Type*} [Preorder Z] [SuccOrder Z] [NoMaxOrder Z] {b : ℕ} [hb : NeZero b] :
    Zero (DigitExpansion Z b) :=
  ⟨{  toFun := (0 : Z → Fin (b + 1))
      bounded' := by
        push_neg
        intro x
        refine' ⟨succ x, lt_succ _, _⟩
        simp [Fin.ext_iff, hb.out.symm] }⟩

section sign

variable {Z : Type*} [Preorder Z] [SuccOrder Z] [NoMaxOrder Z] {b : ℕ} [NeZero b]
    (f : DigitExpansion Z b)

/-- A sequence is positive iff it is not zero and has a left-tail of solely digit 0. -/
protected def Positive : Prop :=
  f ≠ 0 ∧ ∃ x, ∀ y < x, f y = 0

/-- A sequence is negative iff it is not zero and has a left-tail of solely the top digit. -/
protected def Negative : Prop :=
  f ≠ 0 ∧ ∃ x, ∀ y < x, f y = b

end sign

/-- A sequence is called real if it is either negative or zero or positive.
-/
def real : Set (DigitExpansion Z b) := {f | f.Positive ∨ f.Negative ∨ f = 0}

end DigitExpansion

[Niels Voss]

Sorry, I wasn't clear. I meant that you still have to show it is isomorphic to the reals; it's just that those proofs don't count to the character count or whatever metric

[Niels Voss]

On second thought, this isn't a great idea because then people would just do def Real := Set Nat

[Eric Wieser]

Set Nat doesn't give you the field or order structure though, right?

[Dean Young]

@Niels Voss but this does not have the correct cardinality.

[Kevin Buzzard]

Sure it does

[Edward van de Meent]

Set Nat is equivalent to Nat -> Prop, which is equivalent to Nat -> Fin 2, meaning it has cardinality 2^ω, the same as Real

[Elliot]

Oh sorry I see now.

Here's my attempt:

-- constructing the nonnegative extended real numbers using a preorder on Nat × Nat and cancelation of natural number multiplication

-- makeshift preorder structure
structure preorder where
  Obj : Type
  Hom : Obj → Obj → Prop
  Idn : (X : Obj) → (Hom X X)
  Cmp : (X : Obj) → (Y : Obj) → (Z : Obj) → (f : Hom X Y) → (g : Hom Y Z) → (Hom X Z)
-- https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Init/Order/Defs.lean#L37-L41$0

-- makeshift order preserving function
structure order_preserving_function (X : preorder) (Y : preorder) where
  Obj : X.Obj → Y.Obj


--The preorder constructed below has n₁/m₁ ≠ n₂/m₂ when either n₁ ≠ n₂ or m₁ ≠ m₂, so I call it "the nonnegative prerationals".

def preorder_of_nonnegative_prerationalsObj : Type := Nat × Nat

def preorder_of_nonnegative_prerationalsHom (X : preorder_of_nonnegative_prerationalsObj) (Y : preorder_of_nonnegative_prerationalsObj) : Prop := (X.fst * Y.snd ≤ Y.fst * X.snd)

def preorder_of_nonnegative_prerationalsIdn : (X : preorder_of_nonnegative_prerationalsObj) → (preorder_of_nonnegative_prerationalsHom X X) := by
unfold preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
simp


def preorder_of_nonnegative_prerationals_lemma : (X : preorder_of_nonnegative_prerationalsObj) → (Y : preorder_of_nonnegative_prerationalsObj) → (Z : preorder_of_nonnegative_prerationalsObj) → (f : preorder_of_nonnegative_prerationalsHom X Y) → (g : preorder_of_nonnegative_prerationalsHom Y Z) → (X.1 * Z.2 * (Y.2)) ≤ (X.2 * X.1 * (Y.2)) := by
unfold  preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
simp


def preorder_of_nonnegative_prerationalsCmp : (X : preorder_of_nonnegative_prerationalsObj) → (Y : preorder_of_nonnegative_prerationalsObj) → (Z : preorder_of_nonnegative_prerationalsObj) → (f : preorder_of_nonnegative_prerationalsHom X Y) → (g : preorder_of_nonnegative_prerationalsHom Y Z) → preorder_of_nonnegative_prerationalsHom X Z := by
unfold  preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
sorry

def preorder_of_nonnegative_prerationals : preorder := {Obj := preorder_of_nonnegative_prerationalsObj, Hom := preorder_of_nonnegative_prerationalsHom, Idn := preorder_of_nonnegative_prerationalsIdn, Cmp := preorder_of_nonnegative_prerationalsCmp}

def two_element_preorderObj : Type := Prop

def two_element_preorderHom (X : two_element_preorderObj) (Y : two_element_preorderObj) : Prop := X → Y

def two_element_preorderIdn (X : two_element_preorderObj) : two_element_preorderHom X X  := by
unfold two_element_preorderHom
simp

def two_element_preorderCmp : (X : two_element_preorderObj) → (Y : two_element_preorderObj) → (Z : two_element_preorderObj) → (f : two_element_preorderHom X Y) → (g : two_element_preorderHom Y Z) → (two_element_preorderHom X Z) := by sorry

--
def two_element_preorder : preorder := {Obj := two_element_preorderObj, Hom := two_element_preorderHom, Idn := two_element_preorderIdn, Cmp := two_element_preorderCmp}


def inequality_of_order_preserving_functions (X : preorder) (Y : preorder) (f : order_preserving_function X Y)  (g : order_preserving_function X Y) : Prop := by sorry

def reflexivity_for_order_preserving_functions (X : preorder) (Y : preorder) (f : order_preserving_function X Y) : inequality_of_order_preserving_functions X Y f f := by sorry

def transitivity_for_order_preserving_functions (X : preorder) (Y : preorder) (f₁ : order_preserving_function X Y) (f₂ : order_preserving_function X Y) (f₃ : order_preserving_function X Y) (i₁ : inequality_of_order_preserving_functions X Y f₁ f₂) (i₂ : inequality_of_order_preserving_functions X Y f₂ f₃) : inequality_of_order_preserving_functions X Y f₁ f₃ := by sorry

def preorder_of_order_preserving_functions (X : preorder) (Y : preorder) : preorder := {Obj := order_preserving_function X Y, Hom := inequality_of_order_preserving_functions X Y, Idn := reflexivity_for_order_preserving_functions X Y, Cmp :=transitivity_for_order_preserving_functions X Y }


def preorder_of_nonnegative_extended_reals : preorder := preorder_of_order_preserving_functions preorder_of_nonnegative_prerationals two_element_preorder

notation "[0,∞]" => preorder_of_nonnegative_extended_reals

#check [0,∞]

I have made only little progress but I am still a beginner.

[Elliot]

Sorry, that one has division by 0. One can use successor to fix that.

-- constructing the nonnegative extended real numbers using a preorder on Nat × Nat and cancelation of natural number multiplication

-- makeshift preorder structure
structure preorder where
  Obj : Type
  Hom : Obj → Obj → Prop
  Idn : (X : Obj) → (Hom X X)
  Cmp : (X : Obj) → (Y : Obj) → (Z : Obj) → (f : Hom X Y) → (g : Hom Y Z) → (Hom X Z)
-- https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Init/Order/Defs.lean#L37-L41$0

-- makeshift order preserving function
structure order_preserving_function (X : preorder) (Y : preorder) where
  Obj : X.Obj → Y.Obj


--The preorder constructed below has n₁/m₁ ≠ n₂/m₂ when either n₁ ≠ n₂ or m₁ ≠ m₂, so I call it "the nonnegative prerationals".

def preorder_of_nonnegative_prerationalsObj : Type := Nat × Nat

def preorder_of_nonnegative_prerationalsHom (X : preorder_of_nonnegative_prerationalsObj) (Y : preorder_of_nonnegative_prerationalsObj) : Prop := (X.fst * (Y.snd+1) ≤ Y.fst * (X.snd+1))

def preorder_of_nonnegative_prerationalsIdn : (X : preorder_of_nonnegative_prerationalsObj) → (preorder_of_nonnegative_prerationalsHom X X) := by
unfold preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
simp

/-
def preorder_of_nonnegative_prerationals_lemma : (X : preorder_of_nonnegative_prerationalsObj) → (Y : preorder_of_nonnegative_prerationalsObj) → (Z : preorder_of_nonnegative_prerationalsObj) → (f : preorder_of_nonnegative_prerationalsHom X Y) → (g : preorder_of_nonnegative_prerationalsHom Y Z) → (X.1 * Z.2 * (Y.2)) ≤ (X.2 * X.1 * (Y.2)) := by
unfold  preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
simp
-/

def preorder_of_nonnegative_prerationalsCmp : (X : preorder_of_nonnegative_prerationalsObj) → (Y : preorder_of_nonnegative_prerationalsObj) → (Z : preorder_of_nonnegative_prerationalsObj) → (f : preorder_of_nonnegative_prerationalsHom X Y) → (g : preorder_of_nonnegative_prerationalsHom Y Z) → preorder_of_nonnegative_prerationalsHom X Z := by
unfold  preorder_of_nonnegative_prerationalsObj
unfold  preorder_of_nonnegative_prerationalsHom
sorry

def preorder_of_nonnegative_prerationals : preorder := {Obj := preorder_of_nonnegative_prerationalsObj, Hom := preorder_of_nonnegative_prerationalsHom, Idn := preorder_of_nonnegative_prerationalsIdn, Cmp := preorder_of_nonnegative_prerationalsCmp}

def two_element_preorderObj : Type := Prop

def two_element_preorderHom (X : two_element_preorderObj) (Y : two_element_preorderObj) : Prop := X → Y

def two_element_preorderIdn (X : two_element_preorderObj) : two_element_preorderHom X X  := by
unfold two_element_preorderHom
simp

def two_element_preorderCmp : (X : two_element_preorderObj) → (Y : two_element_preorderObj) → (Z : two_element_preorderObj) → (f : two_element_preorderHom X Y) → (g : two_element_preorderHom Y Z) → (two_element_preorderHom X Z) := by sorry

--
def two_element_preorder : preorder := {Obj := two_element_preorderObj, Hom := two_element_preorderHom, Idn := two_element_preorderIdn, Cmp := two_element_preorderCmp}


def inequality_of_order_preserving_functions (X : preorder) (Y : preorder) (f : order_preserving_function X Y)  (g : order_preserving_function X Y) : Prop := by sorry

def reflexivity_for_order_preserving_functions (X : preorder) (Y : preorder) (f : order_preserving_function X Y) : inequality_of_order_preserving_functions X Y f f := by sorry

def transitivity_for_order_preserving_functions (X : preorder) (Y : preorder) (f₁ : order_preserving_function X Y) (f₂ : order_preserving_function X Y) (f₃ : order_preserving_function X Y) (i₁ : inequality_of_order_preserving_functions X Y f₁ f₂) (i₂ : inequality_of_order_preserving_functions X Y f₂ f₃) : inequality_of_order_preserving_functions X Y f₁ f₃ := by sorry

def preorder_of_order_preserving_functions (X : preorder) (Y : preorder) : preorder := {Obj := order_preserving_function X Y, Hom := inequality_of_order_preserving_functions X Y, Idn := reflexivity_for_order_preserving_functions X Y, Cmp :=transitivity_for_order_preserving_functions X Y }


def preorder_of_nonnegative_extended_reals : preorder := preorder_of_order_preserving_functions preorder_of_nonnegative_prerationals two_element_preorder

notation "[0,∞]" => preorder_of_nonnegative_extended_reals

#check [0,∞]

[Dean Young]

A second submission I'm preparing uses the circle and inductive types.

That makes me think, @Johan Commelin's comment on term length would be easier to make sense of if we restricted to inductive types.

Edit: I probably won't have time for it

[Niels Voss]

Has anyone actually completed a minimal ConditionallyCompleteLinearOrderedField, or does anyone have an estimate for how many lines such an instance should take? I started to attempt a construction of the Eudoxus reals, figuring that it might be easier since it skips the rationals, but I'm already at over 100 lines and am not anywhere close to done, mostly due to technical theorems about how operations preserve certain invariants and respect quotients.

I'm starting to think that the Eudoxus reals weren't such a good choice, but this might not be the case if every construction of the reals has the same issue.

[Markus Himmel]

A quick search turned up a (non-golfed) 2700-line construction of the Eudoxus reals in Lean 3: https://github.com/Lix0120/eudoxus/blob/master/src/def.lean, so that could be seen as an upper bound.

[Niels Voss]

That seems to import a bunch of stuff from mathlib though, whereas I was trying to use only stuff in Init

[Niels Voss]

but I was mainly wondering whether or not Eudoxus reals would better or worse than Dedekind cuts or Cauchy sequences

[Daniel Weber]

I'm currently working on defining R by constructing the nonnegative real numbers and then defining the real numbers as a quotient on pairs, but I'm a bit unsure about proving the completeness of the result. It can be done by splitting to positive and negative cases, but is there a nicer way to do this?

[Dean Young]

@Daniel Weber You could take one of the elements of the pair to be a natural number I think.

[Dean Young]

Also, I notice that if one completes ℚ then we can start with pairs (ℤ, ℕ≥1) and no equivalence relation.

[Dean Young]

Daniel Weber said:

@_E. Dean Young|559197 said:

One could also count with respect to l². The idea here is convenient for defining the norm on Rn.

What does this mean?

I don't have a very good answer, but l² is a complete preHilbert space. The preHilbert space structure defines a topology, but to be specific I would like the complete preHilbert space of square summable sequences on the natural numbers. This accompanied the thought that each ℝⁿ would be constructed without use of the others.

Starting with ℚ is an option, which I would construct from ℤ by adding in n!⁻¹ for n ≥ 1. In Lie-algebra valued differential forms, there is something called the Kobayashi convension in the antisymmetrization of an endomorphism, which works in any characteristic because it involves choosing an order on basis elements of the exterior algebra, featuring only one representative in each sum. What would ordinarily be division by n! is simply summing after choosing an order.

This reflects how one could use ℚ while paying close attension to how the Kobayashi convension works in any characteristic.

In ℚ one adds in n!⁻¹ for each n, but in antisymmetrized representations of a Lie-algebra under the Kobayashi convension, one always has used divisibility by n!.

This is probably related to Σₙ ch₁ⁿ/n! in some way I don't understand. Take G = GLₙ(ℂ) and 𝔤 = 𝔤𝔩ₙ(ℂ) and consider the Lie-algebra valued differential forms such as d v + (1/2)[v ∧ v]; the exterior product of lie-algebra valued differential forms is a monoid object in complexes without the square-zero condition, and that half is not necessary in the sum when one chooses an order on certain subtypes of cardinality 2.

So somehow Lie-algebra valued differential forms feature antisymmetrization without division by n!, while ℚ bears a close relationship with the "Chern-Weil type setup", in which one can consider the chern character in which one needs the coefficients to exponentiate.

Somehow I think that passage from the Lie-algebra world to the Lie-group world satisfies my curiosity about how to first form the rationals. I seem to think that adding in 1/n! to ℤ is best and that the tensor product of an algebraic group with ℤ[1/n!] (i.e. the pullback with its geometric content) produces a unique kind of categorical equivalence or bridge.

Given (f : Nat → ℚ)×(_ : ∃(n : Nat),∀(m : Nat),∀(p : n ≤m),f m = 0 we can construct a ℚ-linear map from ℚⁿ ⊗ ℚⁿ into ℚⁿ. To construct ℝ or ℝⁿ from this I might like to start from the open sets of ℚⁿ with respect to the metric this induces.

[Dean Young]

Someone who understands this better can correct me but the above could be saying, "rational coefficients for cohomology are the smallest possible choice of ring (or A-infinity ring!) in which the Chern character exists".

The Chern character is most easily defined in the presence of a connection using Lie-algebra-valued differential forms, and this produces a monoid object in complexes instead of having the usual chain (square zero) condition, and the powers of the curvature form go to the Chern classes under the Chern-Weil homomorphism. These are the integral generators of [BGLₙ(ℂ),ΠₙBⁿℝ] and reside in [BGLₙ(ℂ),ΠₙBⁿℤ].

[Dean Young]

From here one can consider how the Chern character is a "symmetrization", sort of the opposite of the antisymmetrization that takes place in the Lie-algebra valued differential forms.

[Dean Young]

In conclusion, after all of that abstraction, it feels more elegant to use ℕ[n!⁻¹]

[Dean Young]

The method above describes how the completion of a preorder can be used as an alternative to an equivalence relation.

Here's how I'm going to proceed withℕ[n!⁻¹]:

I'll put an order on

ℕ × (a : ℕ → ℕ) × (terminates : ∃(n : Nat),∀(m : Nat),∀(p : n ≤m),a m = 0)

with the usual

factorial : ℕ → ℕ

and

product : (a : ℕ → ℕ) → (terminates : ∃(n : Nat),∀(m : Nat),∀(p : n ≤m),a m = 0) → ℕ.

we can define a function Φ to help with the inequality

a/(a₁! ⋯ aₙ!) ≤ b/(b₁! ⋯ bₙ!)

Specifically just taking (a, termination_proof) to a₁! ⋯ aₙ! ⋯ , which exists by the proof.

where (x₁, (a₁, t₁) ) ≤ (x₂, (a₂, t₂)) when x₁ * Φ ((a₂,t₂)) ≤ x₂ * Φ ((a₂,t₂)).

[Dean Young]

Then I can use the simple two object partial order above to get the non-negative extended reals without using any equivalence relation at all, and with a more elegant source of denomenators than the nonzero natural numbers: factorials of natural numbers!

[Dean Young]

I made a bit more of a mistake, not including powers of those.

[David Michael Roberts]

@Elliot Young is @Elliot also your account?

[Dean Young]

@David Michael Roberts Yeah- sorry for any confusion.

[David Michael Roberts]

Any other duplicate accounts we should know about?