## Stream: new members

### Topic: algebraic structures

#### Patrick Thomas (Oct 01 2020 at 02:30):

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 (Oct 01 2020 at 02:33):

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 (Oct 01 2020 at 02:34):

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 (Oct 01 2020 at 02:36):

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 (Oct 01 2020 at 02:37):

Inverse is a function?

#### Kyle Miller (Oct 01 2020 at 02:38):

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 (Oct 01 2020 at 02:39):

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 (Oct 01 2020 at 02:40):

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 (Oct 01 2020 at 02:42):

(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 (Oct 01 2020 at 02:45):

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

#### Patrick Thomas (Oct 01 2020 at 02:55):

Actually, that is really cool.

#### Kyle Miller (Oct 01 2020 at 03:00):

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


Thank you!

#### Kyle Miller (Oct 01 2020 at 03:03):

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 (Oct 01 2020 at 03:24):

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 (Oct 01 2020 at 03:25):

actually you can drop the unit too

#### Mario Carneiro (Oct 01 2020 at 03:26):

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

#### Mario Carneiro (Oct 01 2020 at 03:26):

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 (Oct 03 2020 at 16:35):

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 (Oct 03 2020 at 16:37):

They syntax for the is_upper_bound definition that is.

#### Patrick Thomas (Oct 03 2020 at 16:46):

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 (Oct 03 2020 at 16:53):

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

Ok.

#### Patrick Thomas (Oct 07 2020 at 03:54):

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 (Oct 07 2020 at 04:02):

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 (Oct 07 2020 at 04:05):

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

#### Kyle Miller (Oct 07 2020 at 04:05):

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

#### Kyle Miller (Oct 07 2020 at 04:08):

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,


Hmm.

#### Kyle Miller (Oct 07 2020 at 04:13):

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 (Oct 07 2020 at 04:20):

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 (Oct 07 2020 at 04:28):

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 (Oct 07 2020 at 04:31):

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 (Oct 07 2020 at 04:36):

I see. Thank you.

#### Patrick Thomas (Oct 17 2020 at 01:44):

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 (Oct 17 2020 at 01:49):

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

#### Patrick Thomas (Oct 17 2020 at 01:50):

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

#### Adam Topaz (Oct 17 2020 at 01:51):

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

#### Adam Topaz (Oct 17 2020 at 01:52):

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

#### Patrick Thomas (Oct 17 2020 at 01:53):

Oh. I see. Thank you.

#### Kyle Miller (Oct 17 2020 at 02:49):

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 (Oct 17 2020 at 02:53):

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

#### Patrick Thomas (Oct 17 2020 at 17:44):

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

#### Patrick Thomas (Oct 17 2020 at 17:45):

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 (Oct 17 2020 at 17:58):

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 (Oct 17 2020 at 17:58):

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

#### Patrick Thomas (Oct 17 2020 at 17:59):

Because of the way I defined left_group_set with two parameters?

Yeah exactly.

Thank you.

#### Patrick Thomas (Oct 17 2020 at 18:02):

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

#### Adam Topaz (Oct 17 2020 at 18:03):

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

#### Adam Topaz (Oct 17 2020 at 18:04):

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

#### Adam Topaz (Oct 17 2020 at 18:05):

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 (Oct 17 2020 at 18:07):

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

#### Patrick Thomas (Oct 17 2020 at 18:09):

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

#### Adam Topaz (Oct 17 2020 at 18:10):

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

#### Adam Topaz (Oct 17 2020 at 18:10):

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

#### Patrick Thomas (Oct 17 2020 at 18:11):

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 (Oct 17 2020 at 18:12):

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

#### Patrick Thomas (Oct 17 2020 at 18:13):

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

#### Adam Topaz (Oct 17 2020 at 18:15):

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

It's not?

#### Adam Topaz (Oct 17 2020 at 18:15):

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 (Oct 17 2020 at 18:22):

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 (Oct 17 2020 at 18:23):

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 }


That's a sketch.

#### Patrick Thomas (Oct 17 2020 at 18:24):

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

#### Adam Topaz (Oct 17 2020 at 18:25):

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

#### Adam Topaz (Oct 17 2020 at 18:25):

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

#### Patrick Thomas (Oct 17 2020 at 18:26):

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

#### Adam Topaz (Oct 17 2020 at 18:26):

What is a closed function?

#### Patrick Thomas (Oct 17 2020 at 18:28):

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

#### Adam Topaz (Oct 17 2020 at 18:30):

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

#### Adam Topaz (Oct 17 2020 at 18:30):

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

#### Adam Topaz (Oct 17 2020 at 18:34):

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 (Oct 17 2020 at 18:35):

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

#### Adam Topaz (Oct 17 2020 at 18:37):

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 (Oct 17 2020 at 18:46):

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 (Oct 17 2020 at 18:50):

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

Ok. Thank you.

#### Kyle Miller (Oct 17 2020 at 19:33):

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 (Oct 17 2020 at 19:58):

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 (Oct 17 2020 at 20:16):

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

Thank you.

#### Patrick Thomas (Oct 21 2020 at 23:42):

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 (Oct 21 2020 at 23:50):

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

#### Patrick Thomas (Oct 21 2020 at 23:51):

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

#### Patrick Thomas (Oct 24 2020 at 17:56):

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)
(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 (Oct 24 2020 at 18:02):

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
e → 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 :=
group.idempotent

end hidden


#### Kevin Buzzard (Oct 24 2020 at 18:05):

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

#### Reid Barton (Oct 24 2020 at 18:05):

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

#### Patrick Thomas (Oct 24 2020 at 18:05):

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

#### Kevin Buzzard (Oct 24 2020 at 18:06):

But a field isn't a group under multiplication

#### Patrick Thomas (Oct 24 2020 at 18:06):

I know, hence the condition.

#### Kevin Buzzard (Oct 24 2020 at 18:06):

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

Ok.

#### Reid Barton (Oct 24 2020 at 18:07):

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

#### Kevin Buzzard (Oct 24 2020 at 18:08):

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 (Oct 24 2020 at 18:08):

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 (Oct 24 2020 at 18:10):

I'll try the monoid. Thank you!

#### Patrick Thomas (Oct 24 2020 at 18:34):

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

#### Kevin Buzzard (Oct 24 2020 at 18:37):

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 (Oct 25 2020 at 03:58):

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)
(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 (Oct 25 2020 at 04:12):

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

Thank you.

#### Yury G. Kudryashov (Oct 25 2020 at 04:18):

docs#conditionally_complete_linear_order

#### Alex J. Best (Oct 25 2020 at 04:26):

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 (Oct 25 2020 at 06:00):

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 (Oct 25 2020 at 06:03):

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

#### Patrick Thomas (Oct 25 2020 at 06:11):

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

#### Patrick Thomas (Oct 25 2020 at 07:01):

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)
(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 (Oct 25 2020 at 07:04):

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 (Oct 25 2020 at 07:13):

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

#### Mario Carneiro (Oct 25 2020 at 07:17):

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 (Oct 25 2020 at 07:19):

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 (Oct 25 2020 at 07:21):

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 (Oct 25 2020 at 07:21):

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

#### Patrick Thomas (Oct 25 2020 at 17:21):

What does Con(PA) mean?

#### Bryan Gin-ge Chen (Oct 25 2020 at 17:28):

Consistency of PA

#### Patrick Thomas (Oct 25 2020 at 17:31):

Why is that worrying?

#### Reid Barton (Oct 25 2020 at 17:31):

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

#### Reid Barton (Oct 25 2020 at 17:32):

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

#### Reid Barton (Oct 25 2020 at 17:34):

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 (Oct 25 2020 at 17:34):

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

#### Patrick Thomas (Oct 25 2020 at 17:36):

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 (Oct 25 2020 at 17:37):

Maybe that is a bad approach?

#### Reid Barton (Oct 25 2020 at 17:38):

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

Yeah.

#### Reid Barton (Oct 25 2020 at 17:40):

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

Yeah.

#### Patrick Thomas (Oct 25 2020 at 18:36):

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 (Oct 25 2020 at 18:37):

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 (Oct 25 2020 at 18:37):

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 (Oct 25 2020 at 18:38):

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 (Oct 25 2020 at 18:38):

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 (Oct 25 2020 at 18:39):

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

#### Patrick Thomas (Oct 25 2020 at 18:41):

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

#### Kevin Buzzard (Oct 25 2020 at 18:41):

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 (Oct 25 2020 at 18:42):

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

#### Kevin Buzzard (Oct 25 2020 at 18:42):

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

#### Patrick Thomas (Oct 25 2020 at 18:53):

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

MWE?

#### Kevin Buzzard (Oct 25 2020 at 18:54):

oh, you're missing an F

#### Kevin Buzzard (Oct 25 2020 at 18:54):

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

#### Kevin Buzzard (Oct 25 2020 at 18:54):

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

hmm

#### Kevin Buzzard (Oct 25 2020 at 18:55):

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

#### Patrick Thomas (Oct 25 2020 at 18:55):

namespace hidden

class field (F : Type) :=
(add : F → F → F)
(zero : F)
(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))

end hidden


#### Kevin Buzzard (Oct 25 2020 at 18:57):

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

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

#check x + y -- F


Thank you!

#### Mario Carneiro (Oct 25 2020 at 18:59):

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

Ah. Ok.

#### Patrick Thomas (Oct 25 2020 at 19:16):

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 (Oct 25 2020 at 19:18):

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

#### Kevin Buzzard (Oct 25 2020 at 19:19):

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.

Cool.

#### Kevin Buzzard (Oct 25 2020 at 19:23):

(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 (Oct 25 2020 at 19:36):

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

#### Patrick Thomas (Oct 25 2020 at 19:42):

Why? Isn't that undefined?

Define undefined

#### Patrick Thomas (Oct 25 2020 at 19:45):

Contradictory? Or at least unexpected to most mathematicians?

#### Mario Carneiro (Oct 25 2020 at 19:46):

well, the axioms already imply it is a real number

#### Mario Carneiro (Oct 25 2020 at 19:47):

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

#### Bryan Gin-ge Chen (Oct 25 2020 at 19:47):

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 (Oct 25 2020 at 20:06):

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

#### Patrick Thomas (Oct 25 2020 at 20:08):

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 (Oct 25 2020 at 20:09):

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

#### Mario Carneiro (Oct 25 2020 at 20:10):

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

#### Patrick Thomas (Oct 25 2020 at 20:11):

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

#### Mario Carneiro (Oct 25 2020 at 20:12):

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

#### Mario Carneiro (Oct 25 2020 at 20:12):

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 (Oct 25 2020 at 20:15):

I'm not sure what is allowed to vary.

#### Mario Carneiro (Oct 25 2020 at 20:15):

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

#### Mario Carneiro (Oct 25 2020 at 20:17):

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 (Oct 25 2020 at 20:18):

What does it mean to fix G?

#### Kenny Lau (Oct 25 2020 at 20:28):

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 (Oct 25 2020 at 20:38):

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

Indeed.

#### Patrick Thomas (Oct 25 2020 at 20:39):

I'm not sure I see where this leads.

#### Reid Barton (Oct 25 2020 at 20:40):

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 (Oct 25 2020 at 20:44):

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

Depends...

#### Mario Carneiro (Oct 25 2020 at 20:45):

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

do you see why?

#### Patrick Thomas (Oct 25 2020 at 20:49):

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

#### Reid Barton (Oct 25 2020 at 20:50):

This is the meaning of

#### Patrick Thomas (Oct 25 2020 at 20:51):

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

#### Reid Barton (Oct 25 2020 at 20:52):

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 (Oct 25 2020 at 20:53):

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

#### Patrick Thomas (Oct 25 2020 at 20:53):

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

#### Reid Barton (Oct 25 2020 at 20:53):

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 (Oct 25 2020 at 20:55):

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 (Oct 25 2020 at 20:55):

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 (Oct 26 2020 at 00:41):

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 (Oct 26 2020 at 00:44):

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 (Oct 26 2020 at 00:48):

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

#### Yakov Pechersky (Oct 26 2020 at 00:49):

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 (Oct 26 2020 at 00:50):

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

I see.

#### Patrick Thomas (Oct 26 2020 at 19:28):

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 (Oct 26 2020 at 19:29):

Never ever use ge or gt?

#### Kevin Buzzard (Oct 26 2020 at 19:29):

(that's the approach used in mathlib)

#### Kevin Buzzard (Oct 26 2020 at 19:30):

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

Hmm. I suppose.

#### Kevin Buzzard (Oct 26 2020 at 19:33):

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 (Oct 26 2020 at 19:35):

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

#### Patrick Thomas (Oct 26 2020 at 19:38):

Is there any way to disable the existing defined notation?

#### Mario Carneiro (Oct 26 2020 at 19:38):

you can use local notation

#### Mario Carneiro (Oct 26 2020 at 19:39):

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

#### Mario Carneiro (Oct 26 2020 at 19:40):

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

#### Mario Carneiro (Oct 26 2020 at 19:41):

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 (Oct 26 2020 at 19:43):

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 (Oct 26 2020 at 19:44):

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

#### Yury G. Kudryashov (Oct 26 2020 at 19:44):

Not having a > b for preorders looks strange.

#### Yury G. Kudryashov (Oct 26 2020 at 19:45):

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

#### Patrick Thomas (Oct 26 2020 at 19:50):

What does prelude do exactly?

#### Yury G. Kudryashov (Oct 26 2020 at 19:50):

It prevents Lean from importing the default prelude library.

#### Yury G. Kudryashov (Oct 26 2020 at 19:50):

The one that comes with lean.

I see.

#### Yury G. Kudryashov (Oct 26 2020 at 19:51):

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

Hmm. Ok.

#### Yury G. Kudryashov (Oct 26 2020 at 19:56):

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

#### Yury G. Kudryashov (Oct 26 2020 at 19:57):

Unless you have some very special needs.

#### Patrick Thomas (Oct 26 2020 at 20:24):

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 :=
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 :=
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 :=
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 :=
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,
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,
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 (Oct 26 2020 at 20:44):

Can I petition gt to be redefined in mathlib :)

#### Kevin Buzzard (Oct 26 2020 at 20:45):

feel free to make the refactor and pull request.

#### Patrick Thomas (Oct 26 2020 at 20:46):

I'm guessing that would be a nightmare?

#### Kevin Buzzard (Oct 26 2020 at 20:46):

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.

I see.

#### Kevin Buzzard (Oct 26 2020 at 20:48):

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 (Oct 26 2020 at 20:48):

What exactly is your proposal for $>$?

#### Patrick Thomas (Oct 26 2020 at 20:49):

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

#### Kevin Buzzard (Oct 26 2020 at 20:50):

and what is your definition of $\geq$?

#### Patrick Thomas (Oct 26 2020 at 20:51):

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

#### Kevin Buzzard (Oct 26 2020 at 20:52):

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

#### Kevin Buzzard (Oct 26 2020 at 20:52):

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 (Oct 26 2020 at 20:53):

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

#### Kevin Buzzard (Oct 26 2020 at 20:53):

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 (Oct 26 2020 at 20:54):

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

#### Kevin Buzzard (Oct 26 2020 at 20:56):

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 (Oct 26 2020 at 20:57):

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 (Oct 26 2020 at 20:59):

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 (Oct 26 2020 at 21:00):

Note also that your definition of gt is incorrect for preorders

#### Mario Carneiro (Oct 26 2020 at 21:00):

and the restriction to total_order T is silly

#### Mario Carneiro (Oct 26 2020 at 21:03):

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 (Oct 26 2020 at 21:04):

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

it is

#### Patrick Thomas (Oct 26 2020 at 21:08):

Ok.

Last updated: May 14 2021 at 06:16 UTC