## Stream: Is there code for X?

### Topic: Guessing the structure from the axioms

#### Bassem Safieldeen (Nov 27 2020 at 17:58):

Is there a way to show Lean this

class test_class (α : Type) extends has_mul α :=
(test_axiom : ∀ a b c : α, a * b * c = a * (b * c))


and have it tell me that this is a semigroup?

#### Kevin Buzzard (Nov 27 2020 at 18:20):

import tactic

set_option old_structure_cmd true

@[ext] class test_class (G : Type) extends has_mul G :=
(test_axiom : ∀ a b c : G, a * b * c = a * (b * c))

def test_class_equiv_semigroup (G : Type) : test_class G ≃ semigroup G :=
{ to_fun := λ tc, by exactI
{ mul := (*),
mul_assoc := test_class.test_axiom },
inv_fun := λ sg, by exactI
{ mul := (*),
test_axiom := semigroup.mul_assoc },
left_inv := λ tc, by {cases tc, ext, refl},
right_inv := λ sg, by {cases sg, simp, refl} }


is one way of interpreting what you're asking for. If this isn't what you meant, then why not post some code with a sorry in?

#### Johan Commelin (Nov 27 2020 at 18:23):

I think @Bassem Safieldeen means a sort of "library_search" for structures... I don't think we really have anything like that.

#### Kenny Lau (Nov 27 2020 at 19:18):

import tactic

#check (by library_search : ∀ a b c : ℕ, (a * b) * c = a * (b * c)) -- Try this: exact mul_assoc
#check @mul_assoc -- ∀ {G : Type u_1} [_inst_1 : semigroup G] (a b c : G), a * b * c = a * (b * c)


#### Kenny Lau (Nov 27 2020 at 19:18):

I suppose this is a workaround

Last updated: May 16 2021 at 05:21 UTC