def nat greater than 0

Stream: new members

[Henrik Böving]

Hey, so I'm currently learning lean and I'm trying to formalize a bit of abstract algebra for self learning purposes so i got this class representing a semigroup:

class semigroup (H: Type) extends has_mul H :=
(mul_assoc: ∀ (a b c: H), (a * b) * c = a * (b * c))

and now I'd basically like to define exponentiation for this class. So I went ahead and wrote

def pow {SG: Type*} [semigroup SG] : SG -> nat -> SG
| a (nat.succ 0)  := a
| a (nat.succ n)  := a * (pow a n)

and rightfully so lean does now complain about the fact that I didnt define my pattern for the natural number 0, however this is only possible inside a monoid as far as I'm concerned since a^0 = 1 which is not something I can express inside a semigroup i believe. So my question would be whether there is some way to still formalize what i want by basically saying that this function only works for "any nat greater than 0"? Or do i have to give up defining this function for a semigroup and instead use a monoid?

[Eric Wieser]

You could use docs#pnat (ℕ+) instead of nat

[Henrik Böving]

Looks just like what I needed, thank you!

[Henrik Böving]

So I now ended up with

def pow {SG: Type*} [half_group SG] : SG -> pnat -> SG
| a one  := a
| a (pnat.succ n)  := a * (pow a n)

but pnat.succ isn't actually defined...and I can't use nat.succ anymore either. Any idea on what the correct notation for this would be?

[Eric Wieser]

This works:

import data.pnat.basic

namespace henrik

class semigroup (H: Type) extends has_mul H :=
(mul_assoc: ∀ (a b c: H), (a * b) * c = a * (b * c))

def pow {SG: Type*} [semigroup SG] : SG -> pnat -> SG
| a ⟨0, h⟩ := false.elim (nat.lt_asymm h h)
| a ⟨1, h⟩ := a
| a ⟨n + 2, h⟩  :=
  have n.succ < n + 2 := nat.succ_le_succ rfl.le,
  a * (pow a ⟨n.succ, n.zero_lt_succ⟩)

end henrik