Zulip Chat Archive

Stream: maths

Topic: make an explicit group


view this post on Zulip Kevin Buzzard (Jul 14 2020 at 21:28):

import tactic

inductive mu2
| p1 : mu2
| m1 : mu2

namespace mu2

def mul : mu2  mu2  mu2
| p1 p1 := p1
| p1 m1 := m1
| m1 p1 := m1
| m1 m1 := p1

def one : mu2 := p1

def inv : mu2  mu2 := id

instance : group mu2 := dec_trivial -- doesn't work yet

end mu2

Is it easy to get this working automatically somehow?

view this post on Zulip Reid Barton (Jul 14 2020 at 21:48):

import tactic

@[derive decidable_eq] inductive mu2
| p1 : mu2
| m1 : mu2

instance : fintype mu2 := ⟨⟨[mu2.p1, mu2.m1], by simp, λ x, by cases x; simp

namespace mu2

def mul : mu2  mu2  mu2
| p1 p1 := p1
| p1 m1 := m1
| m1 p1 := m1
| m1 m1 := p1

def one : mu2 := p1

def inv : mu2  mu2 := id

instance : group mu2 :=
by refine_struct { one := one, mul := mul, inv := inv }; exact dec_trivial

end mu2

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 22:06):

Thanks!

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 22:07):

I did all of that myself apart from the fintype, which I also tried to derive. I don't understand why we have to derive decidable equality, whereas if we want an extensionality lemma we just [ext]

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 22:08):

Isn't there a way to derive the fintype instance?

view this post on Zulip Kyle Miller (Jul 14 2020 at 22:11):

Adding to that question, is there a list of all the derivable instances somewhere?

view this post on Zulip Reid Barton (Jul 14 2020 at 22:15):

Kevin Buzzard said:

Isn't there a way to derive the fintype instance?

You'd think so but afaik it isn't implemented.


Last updated: May 11 2021 at 15:12 UTC