Lean: how to use the refine_struct tactic for commutative ring structures?

Question

Suppose I want to make bool (i.e. the type {ff,tt} of boolean values) into a commutative ring. The following works:

instance : comm_ring bool := {
  zero := ff,
  add := bxor,
  neg := id,
  one := tt,
  mul := band,
  zero_add      := by { repeat { rintro ⟨_⟩ };  refl },
  add_zero      := by { repeat { rintro ⟨_⟩ };  refl },
  one_mul       := by { repeat { rintro ⟨_⟩ };  refl },
  mul_one       := by { repeat { rintro ⟨_⟩ };  refl },
  add_left_neg  := by { repeat { rintro ⟨_⟩ };  refl },
  add_comm      := by { repeat { rintro ⟨_⟩ };  refl },
  mul_comm      := by { repeat { rintro ⟨_⟩ };  refl },
  add_assoc     := by { repeat { rintro ⟨_⟩ };  refl },
  mul_assoc     := by { repeat { rintro ⟨_⟩ };  refl },
  left_distrib  := by { repeat { rintro ⟨_⟩ };  refl },
  right_distrib := by { repeat { rintro ⟨_⟩ };  refl }
}

In other words, I define zero=false, addition=xor and so on. Then I have to check a bunch of identities, each of which is quantified over one, two or three variables of type bool. I introduce as many variables as necessary, split cases according to whether each variable is true or false, and then just apply the definitions to check that the axiom holds in each case.

The refine_struct tactic is supposed to tidy up this sort of thing. My expectation was that this would work:

instance : comm_ring bool := begin
 refine_struct { zero := ff, add := bxor, neg := id, one := tt, mul := band };
 repeat { rintro ⟨_⟩ };
 refl
end

Here the refine_struct tactic is supposed to create 11 goals, one for each of the axioms zero_add,...,right_distrib. This is followed by the tactics repeat { rintro ⟨_⟩ } and refl. The three tactics are separated by semicolons so each tactic is applied to all goals generated by the previous tactic. I had code similar to this which worked correctly in November 2021. However, this approach now fails.

If we replace the semicolon after refine_struct {...} by a comma and place the cursor there, we see the list of goals created by refine_struct. Firstly, the documentation for refine_struct says that these goals should be tagged with the names of the corresponding fields (i.e. zero_add, mul_assoc and so on), but I do not see any tags (in VS Code); am I misunderstanding something here? Secondly, there are actually 23 goals rather than 11, some of which are goals to supply extra structures rather than verify axioms. By comparison with mathlib's ring structure on the reals, I gather that we need to supply the subtraction map bool → bool → bool, scalar multiplication maps ℕ → bool → bool and ℤ → bool → bool and the power map ℕ → bool → bool, and then verify that these satisfy certain axioms. However, in my first approach all this is done silently and automatically. Is there a way to make refine_struct work as it did before?

Answer 1

What changed since November 2021​​​ is that comm_ring got several new data members in order to resolve various diamond issues. refine_struct does not supply these members, and although you can supply the default value it requires you to stage the definition, not going straight to comm_ring but building up from at least a few of the ancestor classes first.

It's not super satisfactory, but this works:

import tactic

instance : comm_ring bool := begin
  letI : has_zero bool := ⟨ff⟩,
  letI : has_one bool := ⟨tt⟩,
  letI : has_add bool := ⟨bxor⟩,
  letI : has_mul bool := ⟨band⟩,
  letI : has_neg bool := ⟨id⟩,
  refine_struct { zero := ff, add := (+), neg := id, one := tt, mul := (*),
    sub := (+), nsmul := nsmul_rec, npow := npow_rec, zsmul := zsmul_rec };
  repeat { rintro ⟨_⟩ };
  refl
end