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