Stream: math-comp users

Topic: Finding the smallest structure with two properties


view this post on Zulip 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?

view this post on Zulip 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
*)

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Sep 11 2023 at 12:54):

Alternative methods:

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 11 2023 at 18:20):

Maybe this would be a great addition to HB.howto

view this post on Zulip Enrico Tassi (Sep 11 2023 at 18:20):

Not trivia though

view this post on Zulip Kazuhiko Sakaguchi (Sep 12 2023 at 13:48):

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

view this post on Zulip 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