How to write a Group instance for xor?

Stream: new members

[Timothy Mou]

I want to make a group instance for Nat, with Nat.xor as the group operation. What's the correct way to do this? Do I have to make a newtype wrapper, like this:

structure XorNat where
  n : Nat

instance : Group XorNat where
  ...

If I do this, it seems that in order to define the instance, I have to constantly wrap/unwrap to use the properties of xor. Is there a way around this to reduce the amount of boilerplate?

[Eric Wieser]

That's usually the recommended approach, though if you're feeling brave you can use def XorNat := Nat

[Eric Wieser]

(your approach is the one I described at LFTCM 2023)

[Timothy Mou]

Ok. Could you possibly help me fix my group instance:

instance : Group XorNat where
  mul x y := open XorNat in match x, y with
    | mk x, mk y => mk (x ^^^ y)
  mul_assoc a b c := by
      simp [(· * ·)]
      apply Nat.xor_assoc
  one := XorNat.mk 0
  one_mul := by
      simp [(· * ·)]
      intros
      rw [Nat.zero_xor]
  mul_one := by
      simp [(· * ·)]
      rw [Nat.xor_zero]
  inv x := x
  mul_left_inv := by
      simp [(· * ·)]
      rfl

In particular, I'm having trouble with defining one_mul and mul_one: I want to use Nat.zero_xor, but it's not able to see that 1.n = 0 even though that's how I defined it.

[Eric Wieser]

You will find it a lot easier if you define Mul and One separately before doing anything else

[Eric Wieser]

here's the full example fro LftCM

[Eric Wieser]

Note how that once you set up the really boring lemmas, everything is obvious

[Timothy Mou]

That helps, thanks

[Kevin Buzzard]

If you call the instance XorNat.instgroup then can you get away without opening XorNat? This would work for a def or lemma so I suspect the same would be true here. (I dread to think what the autogenerated name would be)

[Timothy Mou]

Yes, that works. Thanks for the tip