Zulip Chat Archive

Stream: new members

Topic: algebraic structures


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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,
 ...
}

view this post on Zulip Patrick Thomas (Oct 01 2020 at 02:37):

Inverse is a function?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Patrick Thomas (Oct 01 2020 at 02:45):

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

view this post on Zulip Patrick Thomas (Oct 01 2020 at 02:55):

Actually, that is really cool.

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 01 2020 at 03:02):

Thank you!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 01 2020 at 03:25):

actually you can drop the unit too

view this post on Zulip Mario Carneiro (Oct 01 2020 at 03:26):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 03 2020 at 16:37):

They syntax for the is_upper_bound definition that is.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 03 2020 at 16:56):

Ok.

view this post on Zulip 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
  )
)

view this post on Zulip 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)),

view this post on Zulip Patrick Thomas (Oct 07 2020 at 04:05):

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

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip Patrick Thomas (Oct 07 2020 at 04:11):

Hmm.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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,

view this post on Zulip Patrick Thomas (Oct 07 2020 at 04:36):

I see. Thank you.

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Oct 17 2020 at 01:49):

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

view this post on Zulip Patrick Thomas (Oct 17 2020 at 01:50):

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

view this post on Zulip Adam Topaz (Oct 17 2020 at 01:51):

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

view this post on Zulip Adam Topaz (Oct 17 2020 at 01:52):

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

view this post on Zulip Patrick Thomas (Oct 17 2020 at 01:53):

Oh. I see. Thank you.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Patrick Thomas (Oct 17 2020 at 17:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 17 2020 at 17:58):

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

view this post on Zulip Patrick Thomas (Oct 17 2020 at 17:59):

Because of the way I defined left_group_set with two parameters?

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:00):

Yeah exactly.

view this post on Zulip Patrick Thomas (Oct 17 2020 at 18:00):

Thank you.

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:03):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Thomas (Oct 17 2020 at 18:06):

I think Kyle already did.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:10):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:12):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:15):

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

view this post on Zulip Patrick Thomas (Oct 17 2020 at 18:15):

It's not?

view this post on Zulip 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 SS of α\alpha such that α\alpha has a operation op:αααop : \alpha \to \alpha \to \alpha and an element e:αe : \alpha such that eSe \in S and such that the operation and ee induce a group structure on SS.

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:24):

That's a sketch.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 17 2020 at 18:26):

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

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:26):

What is a closed function?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:30):

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

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:30):

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

view this post on Zulip 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 GG as a function μ:G×GU\mu : G \times G \to \mathbb{U} into some universe U\mathbb{U} where GG is a subset of U\mathbb{U} and it just so happens that μ(g,h)G\mu(g,h) \in G for all g,hGg,h \in G.

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:35):

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

view this post on Zulip Adam Topaz (Oct 17 2020 at 18:37):

But in any case, if you do go this route with U\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.

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 17 2020 at 19:07):

Ok. Thank you.

view this post on Zulip 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 GG, 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}

view this post on Zulip 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?

view this post on Zulip 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×GGG\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.)

view this post on Zulip Patrick Thomas (Oct 17 2020 at 20:22):

Thank you.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 21 2020 at 23:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:05):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:06):

But a field isn't a group under multiplication

view this post on Zulip Patrick Thomas (Oct 24 2020 at 18:06):

I know, hence the condition.

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:06):

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

view this post on Zulip Patrick Thomas (Oct 24 2020 at 18:07):

Ok.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Patrick Thomas (Oct 24 2020 at 18:10):

I'll try the monoid. Thank you!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 04:16):

Thank you.

view this post on Zulip Yury G. Kudryashov (Oct 25 2020 at 04:18):

docs#conditionally_complete_linear_order

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Oct 25 2020 at 06:03):

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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 06:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 07:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Oct 25 2020 at 07:21):

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

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 25 2020 at 17:21):

What does Con(PA) mean?

view this post on Zulip Bryan Gin-ge Chen (Oct 25 2020 at 17:28):

Consistency of PA

view this post on Zulip Patrick Thomas (Oct 25 2020 at 17:31):

Why is that worrying?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 25 2020 at 17:34):

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

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 25 2020 at 17:37):

Maybe that is a bad approach?

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 17:40):

Yeah.

view this post on Zulip Reid Barton (Oct 25 2020 at 17:40):

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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 17:40):

Yeah.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:39):

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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 18:41):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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⟩.

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:53):

MWE?

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:54):

oh, you're missing an F

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:54):

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

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:55):

hmm

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 18:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 18:58):

Thank you!

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 19:00):

Ah. Ok.

view this post on Zulip 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))

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 19:18):

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

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 25 2020 at 19:22):

Cool.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 25 2020 at 19:42):

Why? Isn't that undefined?

view this post on Zulip Reid Barton (Oct 25 2020 at 19:43):

Define undefined

view this post on Zulip Patrick Thomas (Oct 25 2020 at 19:45):

Contradictory? Or at least unexpected to most mathematicians?

view this post on Zulip Mario Carneiro (Oct 25 2020 at 19:46):

well, the axioms already imply it is a real number

view this post on Zulip Mario Carneiro (Oct 25 2020 at 19:47):

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

view this post on Zulip 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/

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:09):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:10):

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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:11):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:12):

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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:15):

I'm not sure what is allowed to vary.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:18):

What does it mean to fix G?

view this post on Zulip 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?

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:38):

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

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 20:38):

Indeed.

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:39):

I'm not sure I see where this leads.

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:44):

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

view this post on Zulip Johan Commelin (Oct 25 2020 at 20:45):

Depends...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:45):

do you see why?

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:49):

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

view this post on Zulip Reid Barton (Oct 25 2020 at 20:50):

This is the meaning of :37:

view this post on Zulip Patrick Thomas (Oct 25 2020 at 20:51):

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

view this post on Zulip Reid Barton (Oct 25 2020 at 20:52):

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

view this post on Zulip Patrick Massot (Oct 25 2020 at 20:53):

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

view this post on Zulip 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.

view this post on Zulip 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 x1x^{-1}.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 26 2020 at 00:48):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 00:50):

I see.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 19:29):

Never ever use ge or gt?

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 19:29):

(that's the approach used in mathlib)

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 26 2020 at 19:31):

Hmm. I suppose.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 19:33):

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

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 19:38):

Is there any way to disable the existing defined notation?

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:38):

you can use local notation

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:39):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:40):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:44):

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

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:44):

Not having a > b for preorders looks strange.

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:45):

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

view this post on Zulip Patrick Thomas (Oct 26 2020 at 19:50):

What does prelude do exactly?

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:50):

It prevents Lean from importing the default prelude library.

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:50):

The one that comes with lean.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 19:50):

I see.

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 19:52):

Hmm. Ok.

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:56):

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

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:57):

Unless you have some very special needs.

view this post on Zulip 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)
)

view this post on Zulip Patrick Thomas (Oct 26 2020 at 20:44):

Can I petition gt to be redefined in mathlib :)

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 20:45):

feel free to make the refactor and pull request.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 20:46):

I'm guessing that would be a nightmare?

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Oct 26 2020 at 20:47):

I see.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 20:48):

What exactly is your proposal for >>?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 20:50):

and what is your definition of \geq?

view this post on Zulip Patrick Thomas (Oct 26 2020 at 20:51):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 20:52):

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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 20:53):

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

view this post on Zulip 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)

view this post on Zulip Patrick Thomas (Oct 26 2020 at 20:54):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 26 2020 at 21:00):

Note also that your definition of gt is incorrect for preorders

view this post on Zulip Mario Carneiro (Oct 26 2020 at 21:00):

and the restriction to total_order T is silly

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 26 2020 at 21:04):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 21:04):

it is

view this post on Zulip Patrick Thomas (Oct 26 2020 at 21:08):

Ok.


Last updated: May 14 2021 at 06:16 UTC