Zulip Chat Archive

Stream: new members

Topic: Natural Number addition definition


Mukesh Tiwari (Mar 21 2020 at 10:50):

Hi everyone,

I have defined a algebraic structure (monoid), and I want make my custom natural number and addition as a instance of monoid. However, my addition function definition is giving this error : equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details). algebraic.lean

Mukesh Tiwari (Mar 21 2020 at 10:52):

namespace Structures

structure monoid {A : Type} (f : A → A → A) (e : A) :=
(Hassoc : ∀ a b c : A, f (f a b) c = f a (f b c))
(Hidl : ∀ a : A, f e a = a)
(Hidr : ∀ a : A, f a e = a)


/- Proofs about monoid -/


/- end proof of monoid -/
end Structures

namespace mynat

inductive nat : Type
| Z : nat
| S : nat → nat

open nat
def add : nat -> nat -> nat
| Z n := n
| (S m) n := S (add m n)

end mynat

namespace mylist

inductive list (A : Type) :  Type
| Nil {} : list
| Cons : A -> list -> list

def append {A : Type} : list A → list A → list A
| Nil l := l
| (Cons x xs) l := Cons x (append xs l)


end mylist
#check mylist.list.Nil
#check (mylist.list.Cons mynat.nat.Z mylist.list.Nil)

Johan Commelin (Mar 21 2020 at 10:57):

namespace custom

structure monoid {A : Type} (f : A  A  A) (e : A) :=
(Hassoc :  a b c : A, f (f a b) c = f a (f b c))
(Hidl :  a : A, f e a = a)
(Hidr :  a : A, f a e = a)

inductive mynat : Type
| Z : mynat
| S : mynat  mynat

namespace mynat

def add : mynat -> mynat -> mynat
| Z n := n
| (S m) n := S (add m n)

def monoid : monoid add Z :=
{ Hassoc := _,
  Hidl := _,
  Hidr := _ }

end mynat

end custom

Johan Commelin (Mar 21 2020 at 10:57):

I didn't test the code, but I think you want something like that :up:

Johan Commelin (Mar 21 2020 at 10:57):

Pro-tip: with

```lean
code goes here
```

you get pretty syntax highlighting

Mukesh Tiwari (Mar 21 2020 at 11:06):

@Johan Commelin Thanks for the answer, but I still did not understand the problem in my code. I see that you created a top level namespace custom, then defined monoid and mynat (while I closed the namespace after monoid definition and created a new namespace). Anyway, I would like to know what is wrong with my structuring?

Johan Commelin (Mar 21 2020 at 11:07):

Sorry, need to run to prepare some lunch for my kids.

Mukesh Tiwari (Mar 21 2020 at 11:09):

No worries.

Johan Commelin (Mar 21 2020 at 11:28):

Quick answer: my guess is that maybe your code got confused with the nat that already exists. That's why I renamed everything to mynat in your code.

Johan Commelin (Mar 21 2020 at 11:29):

But I don't know of that is actually what went wrong.

Mukesh Tiwari (Mar 21 2020 at 11:33):

I figured it out. I don't know why 'open nat' is not working, so I replace every Z with nat.Z and S with nat.S in add, and type checker is happy.

Mukesh Tiwari (Mar 21 2020 at 11:34):

Also, when I need to change structure to class (I don't know why) to make type checker happy because it was complaining that 'Structures.monoid' is not a class

Patrick Massot (Mar 21 2020 at 11:45):

open nat only gives access to stuff defined before that command.

Patrick Massot (Mar 21 2020 at 11:47):

Mukesh Tiwari said:

Also, when I need to change structure to class (I don't know why) to make type checker happy because it was complaining that 'Structures.monoid' is not a class

We need more code to help you here, although we can guess you tried to use square brackets around a structure argument (which is absurd).

Mukesh Tiwari (Mar 21 2020 at 11:53):

namespace AlgebraicStructures


class monoid {A : Type} (e : A) (f : A → A → A)  :=
(Hassoc : ∀ a b c : A, f a (f b c) = f (f a b) c)
(Hidl : ∀ a : A, f e a = a)
(Hidr : ∀ a : A, f a e = a)


class group {A : Type} (e : A) (f : A → A → A) (inv : A → A) :=
 (Hmon : @monoid A e f)
 (Hinvl : ∀ x, f (inv x) x = e)
 (Hinvr : ∀ x, f x (inv x) = e)


end AlgebraicStructures

namespace mynat

inductive nat : Type
| Z : nat
| S : nat → nat


def add : nat -> nat -> nat
| nat.Z n := n
| (nat.S m) n := nat.S (add m n)

theorem add_zerol : ∀ (n : nat), add nat.Z n = n :=
begin
  intro n, trivial
end

theorem add_zeror : ∀ (n : nat), add n nat.Z = n :=
begin
 intro n, induction n,
 trivial,
 sorry
end

theorem add_assoc : ∀ n m r : nat, add n (add m r) = add (add n m) r :=
sorry


instance monoid : AlgebraicStructures.monoid nat.Z add :=
{
  Hassoc := add_assoc,
  Hidl := add_zerol,
  Hidr := add_zeror
}



end mynat

Changing class monoid to structure monoid makes typechecker unhappy about the 'instance monoid : : AlgebraicStructures.monoid nat.Z add'.

Patrick Massot (Mar 21 2020 at 11:54):

Ok, this is even worse than what I expected.

Patrick Massot (Mar 21 2020 at 11:55):

But don't worry, you'll be fine. What do you think instance means?

Mukesh Tiwari (Mar 21 2020 at 12:03):

I understand that it is a way to generate a concrete instance of some abstract structure (but my understanding is very much influenced by Haskell, so pardon me for my stupidity)

Patrick Massot (Mar 21 2020 at 12:15):

No, they declare instances (concrete or not) of classes. There is no stupidity issue here. Everybody is welcome to learn. The standard reference here is https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

Mukesh Tiwari (Mar 21 2020 at 12:17):

Thanks @Patrick Massot . I will have a more careful look at the tutorial.

Mukesh Tiwari (Mar 21 2020 at 12:19):

Also if you don't mind, then can you post your version of my code?

Patrick Massot (Mar 21 2020 at 12:42):

I don't know what you expect from "my version". Did you look at how it's done in the standard library? The differences are pretty visible.

Patrick Massot (Mar 21 2020 at 12:44):

About building algebraic hierarchy, the mathlib paper has explanation, and even the more recent maintenance paper has relevant bits.

Kevin Buzzard (Mar 21 2020 at 12:49):

What's the question here? instance makes terms of classes, and if you change the class to a structure you get an error saying it's not a class, so as far as I can see everything is consistent.

Mukesh Tiwari (Mar 21 2020 at 12:56):

Patrick Massot said:

Ok, this is even worse than what I expected.

Based on your response, I thought I have deviated horribly from idiomatic Lean way; hence the reason for asking about your version.

Kevin Buzzard (Mar 21 2020 at 12:57):

Oh yes you did that too :-)

Mukesh Tiwari (Mar 21 2020 at 12:58):

@Kevin Buzzard and now I am curious :) (care to rewrite it if you have time).

Kevin Buzzard (Mar 21 2020 at 12:58):

In idiomatic Lean we use notation for the identity and multiplication, rather than letting monoid take these functions as input.

Kevin Buzzard (Mar 21 2020 at 12:59):

The way it's set up in Lean's maths library is something like this:

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

-- definition of the group structure
class group (G : Type) extends has_group_notation G :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

Kevin Buzzard (Mar 21 2020 at 12:59):

but without the inverses

Kevin Buzzard (Mar 21 2020 at 13:00):

This has the downside that we need a second class add_monoid extending has_add and has_zero.

Kevin Buzzard (Mar 21 2020 at 13:00):

but we have machinery which transfers lemmas about one structure to lemmas about the other.

Mukesh Tiwari (Mar 21 2020 at 13:03):

What is the advantage of bundling the three (e : A) (f : A → A → A) (inv : A → A) in a separate type class (has_group_notation) ?

Kevin Buzzard (Mar 21 2020 at 13:04):

I am not a type theory person so I can't talk about the relative advantages and disadvantages, but I can tell you that we have managed to make a whole ton of algebra doing it like this and it works fine.

Kevin Buzzard (Mar 21 2020 at 13:04):

oh -- sorry, that's not the question you asked.

Kevin Buzzard (Mar 21 2020 at 13:05):

That was just me trying to be clever.They don't do that in the maths library

Kevin Buzzard (Mar 21 2020 at 13:05):

In the maths library they just extend has_one, has_mul

Kevin Buzzard (Mar 21 2020 at 13:07):

class monoid' (M : Type*) extends has_mul M, has_one M :=
(mul_assoc :  (a b c : M), a * b * c = a * (b * c))
(one_mul :  (a : M), 1 * a = a)
(mul_one :  (a : M), a * 1 = a)

That is a pretty faithful representation of what is actually in the library

Kevin Buzzard (Mar 21 2020 at 13:08):

Just write #check monoid in VS Code and right click on monoid and go to the definition

Mukesh Tiwari (Mar 21 2020 at 13:08):

Thank Kevin for all the explanation. Maybe I need to write more Lean code to understand it better (the problem is my fallback to Coq, but this time, I am fairly determined.)

Kevin Buzzard (Mar 21 2020 at 13:09):

The difference between your definition and the one in Lean is that in Lean you have to use * for the group law. But because you can define the multiplication on M to be whatever you like, it works out fine.

Mukesh Tiwari (Mar 21 2020 at 13:21):

What do you think about this one ?

class monoid {A : Type*} (e : A) (f : A → A → A)  :=
 (Hassoc : ∀ a b c : A, f a (f b c) = f (f a b) c)
 (Hidl : ∀ a : A, f e a = a)
 (Hidr : ∀ a : A, f a e = a)


class group {A : Type*} (e : A) (f : A → A → A)
 (inv : A → A) [@monoid A e f] :=
 (Hinvl : ∀ x, f (inv x) x = e)
 (Hinvr : ∀ x, f x (inv x) = e)

class abelian_group {A : Type*} (e : A) (f : A → A → A)
 (inv : A → A) [Hm : @monoid A e f] [@group A e f inv Hm]:=
 (Hcomm : ∀ x y : A, f x y = f y x)

Kevin Buzzard (Mar 21 2020 at 13:21):

They're not how it's done in mathlib but I can understand that it is possible to do it like this.

Kevin Buzzard (Mar 21 2020 at 13:22):

the mathlibcore Lean way looks less clunky to me

Kevin Buzzard (Mar 21 2020 at 13:23):

class semigroup (α : Type u) extends has_mul α :=
(mul_assoc :  a b c : α, a * b * c = a * (b * c))

class comm_semigroup (α : Type u) extends semigroup α :=
(mul_comm :  a b : α, a * b = b * a)

class left_cancel_semigroup (α : Type u) extends semigroup α :=
(mul_left_cancel :  a b c : α, a * b = a * c  b = c)

class right_cancel_semigroup (α : Type u) extends semigroup α :=
(mul_right_cancel :  a b c : α, a * b = c * b  a = c)

class monoid (α : Type u) extends semigroup α, has_one α :=
(one_mul :  a : α, 1 * a = a) (mul_one :  a : α, a * 1 = a)

class comm_monoid (α : Type u) extends monoid α, comm_semigroup α

class group (α : Type u) extends monoid α, has_inv α :=
(mul_left_inv :  a : α, a⁻¹ * a = 1)

class comm_group (α : Type u) extends group α, comm_monoid α

Kevin Buzzard (Mar 21 2020 at 13:25):

You have f (inv x) x = e, Lean has a⁻¹ * a = 1, so the Lean way kind of looks nicer

Mukesh Tiwari (Mar 21 2020 at 13:28):

Now, I see your point. I agree that it is much cleaner.


Last updated: Dec 20 2023 at 11:08 UTC