While section function_space in topology.v allows to sum l l' : (U -> V)
when V : zmodtype
, this does not seem to extend to l l' : { linear U -> V}
. Are there canonical definitions missing on linear function space or am I doing something wrong ?
U and V are expected to be lmodType R
(* {linear U -> V} == the interface type for linear functions, i.e., a *)
(* Structure that encapsulates the linear property *)
(* for functions f : U -> V; both U and V must have *)
(* lmodType R structures, for the same R. *)
and indeed it seems to work in that case (not really I mistyped \+)
Indeed, I was testing if when U V : lmodType R
and it fails for me :
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Context (R : numFieldType) (U : lmodType R) (V : lmodType R).
Variables (f g : U -> V ).
Check (f + g).
Variables (l l': {linear U -> V}).
Fail Check (l + l').
with
The term "l" has type "{linear U -> V}" while it is expected to have type
"GRing.Zmodule.sort ?V".
Goal ((l : U -> V) + l') = ((l' : U -> V) + l).
by rewrite addrC.
but this is not satisfactory
Can you define this?
Canonical linear_zmodType (R : ringType) (T M : lmodType R) := ZmodType {linear T -> M} (linear_zmodMixin T M).
This would make your example go through but I cannot right now figure out the code for linear_zmodMixin.
Yes, this is what I am doing now.
(It shouldn't be too hard if you are accustomed to ssralg, I am failing to use the notation correctly right now :-/)
But I am rusted on on ssralg structure, so it's taking me some time :-)
Same here. Please let me know.
How am I supposed to prove Linear _ = Linear _
, that is the equality between two linear functions (I want to use funeqE on the underlyong functions) ?
Hi, in mathcomp core, linear
has to be distinguished from 'Hom(_, _)
which is what I think you are looking for.
linear
is the structure to infer linearity, while 'Hom(_, _)
is has algebraic structural properties (you can perform this addition you desperatly want on it)
The correpondance is given by the linfun
interface which gives you everything you need to go back and forth
This is deeply rooted in mathcomp strategic bias to be very conservative wrt to Coq axioms, without which it is impossible to have linearity be both a structure and an extensional object (because of both the absence of functional extensionality and general proof irrelevance without axioms)
Haaaaa, that's it, great, thank you very much !
Cyril Cohen said:
This is deeply rooted in mathcomp stragedic bias to be very conservative wrt to Coq axioms, without which it is impossible to have linearity be both a structure and an extensional object (because of both the absence of functional extensionality and general proof irrelevance without axioms)
Could that be simplified in mc-analysis or is it not possible/not worth it ?
That could totally be simplified, and I guess it would be worth it, even though it would create a lot of redundancy
but that (redundancy) is a burden we already bear...
In particular a lot of vector space theory and field extension theory is tied to 'Hom(_, _)
and it would be really problematic to have to duplicate it...
Do you think you could live with 'Hom(_, _)
and use linfun
and lfunE
explicitly?
Cyril Cohen said:
Do you think you could live with
Hom(_, _)
and uselinfun
andlfunE
explicitly?
For the moment completely, it was more of a rhetorical question. Thank you for all the explanations !
Still trying to make 'Hom(_, _)
work though, is there something to be imported ?
Just From mathcomp Require Import vector.
What is your problem?
oh, I see!!! You probably need a finite dimensional vector space as of today... you are not in a finite dimension context are you?
I am working with lmodtype
If not, there is no way around definition {linear _ -> _} as a zmodule
ok, back to canonical definitions then :-)
You can do it by subtyping, just by proving linearity is closed under addition though, as in https://github.com/math-comp/analysis/blob/18a3c6d315ffd425e13e6e9c19fce5e90f275d43/theories/lebesgue_integral.v#L625-L709
We can make a short call to get you started with this technique, or you can build it from scratch, as you prefer
I should be ok, thanks !
What is the equivalent of FiniteSum.Build
here ? Just Linear
?
(This is indeed the constructor.)
Marie Kerjean said:
What is the equivalent of
FiniteSum.Build
here ? JustLinear
?
Linear
is the equivalent of the 3 lines here https://github.com/math-comp/analysis/blob/18a3c6d315ffd425e13e6e9c19fce5e90f275d43/theories/lebesgue_integral.v#L631-L633
Any idea why here I need to define the linearity predicate with an explicite GRing.Scale.op
? If I juste declare the predicate as Definition linear_pred : {pred U -> V} := mem [set f | linear f].
then Linear (set_mem linear_pred)
does not typecheck. Is there some classical Hint
that I should have ?
Your question seem to turn around the same ideas that I'm about in the mathcomp- users stream: how linearity works within mathcomp.
I was still having trouble with linear
as a predicate. Definition linear_pred : {pred U -> V} := mem [set f | linear f].
does not work while it works when unfolding the notation linear: Definition linear_pred : {pred U -> V} := mem [set f | lmorphism_for *:%R f]
. Is that to be expected or is there a way around it ?
I'm afraid I really don't know this area of the math-comp. I do see the problem you're describing. But if there is an straightforward solution, it's something beyond my abilities.
Marie Kerjean said:
(solved, message deleted)
Could you please restore your message and post your solution? It puzzled me and it can help people to understand what you did.
Last updated: Feb 09 2023 at 02:02 UTC