make an explicit group

Stream: maths

[Kevin Buzzard]

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?

[Reid Barton]

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

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

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]

[Kevin Buzzard]

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

[Kyle Miller]

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

[Reid Barton]

Kevin Buzzard said:

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

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