Ssreflect Users Discussion List

[Florent Hivert <>]

    Dear all,

I'd like to build polynomials or series whose coefficients are polynomials or
series themself. More generally, if A is an R-algebra, then any module over A
is automatically a R-module. Here is a formalization of this fact:

  Variable (R : ringType) (A : lalgType R) (B : lmodType A).

  Definition scale_algmod (r : R) (b : B) : B := r%:A *: b.
  Lemma scale_algmodE r b : scale_algmod r b = in_alg A r *: b.
  Proof. by rewrite /scale_algmod -!in_algE. Qed.

  Program Definition algmod_lmodMixin :=
    @LmodMixin R [zmodType of B] scale_algmod _ _ _ _.
  Next Obligation. by rewrite !scale_algmodE scalerA -rmorphM in_algE. Qed.
  Next Obligation. by move=> b; rewrite scale_algmodE rmorph1 scale1r. Qed.
  Next Obligation. by move=> r b1 b2; rewrite scale_algmodE -scalerDr. Qed.
  Next Obligation. by move=> r1 r2; rewrite scale_algmodE -scalerDl raddfD. 
Qed.
  Canonical algmod_lmodType := Eval hnf in LmodType R B algmod_lmodMixin.

However after that

  Variable (R : ringType).
  Let Truc := [lmodType R of {poly {poly R}}].

I get the error

  Error:
  In environment
  R : ringType
  x : phantom (GRing.Lmodule.class_of R ?cT) (GRing.Lmodule.class ?cT)
  The term "x" has type
   "phantom (GRing.Lmodule.class_of R ?cT) (GRing.Lmodule.class ?cT)"
  while it is expected to have type
   "phantom (GRing.Lmodule.class_of R {poly {poly R}}) ?c".

which I interpret as "I can't manage to find an R-module structure for the
type {poly {poly R}}". Is that interpretation correct ? This seems to be
confirmed by

  Canonical bla_lmodType :=
      Eval hnf in LmodType R {poly {poly R}}
                     (algmod_lmodMixin [lmodType {poly R} of {poly {poly 
R}}]).

leading to the warning

  Warning: Ignoring canonical projection to poly_of by GRing.Lmodule.sort in
  bla_lmodType: redundant with poly_lmodType

Is my understanding correct that There Can Be Only One(tm) *-mod structure for
a type, even with different ring ? If so, is there a simple way to get around
this limitation. I imagine that one can define two trivially isomorphic
objects one for each structure, but I don't know how robust and practical this
can be. Any example of that ?

Best,

Florent