Group Hierarchy and Type Classes

Stream: new members

[Luna]

I've been going through section 7 of MIL and experimenting with type classes and algebraic hierarchies. I wanted to create a hierarchy with the following goals

1. keep data out of type classes (to avoid unnecessary duplication such as Group and AddGroup)
2. implicitly handle non-definitional equality

I've made some interesting progress and would like feedback on possible pain points or improvements to this type of hierarchy. For example, I've noticed that it doesn't play well with the rw tactic, as the tactic doesn't try to synthesize type instances. But apply, simp, and exact seem to work as expected.

The full code is below (with proofs sorry'd out for brevity):

-- Equal is used to implicitly handle non-definition equality
class Equal {α : Type _} (a b : α) where
    equal : a = b

instance Equal.symm_inst {α : Type _} {a b : α} [b_eq_a : Equal b a] : Equal a b where
    equal := Eq.symm b_eq_a.equal

instance Equal.rfl_inst {α : Type _} {a : α} : Equal a a where
    equal := Eq.refl a


section
    variable {α : Type _} (op : α → α → α)
    local infix:70 (priority := high) " * " => op

    class Semigroup where
        op_assoc : ∀ (a b c : α), a * (b * c) = (a * b) * c

    @[simp]
    theorem op_assoc [S : Semigroup op] : ∀ (a b c : α), a * (b * c) = (a * b) * c := S.op_assoc

    -- doesn't contain data and instead the data is derived from the properties placed on the binary operator
    class Group extends (Semigroup op) where
        has_ident_and_inv : ∃ (ident : α), ∃ (inv : α → α), ∀ (a : α), (a * ident = a) ∧ (a * (inv a) = ident)

    instance {α : Type _} {op : α → α → α} : CoeSort (Group op) (Type _) where
        coe _ := α
end


section
    variable {α : Type _} {op : α → α → α} (G : Group op)

    noncomputable def Group.Ident := (Classical.choose G.has_ident_and_inv)
    noncomputable def Group.Inv : α → α := Classical.choose (Classical.choose_spec G.has_ident_and_inv)
end


section
    variable {α : Type _} {op : α → α → α} [G : Group op]
    variable {ident : α} [ident_equal : Equal ident G.Ident]
    variable {inv : α → α} [inv_equal : Equal inv G.Inv]
    local infix:70 (priority := high) " * " => op

    @[simp]
    theorem op_inv : ∀ (a : G), a * (inv a) = ident := by sorry

    @[simp]
    theorem op_ident : ∀ (a : G), a * ident = a := by sorry

    @[simp]
    theorem ident_comm : ∀ (a : G), a * ident = ident * a := by sorry

    @[simp]
    theorem inv_comm : ∀ (a : G), a * (inv a) = (inv a) * a := by sorry

    @[simp]
    theorem inv_op : ∀ (a : G), (inv a) * a = ident := by sorry

    @[simp]
    theorem ident_op : ∀ (a : G), ident * a = a := by sorry

    theorem ident_inv_unique {ident : G} {inv : α → α} (is_ident : ∀ (a : α), a * ident = a) (is_inv : ∀ (a : α), a * (inv a) = ident) : (ident = G.Ident) ∧ (inv = G.Inv) := by sorry
end
-- example instance
instance Int.AddGroup : Group (· + · : Int → Int → Int) where
    op_assoc := sorry
    has_ident_and_inv := sorry
-- register -a as equal to the additive inverse
noncomputable instance : Equal Int.AddGroup.Inv (-· : Int → Int) where
    equal := sorry
-- register 0 equal to the additive identity
noncomputable instance : Equal Int.AddGroup.Ident 0 where
    equal := sorry


example : ∀ (a : Int), a + 0 = a := by
    exact op_ident

example : ∀ (a : Int), a + 0 = 0 + a := by
    exact ident_comm

example : ∀ (a : Int), a + -a = 0 := by
    exact op_inv

[Alex Mobius]

You implemented close to version 3 in my reply, it seems! Your formulas say that for a single identity, there are inverses for all elements. Cool that that's also enough! Although you'd benefit from ExistsUnique for brevity in statement of your proof :)