0
\$\begingroup\$

I'm making a nice little implementation of groups from first principles in lean.

To do this I am making 3 basic structures, semigroups, quasigroups and unital magmata. Groups are then defined to be structures that are all 3.

A lot of things fit really nice here. I can have multiple groups, semigroups etc, for one type and my axioms can be written pretty cleanly.

However, my proof is a mess. There's one non-trivial proof here, It's still a very simple proof, it's just really ugly when written in lean.

The proof is that 1 / a is the inverse of a. It's lemma left_right_cancellation in the code below. But it can be written for humans as:

1 = 1
  = a ⬝ (a \ 1)
  = (a ⬝ 1) ⬝ (a \ 1)
  = (a ⬝ ((1 / a) ⬝ a)) ⬝ (a \ 1)
  = a ⬝ (((1 / a) ⬝ a) ⬝ (a \ 1))
  = a ⬝ ((1 / a) ⬝ (a ⬝ (a \ 1)))
  = a ⬝ ((1 / a) ⬝ 1)
  = a ⬝ (1 / a)

The associativity gets a little hairy, but otherwise this is decently easy to follow. The lean version of this is not easy to follow.

There's a lot of mess generated because I have to use conv to get to the terms I want to manipulate, and I the lack of infix symbols mean that everything is in this bizarre prefix notation, which makes the interactive readout on this proof inscrutable.

I'd like to make this more straightforwardly easy to read, but I feel like I'm lacking the tools to make clean readable lean proofs.

universe u

class unital {α : Type u} (bin : α → α → α) :=
  ( unit : α )
  ( left_id : ∀ a : α, bin unit a = a )
  ( right_id : ∀ a : α, bin a unit = a )

open unital

class semigroup {α : Type u} (bin : α → α → α) :=
  ( assoc : ∀ a b c : α, bin a (bin b c) = bin (bin a b) c )

open semigroup

class quasigroup {α : Type u} (bin : α → α → α) :=
  ( left_div : α → α → α )
  ( right_div : α → α → α )
  ( left_cancel : ∀ a b : α, bin a (left_div a b) = b )
  ( right_cancel : ∀ a b : α, bin (right_div b a) a = b )

open quasigroup

class group {α : Type u} (bin : α → α → α) extends quasigroup bin, semigroup bin, unital bin :=
  ( neg : α → α )
  ( left_inv : ∀ a : α, bin (neg a) a = unit )
  ( right_inv : ∀ a : α, bin a (neg a) = unit )

lemma left_right_cancellation {α : Type u} {bin : α → α → α} [q : quasigroup bin] [s : semigroup bin] [u : unital bin] : ∀ a : α, bin a (right_div bin (unital.unit bin) a) = unital.unit bin := λ a, by
  { rw <- (@right_id α bin u) (bin a (right_div bin (unit bin) a))
  , conv
    { to_lhs
    , congr
    , skip
    , rw <- (@left_cancel α bin q a (unit bin))
    }
  , rw <- (@assoc α bin s)
  , conv
    { to_lhs
    , congr
    , skip
    , rw (@assoc α bin s)
    , rw (@right_cancel α bin q)
    , rw (@left_id α bin u)
    }
  , rw (@left_cancel α bin q)
  }

instance group_def {α : Type u} {bin : α → α → α} [q : quasigroup bin] [s : semigroup bin] [u : unital bin] : group bin :=
  ⟨ @right_div α bin q (@unital.unit α bin u)
  , λ a, right_cancel a (unital.unit bin)
  , left_right_cancellation
  ⟩
\$\endgroup\$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.