@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 beforeTheType
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: Oct 13 2024 at 01:02 UTC