Zulip Chat Archive

Stream: Is there code for X?

Topic: Guessing the structure from the axioms


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Nov 27 2020 at 19:18):

I suppose this is a workaround


Last updated: May 16 2021 at 05:21 UTC