# Zulip Chat Archive

## 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
```

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

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.

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

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,
```

#### Patrick Thomas (Oct 07 2020 at 04:11):

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?

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

Yeah exactly.

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

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

I think Kyle already did.

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

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

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 }
```

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

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.

#### Patrick Thomas (Oct 17 2020 at 19:07):

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

#### Patrick Thomas (Oct 17 2020 at 20:22):

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

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

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

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

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)
(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 (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 07:33):

I have to go to sleep. I'll try to think about this more tomorrow. Thank 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`

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

Yeah.

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

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

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

Yeah.

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

If I add this notation and use `0`

then 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⟩`

.

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

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.

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

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)
(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 (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
```

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

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

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

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.

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

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?

#### Reid Barton (Oct 25 2020 at 19:43):

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?

#### Kevin Buzzard (Oct 25 2020 at 20:38):

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?

#### Johan Commelin (Oct 25 2020 at 20:45):

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

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

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.

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

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

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

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.

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

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.

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

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 :=
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 (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.

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

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?

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

it is

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

Ok.

Last updated: May 14 2021 at 06:16 UTC