Stream: Hierarchy Builder devs & users

Topic: Getting a definition/lemma outside a builder


view this post on Zulip Florent Hivert (Nov 26 2023 at 22:51):

I have a large builder for a unitRing structure. Here is an extract:

HB.factory Record InvLim_isUnitRingInvLim
[...]
HB.builders Context
[...]
  TLim of InvLim_isUnitRingInvLim _ _ _ _ Sys TLim.

Implicit Type x y : TLim.

HB.instance Definition _ :=
  InvLim_isRingInvLim.Build _ _ _ _ Sys TLim.

Definition ilunit x := `[< forall i, 'pi_i x \is a unit >].

[...]
Fact ilunit_impl x y : y * x = 1 /\ x * y = 1 -> ilunit x.
[...]

HB.instance Definition _ :=
  GRing.Ring_hasMulInverse.Build TLim
    ilmulVr ilmulrV ilunit_impl ilinv0id.

HB.end.

Now, I would like to have he following lemma:

Lemma ilunitP (x : TLim) :
  reflect (forall i, 'pi_i x \is a unit) (x \is a unit).
Proof. exact: asboolP. Qed.

This proof is perfectly accepted inside the builder, but then I can't use it. Now If I try to get the same proof in a theory section outside the builder:

Section InvLimUnitRingTheory.
[...]
Variable TLim : unitRingInvLimType Sys.

Lemma ilunitP (x : TLim) :
  reflect (forall i, 'pi_i x \is a unit) (x \is a unit).
Proof.

I can't manage to get the proof because the definition of ilunit is now hidden.
Is there a way to get either the definition of ilunit or the lemma ilunitP out of the builder ?

view this post on Zulip Quentin VERMANDE (Nov 27 2023 at 06:44):

It looks like the command HB.builders starts by opening a module and HB.end closes it. Giving #[verbose] or #[log] to HB.builders should give you a rough idea of what happens. Therefore, an "obvious" solution would be to refer to the constant defined inside the module, or even declare an alias for it outside the module. However, this will break easily when you modify the code preceding the builder since the name of the module might depend on it. The only other solution I can see is to define ilunit and/or prove ilunitP before the builder.
Regarding this particular example, are you sure that the statement of ilunitP (outside the builder) uses your instance?

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:30):

I can't prove ilunitP before the builder, because the role of the builder is to define a unitRingType instance on TLim which is needed to give sense to the statement (x \in a unit). My problem is that before HB I could deconstruct the unit ring mixin to convert the statement (x \in a unit) to its definition namely ilunit x. Now I don't know how to do that.

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:38):

I guess you would have to cut the factory in two: a first factry with a builder with the first HB.instance (InvLim_isRingInvLim.Build) then the definition of ilunit and ilunitP outside of any factory and finally a second factory with a builder with the second eHB.instance (GRing.Ring_hasMulInverse.Build). The expected behavior can be retrieved with a third factory whose builder would simply combine the two previous one.

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:43):

How would that link the tow statement (x \in a unit) and ilunit x ? Again I can't write the former statement before having the second builder.

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:46):

Indeed, ilunitP should be after the second builder.

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:47):

So ?

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:52):

Since the definition of ilunit is outside builders it should become accessible in the proof of ilunitP (maybe other things should be extracted from the builder, potentially putting them in a module to avoid polluting the namespace)

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:56):

My problem is not to access to ilunit but to manage to unfold the definition of (x \in a unit) which should ultimately boils down to ilunit x. Once I manage to do that I'm done.

view this post on Zulip Pierre Roux (Nov 27 2023 at 08:06):

I see, maybe using a kind of feather factory: https://github.com/math-comp/hierarchy-builder/wiki/FeatherFactory

view this post on Zulip Florent Hivert (Nov 27 2023 at 08:08):

Ok. Thank for the pointer. That looks non trivial, but that might solve my problem... I need time to experiment with that.

view this post on Zulip Florent Hivert (Nov 27 2023 at 09:06):

Thinking about it, that look suspiciously complicated. For example, how to you prove that in a direct product of group, one has (e1, f1) * (e2, f2) = (e1 * e2, f1 * f2) ? Anyway, in my case that made me realize that iluntP should't be proved from the implementation, but from the interface. That is, it should be true with a different implementation...

view this post on Zulip Pierre Roux (Nov 27 2023 at 12:06):

For (e1, f1) * (e2, f2) = (e1 * e2, f1 * f2) it should be enough to by [] sinc ethe definition of * on pairs should match the right hand side (rewrite /GRing.mul/= should show it). In your case, I guess the implementation was hidden inside the builder.


Last updated: Apr 21 2024 at 01:02 UTC