algebraic structures

Stream: new members

[Patrick Thomas]

Is it possible, as an example, to define the notion of a group, prove properties that all groups have, prove that ℤ is a group under addition, and thus have proofs of those properties for ℤ under addition? The definition of a group that I know uses a set, so I'm not sure how that translates to type theory. Would a group be a type class?

[Kyle Miller]

Type classes are a feature that let you attach structure to already existing things. Group structures are a perfect use for type classes.

[Patrick Thomas]

My first thought was like

structure group (α : Type) (S : set α) (op : α → α → α) :=
(closure : ∀ a b ∈ S, (op a b ∈ S))
(assoc: ∀ a b c ∈ S, (op (op a b) c) = (op a (op b c)))
(e : α)
(h : e ∈ S)
(ident_1: ∀ a ∈ S, (op e a) = a)
(ident_2: ∀ a ∈ S, (op a e) = a)
(inv_1 : ∀ a ∈ S, ∃ b ∈ S, op a b = e)
(inv_2 : ∀ a ∈ S, ∃ b ∈ S, op b a = e)

But then a set didn't seem right.

[Kyle Miller]

With classes, it's this sort of setup:

class group (G : Type*) :=
(op : G → G → G)
(unit : G)
(inv : G → G)
(assoc : ∀ {x y z : G}, op x (op y z) = op (op x y) z)
(op_unit : ∀ {x : G}, op x unit = x)
(unit_op : ∀ {x : G}, op unit x = x)
(op_inv : ∀ {x : G}, op x (inv x) = unit)
(inv_op : ∀ {x : G}, op (inv x) x = unit)

instance : group ℤ :=
{op := (+),
 unit := 1,
 inv := λ x, -x,
 ...
}

[Patrick Thomas]

Inverse is a function?

[Kyle Miller]

You can define a group as an operation on a set, but with Lean you can lift sets up to being types (with subtype), so you may as well work with an operation on a type.

[Kyle Miller]

I made inverse be a function, but you can use classical.some and the rest with your inv_1 axiom to define it.

[Kyle Miller]

My definition is the constructible version, since to form a group you would need to show you can give an explicit inverse function. If you only care about classical reasoning, then this distinction doesn't matter.

[Kyle Miller]

(By the way, type classes are just structures, but they plug into a special mechanism that lets Lean automatically locate relevant terms (called instances) of the structure.)

[Patrick Thomas]

Thank you. I'll see if I can make the classical version as you described.

[Patrick Thomas]

Actually, that is really cool.

[Kyle Miller]

Here's an example of a generic lemma to get you started, if you didn't know the syntax already:

open group

lemma unit_unique {G : Type*} [group G] (unit' : G)
  (h_left : ∀ x, op unit' x = x) :
  unit' = unit :=
begin
  transitivity op unit' unit,
  rw op_unit,
  rw h_left,
end

[Patrick Thomas]

Thank you!

[Kyle Miller]

I forgot the open group line. This takes everything that's inside the group namespace (i.e., the fields of group) and makes them accessible without needing to write things like group.op.

[Patrick Thomas]

Did you mean that the classical version is just:

class group_classical (G : Type*) :=
(op : G → G → G)
(unit : G)
(assoc : ∀ {x y z : G}, op x (op y z) = op (op x y) z)
(op_unit : ∀ {x : G}, op x unit = x)
(unit_op : ∀ {x : G}, op unit x = x)
(op_inv : ∀ {x : G}, ∃ {b : G}, op x b = unit)
(inv_op : ∀ {x : G}, ∃ {b : G}, op b x = unit)

and that it is the instance that would have to use classical.some?

[Mario Carneiro]

actually you can drop the unit too

[Mario Carneiro]

but the two inverses generally have to be in the same existential

[Mario Carneiro]

groups I think are special because you can prove that the left and right inverse are the same, but for weaker structures you have to assume this

[Patrick Thomas]

Sorry, do you know how I would fix the syntax here:

class total_order {T : Type*} :=
(le : T → T → Prop)
(asymm : ∀ a b : T, le a b ∧ le b a → a = b)
(trans : ∀ a b c : T, le a b ∧ le b c → le a c)
(conn : ∀ a b : T, le a b ∨ le b a)

def is_upper_bound {T : Type*} [total_order T] (S : set T) (t : T) : Prop :=
∀ s ∈ S, le s t

[Patrick Thomas]

They syntax for the is_upper_bound definition that is.

[Patrick Thomas]

I guess I just needed to change it to:
def is_upper_bound {T : Type*} [@total_order T] (S : set T) (t : T) : Prop := sorry.

[Reid Barton]

Change the binder type in total_order to (T : Type*) instead, otherwise you'll have to write @total_order every time.

[Patrick Thomas]

Ok.

[Patrick Thomas]

I know I could use rewrite, but I can't figure out why t6 and s8 don't check here:

class left_group (G : Type*) :=
(op : G → G → G)
(e : G)
(assoc : ∀ a b c : G, op a (op b c) = op (op a b) c)
(op_unit : ∀ a : G, op e a = a)
(op_inv : ∀ a : G, ∃ b : G, op b a = e)


open left_group


example {G : Type*} [left_group G] : ∀ a : G, ∃ a' : G, op a a' = e :=
have s1 : ∀ a : G, ∃ a' : G, op a' a = e := op_inv,
assume a : G,
have s2 : ∃ a' : G, op a' a = e := s1 a,
exists.elim s2 (
  assume a' : G,
  assume a1 : op a' a = e,
  let y := op a a' in
  have s3 : op y y = y := (
    have t1 : op y y = op (op a a') (op a a') := eq.refl (op y y),
    have t2 : op (op a a') (op a a') = op a (op a' (op a a')) := eq.symm (assoc a a' (op a a')),
    have t3 : op a' (op a a') = op (op a' a) a' := assoc a' a a',
    have t4 : op a (op a' (op a a')) = op a (op (op a' a) a') := eq.subst t3 (eq.refl (op a (op a' (op a a')))),
    have t5 : op a (op (op a' a) a') = op a (op e a') := eq.subst a1 (eq.refl (op a (op (op a' a) a'))),
    have t6 : op a (op e a') = op a a' := eq.subst (op_unit a') (eq.refl (op a (op e a'))),
    sorry
  ),
  have s4 : ∃ y' : G, op y' y = e := op_inv y,
  exists.elim s4 (
    assume y' : G,
    assume a2 : op y' y = e,
    have s5 : y = op e y := eq.symm (op_unit y),
    have s6 : op e y = op (op y' y) y := eq.subst (eq.symm a2) (eq.refl (op e y)),
    have s7 : op (op y' y) y = op y' (op y y) := eq.symm (assoc y' y y),
    have s8 : op y' (op y y) = op y' y := eq.subst s3 (eq.refl (op y' (op y y))),
    sorry
  )
)

[Kyle Miller]

Any reason you're not using tactics? Here's something you can do, for example:

    have t6 : op a (op e a') = op a a' := by rw op_unit,
    have s8 : op y' (op y y) = op y' y := by rw s3,

Though, here's how you can fix those two lines:

    have t6 : op a (op e a') = op a a' := eq.subst (op_unit a').symm (eq.refl (op a a')),
    have s8 : op y' (op y y) = op y' y := eq.subst s3.symm (eq.refl (op y' y)),

[Patrick Thomas]

Why doesn't it work the way I had it?

[Kyle Miller]

It seems like the one or more equalities might be backwards. I didn't look too carefully.

[Kyle Miller]

By the way, to save yourself some typing, you can use underscores in places where Lean can infer what should go there:

    have t6 : op a (op e a') = op a a' := eq.subst (op_unit a').symm (eq.refl _),
    have s8 : op y' (op y y) = op y' y := eq.subst s3.symm (eq.refl _),

There's even a function precisely for this called rfl:

    have t6 : op a (op e a') = op a a' := eq.subst (op_unit a').symm rfl,
    have s8 : op y' (op y y) = op y' y := eq.subst s3.symm rfl,

[Patrick Thomas]

Hmm.

[Kyle Miller]

In case you're not familiar with the dot notation: (op_unit a').symm is short for eq.symm (op_unit a'). Lean knows op_unit a' is an eq so it looks for something called symm in the eq namespace.

[Patrick Thomas]

I think I must be misunderstanding how eq.subst works. I'm trying to extrapolate from the example in https://leanprover.github.io/logic_and_proof/first_order_logic_in_lean.html#equality-and-calculational-proofs

[Kyle Miller]

Well, let's look at the type:

lemma eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b

This is saying, giving an equality a = b and that P a is true, then P b is true. Lean will try to figure out what P is automatically , and if you want to use eq.subst it can be useful using @eq.subst to explicitly give the P you want.

You have

op_unit a' : op e a' = a'

and you are trying to prove

op a (op e a') = op a a'

The issue is that in eq.subst (op_unit a') (eq.refl (op a (op e a'))), Lean doesn't figure out the correct P (I don't know it's algorithm to derive a P, so I have no idea why). I believe it happens to find

P := λ x, op a (op e a') = op a x

[Kyle Miller]

Oh, that's actually the P that you wanted, and Lean found a different one. This works:

    have t6 : op a (op e a') = op a a' := @eq.subst _ (λ x, op a (op e a') = op a x) _ _ (op_unit a') rfl,

[Patrick Thomas]

I see. Thank you.

[Patrick Thomas]

How do you define something like a subgroup with this form of definition?

class left_group (G : Type*) :=
(op : G → G → G)
(e : G)
(assoc : ∀ a b c : G, op a (op b c) = op (op a b) c)
(op_unit : ∀ a : G, op e a = a)
(op_inv : ∀ a : G, ∃ a' : G, op a' a = e)

[Adam Topaz]

I suggest to look at how subgroups are defined in mathlib docs#subgroup

[Patrick Thomas]

I had. I was confused that it referred to a set.

[Adam Topaz]

Well, a subgroup is a subset of a group such that blah blah blah...

[Adam Topaz]

set G is the type of subsets of a type G.

[Patrick Thomas]

Oh. I see. Thank you.

[Kyle Miller]

There is some coercion magic involved in making subgroups "be" groups. There's a has_coe_to_sort instance that turns the carrier set into a type, and then that type is given a group instance.

I think I extracted most of what goes into subobjects here, except for the copy and ext lemmas:

class foo (X : Type*) :=
(op : X → X)

open foo

structure subfoo (X : Type*) [foo X] :=
(carrier : set X)
(op_mem : ∀ x ∈ carrier, foo.op x ∈ carrier)

namespace subfoo
variables {X : Type*} [foo X]

instance : has_coe (subfoo X) (set X) := { coe := subfoo.carrier }

instance : has_mem X (subfoo X) := { mem := λ x Y, x ∈ (Y : set X) }

@[simp, norm_cast]
lemma mem_coe {Y : subfoo X} {x : X} : x ∈ (Y : set X) ↔ x ∈ Y := iff.rfl

@[simp, norm_cast]
lemma coe_coe (Y : subfoo X) : ↥(Y : set X) = Y := rfl

instance to_foo (Y : subfoo X) : foo Y := { op := λ x, ⟨op x.1, Y.op_mem x.1 x.2⟩ }

@[simp, norm_cast]
lemma coe_op {Y : subfoo X} (y : Y) : (↑(op y) : X) = op ↑y := rfl

@[simp, norm_cast]
lemma coe_mk {Y : subfoo X} (x : X) (hx : x ∈ Y) : ((⟨x, hx⟩ : Y) : X) = x := rfl

end subfoo

[Kyle Miller]

Then you'd probably also want to define the lattice of subobjects (take a look at the complete_lattice instance for subgroups).

[Patrick Thomas]

Thank you. I may have to come back to this when I understand more.

[Patrick Thomas]

Why doesn't the type of e match in this lemma definition?

class left_group_set (α : Type*) (S : set α) (op : α → α → α) :=
(closure : ∀ a b ∈ S, op a b ∈ S)
(assoc : ∀ a b c ∈ S, op (op a b) c = op a (op b c))
(e : α)
(h : e ∈ S)
(op_unit : ∀ a ∈ S, op e a = a)
(op_inv : ∀ a ∈ S, ∃ b ∈ S, op b a = e)

open left_group_set

lemma idempotent (α : Type*) (S : set α) (op : α → α → α) [left_group_set α S op] :
∀ a ∈ S, op a a = a → a = e := sorry

[Adam Topaz]

class left_group_set (α : Type*) (S : set α) (op : α → α → α) :=
(closure : ∀ a b ∈ S, op a b ∈ S)
(assoc : ∀ a b c ∈ S, op (op a b) c = op a (op b c))
(e : α)
(h : e ∈ S)
(op_unit : ∀ a ∈ S, op e a = a)
(op_inv : ∀ a ∈ S, ∃ b ∈ S, op b a = e)

open left_group_set

lemma idempotent (α : Type*) (S : set α) (op : α → α → α) [left_group_set α S op] :
∀ a ∈ S, op a a = a → a = (e S op) := sorry

[Adam Topaz]

e turns out to be a function which takes two explicit variables

[Patrick Thomas]

Because of the way I defined left_group_set with two parameters?

[Adam Topaz]

Yeah exactly.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Why if I move S and op into the body does e not need α. Why does it become implicit?

[Adam Topaz]

Because lean knows about \alpha from a (which has type \alpha).

[Adam Topaz]

When in doubt, you can just use #check e to see exactly what it's type is. Or maybe #check @e.

[Adam Topaz]

If you're trying to simulate subgroups, the usual way to do it is like this... (one sec, I'll write up some code)

[Patrick Thomas]

I think Kyle already did.

[Patrick Thomas]

I wanted to try proving a lemma with the set version and then coerceing it to the type version.

[Patrick Thomas]

So I didn't introduce α with curly brackets in the class definition, but it still took it as implicit for e?

[Adam Topaz]

Usually you would prove a lemma about groups, and deduce them for subgroups by proving that subgroups are groups.

[Adam Topaz]

I don't think I understand what you're trying to do here...

[Patrick Thomas]

I'm not looking at subgroups here. Well, maybe later. I just like that the set version requires the usual closure axiom, and wanted to try to use it.

[Adam Topaz]

Why are you defining a set version in the first place?

[Patrick Thomas]

Playing around I guess. It is the usual definition given in books, so I wanted to see if I could use it.

[Adam Topaz]

It's not the usual definition given in books though.

[Patrick Thomas]

It's not?

[Adam Topaz]

This is like defining a group to be the data of a set $\alpha$ and a subset $S$ of $\alpha$ such that $\alpha$ has a operation $op : \alpha \to \alpha \to \alpha$ and an element $e : \alpha$ such that $e \in S$ and such that the operation and $e$ induce a group structure on $S$.

[Patrick Thomas]

So instead we make α simulate the set in the usual definition right? Then the closure axiom becomes implicit right? I mainly wanted to have to prove things explicitly using the closure axiom.

[Adam Topaz]

import tactic

class left_group (α : Type*) :=
(op : α → α → α)
(e : α)
(op_assoc {a b c} : op (op a b) c = op a (op b c))
(e_op {a} : op e a = a)
(exists_linv (a) : ∃ b : α, op b a = e)

open left_group

structure sub_left_group (α : Type*) [left_group α] :=
(carrier : set α)
(op_mem {a b} : a ∈ carrier → b ∈ carrier → op a b ∈ carrier)
(e_mem : e ∈ carrier)
(linv_mem {a b} : op b a ∈ carrier → a ∈ carrier → b ∈ carrier)
-- I don't know what you want to actually put for linv_mem, but you get the point.

instance foo1 {α : Type*} [left_group α] : has_coe_to_sort (sub_left_group α) :=
⟨Type*,λ S, subtype S.carrier⟩

open sub_left_group

instance foo2 {α : Type*} [left_group α] {H : sub_left_group α} : left_group H :=
{ op := λ x y, ⟨op x.1 y.1, op_mem _ x.2 y.2⟩,
  e := ⟨e, e_mem _⟩,
  op_assoc :=
  begin
    rintros ⟨⟩ ⟨⟩ ⟨⟩,
    simp [op_assoc],
  end,
  e_op := begin
    rintros ⟨⟩,
    simp [e_op],
  end,
  exists_linv :=
  begin
    rintros ⟨⟩,
    rcases exists_linv a_val with ⟨b,hb⟩,
    have : b ∈ H.carrier,
    { refine linv_mem _ _ a_property,
      rw hb,
      apply e_mem },
    use ⟨b,this⟩,
    simpa,
  end }

[Adam Topaz]

That's a sketch.

[Patrick Thomas]

Or I should say the closure axiom is automatically included by the definition of op. I wanted to avoid making it automatic.

[Adam Topaz]

There is no closure axiom. A group operation is by definition just a function $\alpha \to \alpha \to \alpha$.

[Adam Topaz]

When you go to define a subgroup, you need an axiom that tells you the subset is closed under the operation.

[Patrick Thomas]

It usually has to be given that that function is closed (in the set version) right?

[Adam Topaz]

What is a closed function?

[Patrick Thomas]

Takes members of the set to members of the set.
https://proofwiki.org/wiki/Definition:Group
G0

[Adam Topaz]

This assumes all sets are subsets of some universe $\mathbb{U}$.

[Adam Topaz]

https://en.wikipedia.org/wiki/Binary_operation

[Adam Topaz]

I honestly don't know whether there is any mathematician out there that thinks of a group operation on a group $G$ as a function $\mu : G \times G \to \mathbb{U}$ into some universe $\mathbb{U}$ where $G$ is a subset of $\mathbb{U}$ and it just so happens that $\mu(g,h) \in G$ for all $g,h \in G$.

[Adam Topaz]

Maybe the model theorists will prove me wrong with their monster models ;)

[Adam Topaz]

But in any case, if you do go this route with $\mathbb{U}$, you would be really going against what type theory is all about, and it will be very difficult to work with the object you define.

[Adam Topaz]

Here's a definition of (sub)monoids, using this "subsets of the universe approach."

import tactic

variable {UNIVERSE : Type*}

class monoid' (G : set UNIVERSE) :=
(op : G → G → G)
(e : G)
(op_assoc {x y z} : op (op x y) z = op x (op y z))
(e_op {x} : op e x = x)
(op_e {x} : op x e = x)

open monoid'

structure submonoid' (G : set UNIVERSE) [monoid' G] :=
(H : set UNIVERSE)
(is_subset : H ⊆ G)
(op_mem {x y : G} : x.1 ∈ H → y.1 ∈ H → (op x y).1 ∈ H)
(e_mem : (e : G).1 ∈ H)

instance foo {G : set UNIVERSE} [monoid' G] {H : submonoid' G} : monoid' (H.H) :=
{ op := λ x y, ⟨(op ⟨x.1,H.is_subset x.2⟩ ⟨y.1,H.is_subset y.2⟩).1, H.op_mem x.2 y.2⟩,
  e := ⟨(e : G).1,H.e_mem⟩,
  op_assoc := sorry,
  e_op := sorry,
  op_e := sorry }

[Adam Topaz]

But again, I should stress that this is not the right way to go about defining monoids.

[Patrick Thomas]

Ok. Thank you.

[Kyle Miller]

The closure axiom for groups is a holdover from an earlier time, and in modern books on algebra it's omitted since it's superfluous like @Adam Topaz already explained. My understanding is that most groups arose from a pre-existing (associative) binary operation, for example matrix multiplication, and so you would want to restrict this operation to some subset of, following the example, invertible matrices that's closed under matrix multiplication.

Doing this from the modern point of view, you would first show that you can restrict your pre-existing binary operation to your set-of-interest $G$, and then from there you'd check the group axioms. In Lean, you can create a type from a set very easily. You can use a set anywhere Lean expects a type and it will be automatically coerced, and for places this doesn't work there's a coercion arrow ↥ for places this. You can also use subtype to explicitly convert predicates into types.

Here's an example of restricting the addition operation of the natural numbers to the set of natural numbers that are greater than or equal to some fixed natural number.

def ℕge (n : ℕ) := {m : ℕ | n ≤ m}

def ℕge.add {n : ℕ} (a b : ℕge n) : ℕge n :=
⟨a.1 + b.1, by { cases a, cases b, dsimp [ℕge] at *, linarith }⟩

The definition has two parts: the first is the operation, and the second is the proof of closure.

Checking the type, we see it's

ℕge.add : Π {n : ℕ}, ↥(ℕge n) → ↥(ℕge n) → ↥(ℕge n)

and the up-arrows indicate Lean has coerced each of the sets to types. There's some special notation for immediate coercion of a set constructed with set builder notation to a type, and that's using // instead of |:

↥{m : ℕ | n ≤ m} = {m : ℕ // n ≤ m}

[Patrick Thomas]

The closure axiom is superfluous because we can prove interesting things without it, and it can be moved from the definition of a group to a requirement of the operation on the set of interest?

[Kyle Miller]

Pretty much -- just to clarify a bit more, in the modern approach we're comfortable with the process of restricting functions to subsets as needed, so in the definition of a group we can simply state there is an operation $G\times G\to G$ that's associative, has an identity, and has left and right inverses. You only need to think about closure if you're restricting a pre-existing operation.

(Said differently, the old approach seems to start with a monoid, then you find a subset that forms a submonoid ("closure"), and then you prove the modern group axioms for this monoid. The first two steps are not essential in the definition of a group.)

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Why does it seem that I need to choose a class name other than group here, when I put it in a namespace?

import tactic

namespace hidden

class group' (G : Type*) :=
(op : G → G → G)
(unit : G)
(inv : G → G)
(assoc : ∀ x y z : G, op x (op y z) = op (op x y) z)
(unit_op : ∀ x : G, op unit x = x)
(inv_op : ∀ x : G, op (inv x) x = unit)


open group'


lemma idempotent {G : Type*} [group' G] : ∀ x : G, op x x = x → x = unit :=
assume x : G,
assume a1 : op x x = x,
let x' := inv x in
calc
x = op unit x : by exact eq.symm (unit_op x)
... = op (op x' x) x : by rw (inv_op x)
... = op x' (op x x) : by exact eq.symm (assoc x' x x)
... = op x' x : by rw a1
... = unit : by exact (inv_op x)

end hidden

[Reid Barton]

Lean doesn't know that you intended for open group to refer to the namespace hidden.group rather than group.

[Patrick Thomas]

Ah. Yes, changing it to hidden.group works. Thank you!

[Patrick Thomas]

If I define a field by extending the definition of a group, do I have to keep the names used by the group (op, e, etc.) in the definition of the field? If so, can I instead reuse the theorems proved for a group with a separate definition of a field?

namespace hidden


class group (G : Type) :=
(op : G → G → G)
(e : G)
(inv : G → G)
(assoc : ∀ x y z : G, op x (op y z) = op (op x y) z)
(op_unit_left : ∀ x : G, op e x = x)
(op_inv_left : ∀ x : G, op (inv x) x = e)


open hidden.group


lemma group.idempotent {G : Type} [group G] : ∀ x : G, op x x = x → x = e :=
assume x : G,
assume a1 : op x x = x,
let x' := inv x in
calc
x = op e x : by exact eq.symm (op_unit_left x)
... = op (op x' x) x : by rw (op_inv_left x)
... = op x' (op x x) : by exact eq.symm (assoc x' x x)
... = op x' x : by rw a1
... = e : by exact (op_inv_left x)


class field (F : Type) :=
(add : F → F → F)
(zero : F)
(add_inv : F → F)
(add_assoc : ∀ x y z : F, add x (add y z) = add (add x y) z)
(add_comm : ∀ x y : F, add x y = add y x)
(add_zero_left : ∀ x : F, add zero x = x)
(add_inv_left : ∀ x : F, add (add_inv x) x = zero)
(mul : F → F → F)
(one : F)
(mul_inv : F → F)
(mul_assoc : ∀ x y z : F, mul x (mul y z) = mul (mul x y) z)
(mul_comm : ∀ x y : F, mul x y = mul y x)
(mul_one_left : ∀ x : F, mul one x = x)
(mul_inv_left : ∀ x : F, ¬ x = zero → mul (mul_inv x) x = one)
(dist : ∀ x y z : F, mul x (add y z) = add (mul x y) (mul y z))


open hidden.field


lemma field.add_idempotent {F : Type} [field F] : ∀ x : F, add x x = x → x = zero := sorry


end hidden

[Reid Barton]

You actually can, with old_structure_cmd:

namespace hidden

set_option old_structure_cmd true

class group (G : Type) :=
(op : G → G → G)
(e : G)
(inv : G → G)
(assoc : ∀ x y z : G, op x (op y z) = op (op x y) z)
(op_unit_left : ∀ x : G, op e x = x)
(op_inv_left : ∀ x : G, op (inv x) x = e)


open hidden.group


lemma group.idempotent {G : Type} [group G] : ∀ x : G, op x x = x → x = e :=
assume x : G,
assume a1 : op x x = x,
let x' := inv x in
calc
x = op e x : by exact eq.symm (op_unit_left x)
... = op (op x' x) x : by rw (op_inv_left x)
... = op x' (op x x) : by exact eq.symm (assoc x' x x)
... = op x' x : by rw a1
... = e : by exact (op_inv_left x)


class field (F : Type) extends group F
  renaming
    op → add
    e → zero
    inv → add_inv
    assoc → add_assoc
    op_unit_left → add_zero_left
    op_inv_left → add_inv_left :=
(add_comm : ∀ x y : F, add x y = add y x)
(mul : F → F → F)
(one : F)
(mul_inv : F → F)
(mul_assoc : ∀ x y z : F, mul x (mul y z) = mul (mul x y) z)
(mul_comm : ∀ x y : F, mul x y = mul y x)
(mul_one_left : ∀ x : F, mul one x = x)
(mul_inv_left : ∀ x : F, ¬ x = zero → mul (mul_inv x) x = one)
(dist : ∀ x y z : F, mul x (add y z) = add (mul x y) (mul y z))


open hidden.field

lemma field.add_idempotent {F : Type} [field F] : ∀ x : F, add x x = x → x = zero :=
group.idempotent

end hidden

[Kevin Buzzard]

renaming doesn't seem to ever be used in mathlib!

[Reid Barton]

Yeah, I think I discovered this feature while trying to figure out why the a -> _x change was causing Lean to crash

[Patrick Thomas]

Nice! Is there a way I can make it work for mul too, with the condition on the mul_inv_left?

[Kevin Buzzard]

But a field isn't a group under multiplication

[Patrick Thomas]

I know, hence the condition.

[Kevin Buzzard]

If you add the condition then you're not putting a group structure on F.

[Patrick Thomas]

Ok.

[Reid Barton]

But if you also have a monoid class then I think you could extend both while renaming both.

[Kevin Buzzard]

You could make a new type, a subtype of F, and try to put a group structure on this, but before this will work you'll need to prove some theorems guaranteeing that the product of two non-zero things is non-zero etc.

[Reid Barton]

See https://github.com/leanprover-community/lean/blob/master/tests/lean/run/record10.lean (which also uses some other feature private which I don't know about).

[Patrick Thomas]

I'll try the monoid. Thank you!

[Patrick Thomas]

Hmm, it seems that a monoid defines both the left and right identity property, which a group and field do not.

[Kevin Buzzard]

there is no one definition of a group/field -- no "official list of axioms" (not least because mathematicians can't tell the difference between the left identity and right identity assertions for symmetry reasons). The left and right identity property are true in a group. If you don't want to add both as axioms then you could prove them from what you have decided to use as axioms.

[Patrick Thomas]

Would this be a correct definition of a complete ordered field, that is an axiomatic approach to defining the real numbers?

namespace hidden

class total_order (T : Type) :=
(le : T → T → Prop)
(le_asymm : ∀ {x y : T}, le x y → le y x → x = y)
(le_trans : ∀ {x y z : T}, le x y → le y z → le x z)
(le_conn : ∀ {x y : T}, le x y ∨ le y x)


class field (F : Type) :=
(add : F → F → F)
(zero : F)
(add_inv : F → F)
(add_assoc : ∀ x y z : F, add x (add y z) = add (add x y) z)
(add_comm : ∀ x y : F, add x y = add y x)
(add_zero_left : ∀ x : F, add zero x = x)
(add_inv_left : ∀ x : F, add (add_inv x) x = zero)
(mul : F → F → F)
(one : F)
(mul_inv : F → F)
(mul_assoc : ∀ x y z : F, mul x (mul y z) = mul (mul x y) z)
(mul_comm : ∀ x y : F, mul x y = mul y x)
(mul_one_left : ∀ x : F, mul one x = x)
(mul_inv_left : ∀ x : F, ¬ x = zero → mul (mul_inv x) x = one)
(dist_left : ∀ x y z : F, mul x (add y z) = add (mul x y) (mul x z))


class ordered_field (F : Type) extends field F, total_order F :=
(add_le : ∀ x y z : F, le x y → le (add x z) (add y z))
(mul_le : ∀ x y : F, le zero x → le zero y → le zero (mul x y))


open total_order

def is_ub {T : Type} [total_order T] (S : set T) (t : T) : Prop :=
∀ s ∈ S, le s t

def is_lub {T : Type} [total_order T] (S : set T) (t : T) : Prop :=
is_ub S t ∧ ∀ r : T, (is_ub S r → le t r)

class complete_ordered_field (F : Type) extends ordered_field F :=
(has_lub : ∀ S : set F, (∃ x : F, x ∈ S) → (∃ x : F, is_ub S x) → ∃ x : F, is_lub S x)

end hidden

[Alex J. Best]

Looks right to me, mathlib calls this property conditional completeness https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html

[Patrick Thomas]

Thank you.

[Yury G. Kudryashov]

docs#conditionally_complete_linear_order

[Alex J. Best]

I introduced condititonally_complete_linear_ordered_field in #3292 which should be equivalent to what you have, but haven't had time to finish it unfortunately.

[Patrick Thomas]

Unfortunately I'm struggling to find the similar smallest sets of axioms for the natural numbers and integers. I think the ordered_field definition fills that role for the rationals?

[Heather Macbeth]

https://en.wikipedia.org/wiki/Peano_axioms

[Patrick Thomas]

I was looking at that earlier, I'll give it another try. Thank you.

[Patrick Thomas]

Is this right for the natural numbers? add one n in ind is kind of ugly, but I'm not sure if I'm supposed to define succ here?

namespace hidden

class total_order (T : Type) :=
(le : T → T → Prop)
(le_asymm : ∀ {x y : T}, le x y → le y x → x = y)
(le_trans : ∀ {x y z : T}, le x y → le y z → le x z)
(le_conn : ∀ {x y : T}, le x y ∨ le y x)

open total_order

def lt {T : Type} [total_order T] (x y : T) : Prop := le x y ∧ ¬ x = y


class something (N : Type) extends total_order N :=
(zero : N)
(add : N → N → N)
(add_assoc : ∀ x y z : N, add x (add y z) = add (add x y) z)
(add_comm : ∀ x y : N, add x y = add y x)
(add_zero_left : ∀ x : N, add zero x = x)
(one : N)
(mul : N → N → N)
(mul_assoc : ∀ x y z : N, mul x (mul y z) = mul (mul x y) z)
(mul_comm : ∀ x y : N, mul x y = mul y x)
(mul_one_left : ∀ x : N, mul one x = x)
(dist_left : ∀ x y z : N, mul x (add y z) = add (mul x y) (mul x z))
(add_le : ∀ x y z : N, le x y → le (add x z) (add y z))
(mul_le : ∀ x y z : N, le x y → le (mul x z) (mul y z))
(zero_lt_one : lt zero one)
(ge_one : ∀ n : N, lt zero n → le one n)
(zero_min : ∀ n : N, le zero n)
(ind (P : N → Prop) : P zero ∧ (∀ n : N, (P n → P (add n one))) → ∀ n : N, P n)

end hidden

[Kenny Lau]

universes u v

set_option old_structure_cmd true
class natlike (α : Type u) extends has_zero α :=
(succ : α → α)
(succ_inj : function.injective succ)
(succ_ne_zero : ∀ x, succ x ≠ 0)
(ind : ∀ (P : α → Prop) (h0 : P 0) (ih : ∀ n, P n → P (succ n)), ∀ n, P n)

namespace natlike

variables (α : Type u) [natlike α]

def of_nat : ℕ → α
| 0     := 0
| (n+1) := succ (of_nat n)

theorem of_nat_inj : function.injective (of_nat α) :=
λ m, nat.rec_on m
  (λ n, nat.cases_on n (λ _, rfl) (λ n hn, (natlike.succ_ne_zero _ hn.symm).elim))
  (λ m ih n, nat.cases_on n (λ hm, (natlike.succ_ne_zero _ hm).elim)
    (λ n hmn, congr_arg nat.succ $ ih $ natlike.succ_inj hmn))

theorem of_nat_surj : function.surjective (of_nat α) :=
natlike.ind _ ⟨0, rfl⟩ $ λ x ⟨n, hn⟩, ⟨n+1, hn ▸ rfl⟩

end natlike

[Patrick Thomas]

This is a different kind of formulation right? It leaves out addition, multiplication and order?

[Mario Carneiro]

Well, as usual lean's axiomatics are too strong to allow for writing these things in a way that doesn't imply far more than you intended. You may as well define def natlike A := A ~= nat

[Mario Carneiro]

You can define addition, multiplication and order from kenny's structure, although addition and multiplication will be noncomputable (a concept foreign to PA) because there is no recursion principle

[Mario Carneiro]

You can define addition, multiplication and order from my version as well, and they will be computable, but you might wonder what other properties of nat you are inheriting, and the answer is "all of them, with all three formulations"

[Mario Carneiro]

in particular you can prove Con(PA) with any of these formulations, which should worry you

[Patrick Thomas]

I have to go to sleep. I'll try to think about this more tomorrow. Thank you.

[Patrick Thomas]

What does Con(PA) mean?

[Bryan Gin-ge Chen]

Consistency of PA

[Patrick Thomas]

Why is that worrying?

[Reid Barton]

I think the bigger worry is that you can prove that any instance of something is in fact isomorphic to nat

[Reid Barton]

if your goal was to define what a (first order!) model of PA is, that's presumably not what you wanted

[Reid Barton]

and the problem is that ind is way too strong because it applies to all P : N -> Prop, which includes everything that can be defined in Lean

[Reid Barton]

But, it's not clear to me that defining "model of PA" really is your goal

[Patrick Thomas]

I'm not sure. I defined the axioms for a complete ordered field so that I could use them to prove properties of the reals without having to define the reals. I was then going to do the same for the other number systems.

[Patrick Thomas]

Maybe that is a bad approach?

[Reid Barton]

In that case I think your definition is okay, but it might be longer than just defining nat, nat.add and nat.mul

[Patrick Thomas]

Yeah.

[Reid Barton]

while for the reals, the abstract description is simpler than the object being described

[Patrick Thomas]

Yeah.

[Patrick Thomas]

If I add this notation and use 0then I get an ambiguous overload. Is there a way to add this notation and avoid that when I am only working with my definition of a field?

notation x `+` y := add x y
notation 0 := zero

notation x `*` y := mul x y
notation 1 := one

[Kevin Buzzard]

What you are doing in this thread is that you are rewriting a whole bunch of things which are already in Lean, in your own way.

[Kevin Buzzard]

Lean has fields and groups, and they're done a bit differently to the way you've done them, but this isn't really a problem because your definitions can coexist with Lean's.

[Kevin Buzzard]

Lean has 0 and 1, and they're done a bit differently to the way you've done them, and this time it is a problem.

[Kevin Buzzard]

Instead of doing this part your own way, I would definitely recommend that you used Lean's way of doing it, which would be by adding instances of the has_zero, has_one, has_add and has_mul typeclasses.

[Kevin Buzzard]

e.g. instance : has_add X := \<add\> if add : X -> X -> X

[Patrick Thomas]

And then there is existing notation for has_add, etc.?

[Kevin Buzzard]

Or letting your field extend has_add like it's done in mathlib. You're working in some hidden namespace so you can define field in that namespace any way you like. But + is already taken, it means has_add.add, and this is clever, because it means you can use + on any type; all you have to do is to make it an instance of the has_add typeclass.

[Kevin Buzzard]

Right. has_add is in core Lean so it will always be imported, and + is notation for has_add.add.

[Kevin Buzzard]

You could either use some weird unicode + instead, or you could stick to the traditional method and add an instance.

[Patrick Thomas]

I'm sorry, what is the syntax? This doesn't seem to be working: instance : has_add hidden.field := ⟨hidden.field.add⟩.

[Kevin Buzzard]

MWE?

[Kevin Buzzard]

oh, you're missing an F

[Kevin Buzzard]

hidden.field is a function, which eats a type F and outputs the type of field structures on F

[Kevin Buzzard]

posting errors helps -- and learning to read them helps even more.

[Kevin Buzzard]

hmm

[Kevin Buzzard]

the usual way to do this would be to extend has_add.

[Patrick Thomas]

namespace hidden


class field (F : Type) :=
(add : F → F → F)
(zero : F)
(add_inv : F → F)
(add_assoc : ∀ x y z : F, add x (add y z) = add (add x y) z)
(add_comm : ∀ x y : F, add x y = add y x)
(add_zero_left : ∀ x : F, add zero x = x)
(add_inv_left : ∀ x : F, add (add_inv x) x = zero)
(mul : F → F → F)
(one : F)
(mul_inv : F → F)
(mul_assoc : ∀ x y z : F, mul x (mul y z) = mul (mul x y) z)
(mul_comm : ∀ x y : F, mul x y = mul y x)
(mul_one_left : ∀ x : F, mul one x = x)
(mul_inv_left : ∀ x : F, ¬ x = zero → mul (mul_inv x) x = one)
(dist_left : ∀ x y z : F, mul x (add y z) = add (mul x y) (mul x z))


instance : has_add hidden.field := ⟨hidden.field.add⟩

end hidden

[Kevin Buzzard]

instance (F : Type) [field F] : has_add F := ⟨hidden.field.add⟩

variables (F : Type) [field F] (x y : F)

#check x + y -- F

[Patrick Thomas]

Thank you!

[Mario Carneiro]

If you use extends has_add F in the definition of field, you can use the + notation even in the structure definition

[Patrick Thomas]

Ah. Ok.

[Patrick Thomas]

Nice.

class field (F : Type) extends has_add F, has_zero F, has_neg F, has_mul F, has_one F, has_inv F :=
(add_assoc : ∀ x y z : F, x + (y + z) = (x + y) + z)
(add_comm : ∀ x y : F, x + y = y + x)
(add_zero_left : ∀ x : F, 0 + x = x)
(add_neg_left : ∀ x : F, -x + x = 0)
(mul_assoc : ∀ x y z : F, x * (y * z) = (x * y) * z)
(mul_comm : ∀ x y : F, x * y = y * x)
(mul_one_left : ∀ x : F, 1 * x = x)
(mul_inv_left : ∀ x : F, ¬ x = 0 → x⁻¹ * x = 1)
(dist_left : ∀ x y z : F, x * (y + z) = (x * y) + (x * z))

[Kevin Buzzard]

Now you're really close to the import algebra.field definition.

[Kevin Buzzard]

In this repo here https://github.com/ImperialCollegeLondon/group-theory-game, me and some undergraduates defined a group ourselves in a random namespace, and then developed all of the theory of groups up to Sylow's theorems.

[Patrick Thomas]

Cool.

[Kevin Buzzard]

(my point is: I'm not suggesting that you use Lean's definition -- indeed I've worked with my own definitions before in order to teach people)

[Kenny Lau]

you are encouraged (by me) to include an axiom saying that the inverse of 0 is 0.

[Patrick Thomas]

Why? Isn't that undefined?

[Reid Barton]

Define undefined

[Patrick Thomas]

Contradictory? Or at least unexpected to most mathematicians?

[Mario Carneiro]

well, the axioms already imply it is a real number

[Mario Carneiro]

so if it's not 0, what is it?

[Bryan Gin-ge Chen]

If you haven't already seen it, here's a related blog post by Kevin: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Johan Commelin]

@Patrick Thomas How many field structures are there on the real numbers (with the usual addition and multiplication)?

[Patrick Thomas]

I don't know, it has been a long time since I studied abstract algebra, and I'm not sure if we covered this. Why?

[Patrick Thomas]

I'm not sure what field structure on the real numbers means.

[Mario Carneiro]

I think he is asking what is card (field real)

[Patrick Thomas]

Sorry, I'm not sure what that means either.

[Mario Carneiro]

field real is a type, whose elements are (0,1,+,*) tuples satisfying the field axioms

[Mario Carneiro]

the question is, how many such tuples are there, holding fixed that the base type is real and + and * are the usual ones

[Patrick Thomas]

I'm not sure what is allowed to vary.

[Mario Carneiro]

everything else: 0, 1, neg, inv, but whatever is chosen must be consistent with the addition and multiplication

[Mario Carneiro]

Here's a simpler version of the same question: how many group structures are there if you fix G and * but allow 1 and inv to vary?

[Patrick Thomas]

What does it mean to fix G?

[Kenny Lau]

Let (G, *, 1, inv) be a group. How many elements 1' : G and functions inv' : G -> G are there such that (G, *, 1', inv') is a group?

[Patrick Thomas]

If the operation (*) is fixed, doesn't that fix everything?

[Kevin Buzzard]

Indeed.

[Patrick Thomas]

I'm not sure I see where this leads.

[Reid Barton]

Now do the same thing for your definition of a field structure on real, fixing the definitions of 0, 1, add, mul to be the usual ones

[Patrick Thomas]

Ok. So there is only one possible inverse function because it is defined by mul?

[Johan Commelin]

Depends...

[Mario Carneiro]

That's what you would like to be true, but the key point is that it isn't true for your definition as stated

[Mario Carneiro]

do you see why?

[Patrick Thomas]

There are any number of elements it could take zero to.

[Reid Barton]

This is the meaning of

[Patrick Thomas]

We can just leave it undefined for 0 though. Why is that bad?

[Reid Barton]

In math we would say that $x^{-1}$ is undefined for $x = 0$. But in Lean, you wrote inv : F -> F so inv x is valid for every x : F.

[Patrick Massot]

Patrick, did you read that blogpost that was pointed out to you?

[Patrick Thomas]

Yeah, I was in the middle of it. I need to reread it a couple of times.

[Reid Barton]

One way to bring the Lean closer to the math version is to pin down the "bad" values by adding axioms like inv 0 = 0 (or inv 0 = 37) so that at least we're not providing more information in inv than there is in $x^{-1}$.

[Johan Commelin]

Patrick Thomas said:

We can just leave it undefined for 0 though. Why is that bad?

If I have two field extensions of degree two of real, are they isomorphic? What does it mean for two field extensions to be isomorphic?

[Mario Carneiro]

Another way, that is closer to the math version, is to define inv : \all x : F, x != 0 -> F, and then it really is undefined at zero. The blog post answers the question of why lean's version is more convenient

[Patrick Thomas]

This doesn't seem to work. For some reason the error gives the goal as has_inv ℕ.

namespace hidden


class field (F : Type) extends has_add F, has_zero F, has_neg F, has_mul F, has_one F, has_inv F :=
(add_assoc : ∀ x y z : F, x + (y + z) = (x + y) + z)
(add_comm : ∀ x y : F, x + y = y + x)
(add_zero_left : ∀ x : F, 0 + x = x)
(add_neg_left : ∀ x : F, -x + x = 0)
(mul_assoc : ∀ x y z : F, x * (y * z) = (x * y) * z)
(mul_comm : ∀ x y : F, x * y = y * x)
(mul_one_left : ∀ x : F, 1 * x = x)
(mul_inv_left : ∀ x : F, ¬ x = 0 → x⁻¹ * x = 1)
(dist_left : ∀ x y z : F, x * (y + z) = (x * y) + (x * z))
(zero_inv : 0⁻¹ = 0)

end hidden

[Patrick Thomas]

It seems I have to make the type of 0 explicit?

namespace hidden


class field (F : Type) extends has_add F, has_zero F, has_neg F, has_mul F, has_one F, has_inv F :=
(add_assoc : ∀ x y z : F, x + (y + z) = (x + y) + z)
(add_comm : ∀ x y : F, x + y = y + x)
(add_zero_left : ∀ x : F, 0 + x = x)
(add_neg_left : ∀ x : F, -x + x = 0)
(mul_assoc : ∀ x y z : F, x * (y * z) = (x * y) * z)
(mul_comm : ∀ x y : F, x * y = y * x)
(mul_one_left : ∀ x : F, 1 * x = x)
(mul_inv_left : ∀ x : F, ¬ x = 0 → x⁻¹ * x = 1)
(dist_left : ∀ x y z : F, x * (y + z) = (x * y) + (x * z))
(zero_inv : (0 : F)⁻¹ = 0)

end hidden

[Patrick Thomas]

I guess there is no other element in the definition to infer the type from?

[Yakov Pechersky]

Yes, by default, a numeric value like 0, 37 is assumed to be nat unless a different type can be inferred. Such inferring usually happens more on the RHS.

[Yakov Pechersky]

zero_inv can't know that your LHS will be about F as opposed to anything else.

[Patrick Thomas]

I see.

[Patrick Thomas]

So here there is no has_ge and has_gt to extend and I will end up with ambiguous overloads if I define the notation for them. Is there another way around it?

class total_order (T : Type) extends has_le T :=
(le_asymm : ∀ {x y : T}, x ≤ y → y ≤ x → x = y)
(le_trans : ∀ {x y z : T}, x ≤ y → y ≤ z → x ≤ z)
(le_conn : ∀ {x y : T}, x ≤ y ∨ y ≤ x)

[Kevin Buzzard]

Never ever use ge or gt?

[Kevin Buzzard]

(that's the approach used in mathlib)

[Kevin Buzzard]

Note that x >= y is just defined to mean y <= x, so you can use it if you want, but basically you end up doubling the number of lemmas in the <= part of the library for no obvious gain

[Patrick Thomas]

Hmm. I suppose.

[Kevin Buzzard]

In fact I think $\forall \epsilon>0$ might show up in some places -- somehow this was allowed, because $\forall 0 < \epsilon$ is a bit weird

[Yury G. Kudryashov]

I thought that it's allowed because Lean can't parse ∀ 0 < ε, p ε correctly and ∀ ε, 0 < ε → p ε is weird.

[Patrick Thomas]

Is there any way to disable the existing defined notation?

[Mario Carneiro]

you can use local notation

[Mario Carneiro]

but why would you want to do anything different than the core definition of ge?

[Mario Carneiro]

because it will be tremendously confusing if y >= x means anything other than x <= y

[Mario Carneiro]

Also, if you really want to reinvent lean core you might consider just slapping prelude at the top and rolling your own everything

[Patrick Thomas]

It was gt that I was going to change for symmetry to be similar to lt. I was going to make it def gt {T : Type} [total_order T] (x y : T) : Prop := x ≥ y ∧ ¬ x = y.

[Mario Carneiro]

if you have lt defined already, then gt should just work

[Yury G. Kudryashov]

Not having a > b for preorders looks strange.

[Yury G. Kudryashov]

I suggest that you add an iff lemma instead of changing the definition.

[Patrick Thomas]

What does prelude do exactly?

[Yury G. Kudryashov]

It prevents Lean from importing the default prelude library.

[Yury G. Kudryashov]

The one that comes with lean.

[Patrick Thomas]

I see.

[Yury G. Kudryashov]

Of course, if you use prelude, the you'll have to redo or import all parts of the prelude library you need.

[Patrick Thomas]

Hmm. Ok.

[Yury G. Kudryashov]

But I suggest reusing existing code as much as possible instead of reinventing wheels.

[Yury G. Kudryashov]

Unless you have some very special needs.

[Patrick Thomas]

Yeah, I was just hoping to keep these beautiful symmetric lemmas unchanged except for the notation :)

class total_order (T : Type*) :=
(le : T → T → Prop)
(le_asymm : ∀ {x y : T}, le x y → le y x → x = y)
(le_trans : ∀ {x y z : T}, le x y → le y z → le x z)
(le_conn : ∀ {x y : T}, le x y ∨ le y x)

open total_order


-- x < y
def lt {T : Type*} [total_order T] (x y : T) : Prop := le x y ∧ ¬ x = y

-- x ≥ y
def ge {T : Type*} [total_order T] (x y : T) : Prop := le y x

-- x > y
def gt {T : Type*} [total_order T] (x y : T) : Prop := ge x y ∧ ¬ x = y


lemma ne_symm {α : Type*} {x y : α} : ¬ x = y → ¬ y = x :=
assume a1 : ¬ x = y,
assume a2 : y = x,
have s1 : x = y := eq.symm a2,
show false, from a1 s1


lemma lt_to_gt {T : Type*} [total_order T] {x y : T} : lt x y → gt y x :=
assume a1 : lt x y,
have s1 : le x y := and.left a1,
have s2 : ge y x := s1,
have s3 : ¬ x = y := and.right a1,
have s4 : ¬ y = x := ne_symm s3,
and.intro s1 s4

lemma gt_to_lt {T : Type*} [total_order T] {x y : T} : gt x y → lt y x :=
assume a1 : gt x y,
have s1 : ge x y := and.left a1,
have s2 : le y x := s1,
have s3 : ¬ x = y := and.right a1,
have s4 : ¬ y = x := ne_symm s3,
and.intro s1 s4


lemma ge_asymm {T : Type*} [total_order T] {x y : T} : ge x y → ge y x → x = y :=
assume a1 : ge x y,
assume a2 : ge y x,
have s1 : le y x := a1,
have s2 : le x y := a2,
le_asymm s2 s1


lemma ge_trans {T : Type*} [total_order T] {x y z : T} : ge x y → ge y z → ge x z :=
assume a1 : ge x y,
assume a2 : ge y z,
have s1 : le y x := a1,
have s2 : le z y := a2,
le_trans s2 s1


lemma ge_conn {T : Type*} [total_order T] {x y : T} : ge x y ∨ ge y x :=
have s1 : le x y ∨ le y x := le_conn,
or.elim s1
(
  assume a1 : le x y,
  have s2 : ge y x := a1,
  or.intro_right (ge x y) s2
)
(
  assume a2 : le y x,
  have s3 : ge x y := a2,
  or.intro_left (ge y x) s3
)


lemma le_refl {T : Type*} [total_order T] {x : T} : le x x :=
have s1 : le x x ∨ le x x := le_conn,
or.elim s1
(
  assume a1 : le x x,
  a1
)
(
  assume a2 : le x x,
  a2
)

lemma ge_refl {T : Type*} [total_order T] {x : T} : ge x x :=
have s1 : ge x x ∨ ge x x := ge_conn,
or.elim s1
(
  assume a1 : ge x x,
  a1
)
(
  assume a2 : ge x x,
  a2
)


lemma not_lt_refl {T : Type*} [total_order T] {x : T} : ¬ lt x x :=
assume a1 : lt x x,
have s1 : ¬ x = x := and.right a1,
have s2 : x = x := eq.refl x,
show false, from s1 s2

lemma not_gt_refl {T : Type*} [total_order T] {x : T} : ¬ gt x x :=
assume a1 : gt x x,
have s1 : ¬ x = x := and.right a1,
have s2 : x = x := eq.refl x,
show false, from s1 s2


lemma le_lt_trans {T : Type*} [total_order T] {x y z : T} : le x y → lt y z → lt x z :=
assume a1 : le x y,
assume a2 : lt y z,
have s1 : le y z := and.left a2,
have s2 : ¬ y = z := and.right a2,
have s3 : le x z := le_trans a1 s1,
have s4 : ¬ x = z :=
by_contradiction (
  assume a3: ¬ ¬ x = z,
  have s5 : x = z := not_not_1 a3,
  have s6 : le z y := eq.subst s5 a1,
  have s7 : y = z := le_asymm s1 s6,
  show false, from s2 s7
),
and.intro s3 s4

lemma lt_le_trans {T : Type*} [total_order T] {x y z : T} : lt x y → le y z → lt x z :=
assume a1 : lt x y,
assume a2 : le y z,
have s1 : le x y := and.left a1,
have s2 : ¬ x = y := and.right a1,
have s3 : le x z := le_trans s1 a2,
have s4 : ¬ x = z :=
by_contradiction (
  assume a3 : ¬ ¬ x = z,
  have s5 : x = z := not_not_1 a3,
  have s6 : le y x := eq.subst (eq.symm s5) a2,
  have s7 : x = y := le_asymm s1 s6,
  show false, from s2 s7
),
and.intro s3 s4

lemma lt_lt_trans {T : Type*} [total_order T] {x y z : T} : lt x y → lt y z → lt x z :=
assume a1 : lt x y,
assume a2 : lt y z,
have s1 : le x y := and.left a1,
le_lt_trans s1 a2


lemma ge_gt_trans {T : Type*} [total_order T] {x y z : T} : ge x y → gt y z → gt x z :=
assume a1 : ge x y,
assume a2 : gt y z,
have s1 : ge y z := and.left a2,
have s2 : ¬ y = z := and.right a2,
have s3 : ge x z := ge_trans a1 s1,
have s4 : ¬ x = z :=
by_contradiction (
  assume a3: ¬ ¬ x = z,
  have s5 : x = z := not_not_1 a3,
  have s6 : ge z y := eq.subst s5 a1,
  have s7 : y = z := ge_asymm s1 s6,
  show false, from s2 s7
),
and.intro s3 s4

lemma gt_ge_trans {T : Type*} [total_order T] {x y z : T} : gt x y → ge y z → gt x z :=
assume a1 : gt x y,
assume a2 : ge y z,
have s1 : ge x y := and.left a1,
have s2 : ¬ x = y := and.right a1,
have s3 : ge x z := ge_trans s1 a2,
have s4 : ¬ x = z :=
by_contradiction (
  assume a3 : ¬ ¬ x = z,
  have s5 : x = z := not_not_1 a3,
  have s6 : ge y x := eq.subst (eq.symm s5) a2,
  have s7 : x = y := ge_asymm s1 s6,
  show false, from s2 s7
),
and.intro s3 s4

lemma gt_gt_trans {T : Type*} [total_order T] {x y z : T} : gt x y → gt y z → gt x z :=
assume a1 : gt x y,
assume a2 : gt y z,
have s1 : ge x y := and.left a1,
ge_gt_trans s1 a2


lemma le_to_or {T : Type*} [total_order T] {x y : T} : le x y → (lt x y ∨ x = y) :=
assume a1 : le x y,
by_contradiction (
  assume a2 : ¬ (lt x y ∨ x = y),
  have s1 : ¬ lt x y ∧ ¬ x = y := dm_3_a a2,
  have s2 : ¬ (le x y ∧ ¬ x = y) := and.left s1,
  have s3 : ¬ x = y := and.right s1,
  have s4 : ¬ le x y ∨ x = y := dm_1_b s2,
  or.elim s4
  (
    assume a3 : ¬ le x y,
    show false, from a3 a1
  )
  (
    assume a4 : x = y,
    show false, from s3 a4
  )
)


lemma or_to_le {T : Type*} [total_order T] {x y : T} : (lt x y ∨ x = y) → le x y :=
assume a1 : lt x y ∨ x = y,
or.elim a1
(
  assume a2 : lt x y,
  have s1 : le x y ∧ ¬ x = y := a2,
  and.left s1
)
(
  assume a3 : x = y,
  have s2 : le x x := le_refl,
  eq.subst a3 s2
)


lemma ge_to_or {T : Type*} [total_order T] {x y : T} : ge x y → (gt x y ∨ x = y) :=
assume a1 : ge x y,
by_contradiction (
  assume a2 : ¬ (gt x y ∨ x = y),
  have s1 : ¬ gt x y ∧ ¬ x = y := dm_3_a a2,
  have s2 : ¬ (ge x y ∧ ¬ x = y) := and.left s1,
  have s3 : ¬ x = y := and.right s1,
  have s4 : ¬ ge x y ∨ x = y := dm_1_b s2,
  or.elim s4
  (
    assume a3 : ¬ ge x y,
    show false, from a3 a1
  )
  (
    assume a4 : x = y,
    show false, from s3 a4
  )
)

lemma or_to_ge {T : Type*} [total_order T] {x y : T} : (gt x y ∨ x = y) → ge x y :=
assume a1 : gt x y ∨ x = y,
or.elim a1
(
  assume a2 : gt x y,
  have s1 : ge x y ∧ ¬ x = y := a2,
  and.left s1
)
(
  assume a3 : x = y,
  have s2 : ge x x := ge_refl,
  eq.subst a3 s2
)


example {T : Type*} [total_order T] {x y : T} : lt x y → ¬ ge x y :=
assume a1 : lt x y,
assume a2 : ge x y,
have s1 : le x y := and.left a1,
have s2 : ¬ x = y := and.right a1,
have s3 : le y x := a2,
have s4 : x = y := le_asymm s1 s3,
show false, from s2 s4


example {T : Type*} [total_order T] {x y : T} : ¬ ge x y → ¬ x = y :=
assume a1 : ¬ ge x y,
assume a2 : x = y,
have s1 : ge x x := ge_refl,
have s2 : ge x y := eq.subst a2 s1,
show false, from a1 s2


example {T : Type*} [total_order T] {x y : T} : ¬ ge x y → le x y :=
assume a1 : ¬ ge x y,
have s1 : ¬ le y x := a1,
have s2 : le x y ∨ le y x := le_conn,
or.elim s2
(
  assume a2 : le x y,
  a2
)
(
  assume a3 : le y x,
  false.elim (s1 a3)
)


example {T : Type*} [total_order T] {x y : T} : gt x y → ¬ le x y :=
assume a1 : gt x y,
assume a2 : le x y,
have s1 : ge x y := and.left a1,
have s2 : ¬ x = y := and.right a1,
have s3 : ge y x := a2,
have s4 : x = y := ge_asymm s1 s3,
show false, from s2 s4


example {T : Type*} [total_order T] {x y : T} : ¬ le x y → ¬ x = y :=
assume a1 : ¬ le x y,
assume a2 : x = y,
have s1 : le x x := le_refl,
have s2 : le x y := eq.subst a2 s1,
show false, from a1 s2


example {T : Type*} [total_order T] {x y : T} : ¬ le x y → ge x y :=
assume a1 : ¬ le x y,
have s1 : ¬ ge y x := a1,
have s2 : ge x y ∨ ge y x := ge_conn,
or.elim s2
(
  assume a2 : ge x y,
  a2
)
(
  assume a3 : ge y x,
  false.elim (s1 a3)
)

[Patrick Thomas]

Can I petition gt to be redefined in mathlib :)

[Kevin Buzzard]

feel free to make the refactor and pull request.

[Patrick Thomas]

I'm guessing that would be a nightmare?

[Kevin Buzzard]

Actually that's a silly thing to say -- this issue has been thought about seriously and people are very happy with the situation we have now. There is a trade-off between getting something which is acceptable to mathematicians and getting something which is acceptable to computer scientists. Right now everyone is happy with how $>$ is being handled.

[Patrick Thomas]

I see.

[Kevin Buzzard]

Definitely people do come along and say "I think that this should be done differently" and if the idea has enough merit and someone cares enough to implement it, it gets implemented.

[Kevin Buzzard]

What exactly is your proposal for $>$?

[Patrick Thomas]

Something along the lines of def gt {T : Type*} [total_order T] (x y : T) : Prop := x ≥ y ∧ ¬ x = y.

[Kevin Buzzard]

and what is your definition of $\geq$?

[Patrick Thomas]

def ge {T : Type*} [total_order T] (x y : T) : Prop := y ≤ x

[Kevin Buzzard]

So then your definition of $>$ will be equal to Lean's definition, but because of a theorem rather than by definition.

[Kevin Buzzard]

So every time that someone doing analysis in Lean writes $\forall \epsilon>0$ there is a risk that you'll have to now apply a theorem to get mathlib compiling again.

[Kevin Buzzard]

I see no reason at all to do this refactor. What do you gain?

[Kevin Buzzard]

gt is equal to what you say -- just not by definition. (in fact it probably _will_ be equal by definition in many cases, but not for the naturals)

[Patrick Thomas]

How is it equal by definition for some things and not others?

[Kevin Buzzard]

Because x > y is by definition y < x right now, and < is a typeclass, so on a given type it is defined however it was chosen to be defined. For example on the naturals there's some funky inductive definition IIRC which is easier to compute with than your definition.

[Kevin Buzzard]

We have flexibility with the < typeclass to define it how we like; in different situations one might want different definitions which behave better from a computer science viewpoint.

[Kevin Buzzard]

There's simply no point in changing the definition. What you want to be true is true by a theorem. Why do you care whether it's the definition or not? Computer scientists have thought hard about appropriate definitions and they choose ones which are optimal for the given situation, for reasons which I don't even understand. As a mathematician I only care about what is true, not what is defined to be what. Why would you want to change a definition to something equivalent but in some cases less efficient?

[Mario Carneiro]

Note also that your definition of gt is incorrect for preorders

[Mario Carneiro]

and the restriction to total_order T is silly

[Mario Carneiro]

the definition in lean now: def gt {A} [has_lt A] (x y : A) := y < x is extremely general: it says whenever you have a less-than-able type A you can use > just like <. It doesn't care about whether lt has any structure at all. If you add anything like your x >= y /\ x != y you will have to ask for a lot of structure for the predicate to be sensible

[Patrick Thomas]

I think my definition of lt may be wrong for a preorder to?

[Mario Carneiro]

it is

[Patrick Thomas]

Ok.