Guessing the structure from the axioms

Stream: Is there code for X?

[Bassem Safieldeen]

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]

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]

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

[Kenny Lau]

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]

I suppose this is a workaround