Stream: Hierarchy Builder devs & users

Topic: `Error: elpi: subst-fun: not a lambda` while porting dioid


view this post on Zulip Pierre Roux (Mar 04 2021 at 22:55):

@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?

view this post on Zulip Cyril Cohen (Mar 04 2021 at 23:00):

@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?

view this post on Zulip Pierre Roux (Mar 05 2021 at 07:48):

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

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:35):

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

view this post on Zulip Pierre Roux (Mar 05 2021 at 08:36):

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.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:38):

It is forbidden to use Build without providing the key, we should put a nice error message for that. Thanks

view this post on Zulip Pierre Roux (Mar 05 2021 at 08:49):

I guess the key is the "TheType" parameter?

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:50):

yes, in your case it is eenat

view this post on Zulip Pierre Roux (Mar 05 2021 at 08:52):

then I don't see were I broke the rule, the underscores in PredSubSemiRing.Build _ _ _ _ eenat are parameters coming before TheType

view this post on Zulip Enrico Tassi (Mar 05 2021 at 08:54):

Maybe Set Implicit Arguments.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:56):

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.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:58):

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

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:59):

we'll see

view this post on Zulip Cyril Cohen (Mar 05 2021 at 08:59):

Anyway HB should report a nicer message.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 11:04):

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

view this post on Zulip Enrico Tassi (Mar 05 2021 at 11:35):

Know what?

view this post on Zulip Cyril Cohen (Mar 05 2021 at 11:36):

Whether @Pierre Roux diagnose something thanks to your presentation

view this post on Zulip Pierre Roux (Mar 05 2021 at 18:38):

@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?

view this post on Zulip Enrico Tassi (Mar 05 2021 at 18:51):

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
  )
].

view this post on Zulip Pierre Roux (Mar 05 2021 at 18:53):

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

view this post on Zulip Enrico Tassi (Mar 05 2021 at 18:55):

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.

view this post on Zulip Enrico Tassi (Mar 05 2021 at 18:55):

But, is this the thing that fails?

view this post on Zulip Pierre Roux (Mar 05 2021 at 18:56):

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

view this post on Zulip Enrico Tassi (Mar 05 2021 at 18:57):

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

view this post on Zulip Enrico Tassi (Mar 05 2021 at 18:58):

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

view this post on Zulip Pierre Roux (Mar 05 2021 at 18:59):

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

view this post on Zulip Enrico Tassi (Mar 05 2021 at 19:00):

Ah, then it must be the same root cause.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:02):

We usually maximally eta expand mixins, so that the funs correspond to the prods... I did not put hd-beta because I do not want things to be applied more that what we expect in the first place...

view this post on Zulip Enrico Tassi (Mar 05 2021 at 19:02):

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}

view this post on Zulip Enrico Tassi (Mar 05 2021 at 19:03):

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

view this post on Zulip Pierre Roux (Mar 05 2021 at 19:12):

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»)])

view this post on Zulip Pierre Roux (Mar 05 2021 at 19:29):

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

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:33):

I think I know what this is...

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:34):

I think this would solve the problem.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:34):

The section discharge struck once more

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:38):

If you are using nix, you can set hierarchy-builder.override.version = "#181"; in your .nix/config.nix to try it out

view this post on Zulip Pierre Roux (Mar 05 2021 at 19:41):

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

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:41):

Yes, I figured there is another one

view this post on Zulip Pierre Roux (Mar 05 2021 at 19:42):

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

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:45):

Thanks

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:45):

The problem is slightly more subtle than what I thought.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:46):

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.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 19:47):

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

view this post on Zulip Pierre Roux (Mar 05 2021 at 19:52):

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

view this post on Zulip Pierre Roux (Mar 05 2021 at 20:01):

for instance with a Proof using f

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:06):

Yes, I'm working on it

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:09):

Ahahah ok

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:10):

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.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:10):

(if you write HB.instance Definition _ : PreSemiRing U := semiringU.) it should work

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:11):

(instead of HB.instance U semiringU)

view this post on Zulip Cyril Cohen (Mar 05 2021 at 20:11):

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.

view this post on Zulip Cyril Cohen (Mar 05 2021 at 22:13):

Cf math-comp/hierarchy-builder#182 now


Last updated: Jan 29 2023 at 16:02 UTC