I am trying to follow the 2020 article about HB to learn how to use it.

I try to type the examples while reading and cannot define the Ring structure on `Z`

.

Somehow, Coq cannot unify `add`

and Z's `+`

.

Here is my last attempt:

```
HB.instance Definition Z_Monoid : Monoid_of_Type Z :=
@Monoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_0_l Z.add_0_r.
HB.instance Definition Z_Ring : Ring_of_Monoid Z :=
@Ring_of_Monoid.Build Z 1%Z Z.opp Z.mul Z.add_opp_diag_l Z.add_opp_diag_r
Z.mul_assoc Z.mul_1_l Z.mul_1_r Z.mul_add_distr_r Z.mul_add_distr_l.
(*
Definition illtyped: The term "Z.mul_add_distr_r" has type
"forall n m p : Z, ((n + m) * p)%Z = (n * p + m * p)%Z"
while it is expected to have type "left_distributive Z.mul add"
(cannot unify "((n + m) * p)%Z = (n * p + m * p)%Z" and
"(add n m * p)%Z = add (n * m)%Z (m * p)%Z").
*)
```

The rest of the file might be relevant, I enclose it. I may have forgotten to `Set`

some crucial option.

Coq version is 8.19.0, coq-elpi is 2.0.2 and coq-hierarchy-builder is 1.7.0.

article.v

You definition of left_distributive is buggy ;-)

I don't know why it does not print the infix notation in the error message, but `add (n * m)%Z ...`

and `n * p + ...`

are not equal

I think these files are tested in CI: https://github.com/math-comp/hierarchy-builder/tree/master/examples/FSCD2020_material

There is a preamble that redefines the combinators from ssrfun.

I don't know why, but it redefines them. And they contain a typo

Last updated: Oct 13 2024 at 01:02 UTC