Natural Number addition definition

Stream: new members

[Mukesh Tiwari]

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]

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]

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]

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

[Johan Commelin]

Pro-tip: with

```lean
code goes here
```

you get pretty syntax highlighting

[Mukesh Tiwari]

@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]

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

[Mukesh Tiwari]

No worries.

[Johan Commelin]

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]

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

[Mukesh Tiwari]

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]

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]

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

[Patrick Massot]

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]

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]

Ok, this is even worse than what I expected.

[Patrick Massot]

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

[Mukesh Tiwari]

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]

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]

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

[Mukesh Tiwari]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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]

Oh yes you did that too :-)

[Mukesh Tiwari]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

but without the inverses

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mukesh Tiwari]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

In the maths library they just extend has_one, has_mul

[Kevin Buzzard]

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]

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

[Mukesh Tiwari]

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]

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]

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]

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

[Kevin Buzzard]

the mathlibcore Lean way looks less clunky to me

[Kevin Buzzard]

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]

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

[Mukesh Tiwari]

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