@Cyril Cohen so I tried to build substructures taking inspiration of PredSubZmodule in ssralg and when giving such factories to HB.instance, I get errors like

```
elpi: subst-fun: not a lambda: app [...]
```

Is that a common/expected error?

@Pierre Roux Thanks for reporting, "common/expected error" start with "HB:", if not (like here), it means we failed to check something... Are you using the `master`

branch of HB?

@Cyril Cohen yes, so I'm minimizing the example to share it

Ah show me the code first... maybe I can guess

Well, just reduced it, so here it is (last line fails):

```
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
HB.mixin Record IsSemiRing R := {
zero : R;
add : R -> R -> R;
add0d : left_id zero add;
}.
HB.structure Definition SemiRing := {R of IsSemiRing R}.
Notation "0" := (@zero _).
Infix "+" := (@add _).
Definition add_closed {R : SemiRing.type} (S : {pred R}) :=
0 \in S /\ {in S &, forall u v, u + v \in S}.
Module Pred.
Structure add V S := Add {add_key : pred_key S; _ : @add_closed V S}.
Lemma add_ext (U : SemiRing.type) S k (kS : @keyed_pred U S k) :
add_closed kS -> add_closed S.
Proof.
by case=> S0 addS; split=> [|x y]; rewrite -!(keyed_predE kS) //; apply: addS.
Qed.
Module Exports.
Coercion add_key : add >-> pred_key.
Notation addPred := add.
Definition AddPred U S k kS DkS := Add k (@add_ext U S k kS DkS).
End Exports.
End Pred.
Export Pred.Exports.
Section SemiRingPred.
Variables (V : SemiRing.type) (S : {pred V}).
Variables (addS : addPred S) (kS : keyed_pred addS).
Lemma rpred0D : add_closed kS.
Proof. split=> [|x y]; rewrite !keyed_predE; case: addS=> _ [_]//; exact. Qed.
Lemma rpred0 : (@zero V) \in kS.
Proof. by case: rpred0D. Qed.
Lemma rpredD : {in kS &, forall u v, (@add V u v) \in kS}.
Proof. by case: rpred0D. Qed.
End SemiRingPred.
HB.factory Record PreSemiRing U := {
V : SemiRing.type;
f : U -> V;
zero : U;
add : U -> U -> U;
injf : injective f;
f0 : f zero = 0;
fD : {morph f : x y / add x y >-> x + y};
}.
HB.builders Context U of PreSemiRing U.
Program Definition semiringU := @IsSemiRing.Build U zero add _.
Next Obligation. by move=> x; apply: injf; rewrite fD f0 add0d. Qed.
HB.instance U semiringU.
HB.end.
HB.factory Record PredSubSemiRing (V : SemiRing.type) (S : {pred V})
(subS : addPred S) (kS : keyed_pred subS) U of SUB V (mem kS) U := {}.
HB.builders Context (V : SemiRing.type) (S : {pred V})
(subS : addPred S) (kS : keyed_pred subS) U
of PredSubSemiRing V S subS kS U.
Let inU v Sv : U := Sub v Sv.
Let zeroU := inU (rpred0 kS).
Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).
Program Definition semiringU := @PreSemiRing.Build U V _ zeroU addU val_inj _ _.
Next Obligation. by rewrite SubK. Qed.
Next Obligation. by move=> x y; rewrite SubK. Qed.
HB.instance U semiringU.
HB.end.
(** nat extended with -oo and +oo *)
Variant enat := ENFin of nat | ENPInf | ENMInf.
Definition ezero := ENMInf.
Definition adden (x y : enat) :=
match x, y with
| ENFin x, ENFin y => ENFin (maxn x y)
| ENPInf, _ | _, ENPInf => ENPInf
| ENMInf, x | x, ENMInf => x
end.
Lemma add0en : left_id ezero adden.
Proof. by case. Qed.
HB.instance Definition _ := IsSemiRing.Build enat add0en.
Definition evenenat_def (x : enat) : bool :=
match x with
| ENPInf | ENMInf => true
| ENFin x => ~~ odd x
end.
Definition evenenat := [qualify a x | evenenat_def x].
Record eenat := {
eenat_val :> enat;
eenat_prop : eenat_val \is a evenenat
}.
HB.instance Definition _ := BuildSubTypeFor eenat eenat_val.
Lemma eenat_add_closed : add_closed evenenat.
Proof.
split=> [// | x y Hx Hy].
case: x Hx => [x||] Hx; case: y Hy => [y||] Hy //.
by rewrite /add /=; case: ltnP => _.
Qed.
Fact eenat_key : pred_key evenenat. Proof. by []. Qed.
Canonical eenat_keyed := KeyedQualifier eenat_key.
Canonical eenat_addPred := AddPred eenat_add_closed.
Definition eenat_semiring := PredSubSemiRing.Build _ _ _ _ eenat.
HB.instance eenat eenat_semiring.
```

It is forbidden to use `Build`

without providing the key, we should put a nice error message for that. Thanks

I guess the key is the "TheType" parameter?

yes, in your case it is `eenat`

then I don't see were I broke the rule, the underscores in `PredSubSemiRing.Build _ _ _ _ eenat`

are parameters coming before `TheType`

Maybe `Set Implicit Arguments.`

Pierre Roux said:

then I don't see were I broke the rule, the underscores in

`PredSubSemiRing.Build _ _ _ _ eenat`

are parameters coming before`TheType`

Sorry I read a bit too quickly... I was busy sending mails... we'll look into it after the meeting.

I think it's like Enrico is right it's maybe because there are implicit parameters....

we'll see

Anyway HB should report a nicer message.

Sorry I left while you were talking, thanks for letting us know indeed

Know what?

Whether @Pierre Roux diagnose something thanks to your presentation

@Cyril Cohen @Enrico Tassi I took a deeper look tonight and the error happens in `synthesis.private.mixin-for`

but I don't even understand why the code is executed since it is in the else branch of a `if`

whose guard is true?

Is this the code you are looking at? Did you put a `spy-do!`

?

```
mixin-for T M MI :- mixin-src T M Tm, !, std.do! [
std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped",
factory? Ty (triple Factory Params _),
if (M = Factory) (MI = Tm) (
private.builder->term Params T Factory M B,
coq.subst-fun [Tm] B MI
)
].
```

Indeed, I must confess I'm not familiar at all with logical programming and this could well have changed the behavior.

Anyway, this code can be improved by using `hd-beta`

instead of subst fun which would not fail if there is no lambda in head position in `B`

.

But, is this the thing that fails?

IIC yes, the coq.subst-fun complains about not being provided a function : `subst-fun: not a lambda`

replacing `coq.subst-fun [Tm] B MI`

by `unwind {hd-beta B [Tm]} MI`

should work around this issue, I don't know why the old code was expecting B to begin with a lambda

So either the invariant was wrong and the code has to be fixed as I say, or something else went south breaking the invariant.

this goes further: I get an error `declare-instances: mixin illtyped: Illegal application (Non-functional construction):`

I have to look further

Ah, then it must be the same root cause.

We usually maximally eta expand mixins, so that the `fun`

s correspond to the `prod`

s... I did not put `hd-beta`

because I do not want things to be applied more that what we expect in the first place...

if B is not a "function" (with an explicit lambda or not) then it cannot be applied, full stop. `subst-fun`

errors if it can't fire an head beta redex, while hd-beta does not fail, but generates the application `app[B, Tm]`

which is evidently wrong. I think you should print the term and see what it is, just write `coq.say B`

or `coq.say {coq.term->string B}`

ok, then "something else went south breaking the invariant" ;-)

here is B

```
(app
[global (const «Builders_5.PredSubSemiRing_to_IsSemiRing__8»),
global (const «enat_is_a_SemiRing»),
app
[global (const «has_quality»),
app [global (indc «S»), global (indc «O»)],
app
[global (const «SemiRing.sort»),
global (const «enat_is_a_SemiRing»)], global (const «evenenat»)],
global (const «eenat_addPred»),
app
[global (const «keyed_qualifier_keyed»),
app
[global (const «SemiRing.sort»),
global (const «enat_is_a_SemiRing»)],
app [global (indc «S»), global (indc «O»)],
global (const «evenenat»),
app
[global (const «Pred.add_key»),
global (const «enat_is_a_SemiRing»),
app
[global (const «has_quality»),
app [global (indc «S»), global (indc «O»)],
app
[global (const «SemiRing.sort»),
global (const «enat_is_a_SemiRing»)],
global (const «evenenat»)], global (const «eenat_addPred»)],
global (const «eenat_keyed»)], global (indt «eenat»),
global (const «HB_unnamed_factory_11»)])
```

And if I change the `subst-fun`

to `hd-beta`

, I get the following error

```
Error:
elpi: declare-instances: mixin illtyped: Illegal application (Non-functional construction):
The expression "Builders_41.PredSubSemiRing_to_IsSemiRing__44" of type
"forall (V : SemiRing.type) (S : {pred V}) (subS : addPred S)
(kS : keyed_pred subS) (U : Type),
SUB.mixin_of V (mem kS) U -> IsSemiRing.axioms_ U"
cannot be applied to the terms
"enat_is_a_SemiRing" : "SemiRing.type"
"has_quality 1 evenenat" : "{pred enat_is_a_SemiRing}"
"eenat_addPred" : "addPred evenenat"
"keyed_qualifier_keyed eenat_keyed" : "keyed_pred eenat_addPred"
"eenat" : "Set"
"HB_unnamed_factory_47" : "SUB.mixin_of enat (in_mem^~ (mem evenenat)) eenat"
"eenat_semiring"
: "PredSubSemiRing.axioms_ enat_is_a_SemiRing evenenat eenat_addPred
(keyed_qualifier_keyed eenat_keyed) eenat HB_unnamed_factory_47"
```

so indeed, there seems to be a missing last argument in `Builders_41.PredSubSemiRing_to_IsSemiRing__44`

I think I know what this is...

I think this would solve the problem.

The section discharge struck once more

If you are using nix, you can set `hierarchy-builder.override.version = "#181";`

in your `.nix/config.nix`

to try it out

Unfortunately, I still get the same error (thanks for the NIX solution, I should indeed give a try to nix at some point)

Yes, I figured there is another one

Well, at least my bug report isn't useless ;-)

Thanks

The problem is slightly more subtle than what I thought.

I had spotted it before for factory aliases which may forget some parameters/mixins, but it is actually the same for builder sections... So when we introduce the context we must remember to use it all.

But we do not want user defined local variables to weight in (or do we?)

Indeed, if I artificially use the factory in any part of the builder, it does work.

for instance with a `Proof using f`

Yes, I'm working on it

Ahahah ok

We perform a hack (a fake let in) but only if you use `HB.instance Definition ...`

(not `HB.instance`

).

Anyway, both the non-uniformity and the hack must go away.

(if you write `HB.instance Definition _ : PreSemiRing U := semiringU.`

) it should work

(instead of `HB.instance U semiringU`

)

cf this

```
% If you don't mention the factory in a builder, then Coq won't make
% a lambda for it at section closing time.
pred hack-section-discharging i:term, o:term.
hack-section-discharging B B1 :- current-mode (builder-from TheFactory _ _), !,
std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)",
B1 = {{ let _ : lp:TheFactoryTy := lp:TheFactory in lp:B }}.
hack-section-discharging B B.
```

Cf math-comp/hierarchy-builder#182 now

Last updated: Apr 21 2024 at 02:41 UTC