## Stream: math-comp users

### Topic: Finding the smallest structure with two properties

#### Yves Bertot (Sep 11 2023 at 11:33):

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?

#### Kazuhiko Sakaguchi (Sep 11 2023 at 11:50):

`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
*)
``````

#### Kazuhiko Sakaguchi (Sep 11 2023 at 11:54):

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.

#### Pierre Roux (Sep 11 2023 at 12:54):

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}.
``````

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

#### Yves Bertot (Sep 11 2023 at 15:13):

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

#### Enrico Tassi (Sep 11 2023 at 18:20):

Maybe this would be a great addition to HB.howto

#### Enrico Tassi (Sep 11 2023 at 18:20):

Not trivia though

#### Kazuhiko Sakaguchi (Sep 12 2023 at 13:48):

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

#### Enrico Tassi (Sep 12 2023 at 14:02):

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