Hello, in an example I am developing for teaching purposes, I would like to find the smallest structure where I can use both `mulrz_neq0`

and `mulfK`

. Is there an easy to find that out?

`numFieldType`

would suffice:

```
From mathcomp Require Import all_ssreflect all_algebra.
(*
The lemmas `mulrz_neq0` and `GRing.mulfK` respectively applies to any
`numDomainType` and `fieldType`.
*)
Check mulrz_neq0.
Check GRing.mulfK.
(*
To find the smallest structure that inherits from both `numDomainType` and
`fieldType` (so called "join" of structures), we can lookup the table of
canonical structure instances.
*)
Print Canonical Projections Num.NumDomain.sort GRing.Field.sort.
(*
GRing.Field.sort <- Num.NumDomain.sort ( join_Num_NumField_between_GRing_Field_and_Num_NumDomain )
*)
Print join_Num_NumField_between_GRing_Field_and_Num_NumDomain.
(*
join_Num_NumField_between_GRing_Field_and_Num_NumDomain =
fun R : numFieldType => {| Num.NumDomain.sort := R; Num.NumDomain.class := Num.NumDomain.class R |}
: numFieldType -> numDomainType
Arguments join_Num_NumField_between_GRing_Field_and_Num_NumDomain R
*)
```

The database of minimal structures that inherit from arbitrary pairs of two structures is available as the table of canonical structure instances, although it is not very user-friendly.

Alternative methods:

- use
`HB.graph`

but the graph is rapidly too big to be easily readable - declare a structure like

```
HB.structure Definition test := { T of GRing.Field T & Num.NumDomain T}.
```

and read the answer in the error message:

```
Error: Structure Num_NumField contains the same mixins as test
```

Thanks @Kazuhiko Sakaguchi and @Pierre Roux , this is quite enlightening. It particularly interesting that the error message already contains the needed computation.

Maybe this would be a great addition to HB.howto

Not trivia though

Similar tooling work exists in mathlib: https://ceur-ws.org/Vol-3377/fmm12.pdf

The work is IMO about finding the 2 structures out of the lemma names.

Once you have that the query is trivial, eg `Check (erefl _ : S1.sort _ = S2.sort _).`

Last updated: Jul 25 2024 at 15:02 UTC