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 ?
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?
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.
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.
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.
Indeed, ilunitP should be after the second builder.
So ?
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)
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.
I see, maybe using a kind of feather factory: https://github.com/math-comp/hierarchy-builder/wiki/FeatherFactory
Ok. Thank for the pointer. That looks non trivial, but that might solve my problem... I need time to experiment with that.
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...
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: Oct 13 2024 at 01:02 UTC