Stream: math-comp analysis

Topic: linear_zmodtype

Marie Kerjean (Feb 11 2022 at 10:09):

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 ?

Reynald Affeldt (Feb 11 2022 at 10:39):

U and V are expected to be lmodType R

Reynald Affeldt (Feb 11 2022 at 10:39):

(*        {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.           *)

Reynald Affeldt (Feb 11 2022 at 10:40):

and indeed it seems to work in that case (not really I mistyped \+)

Marie Kerjean (Feb 11 2022 at 10:46):

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".

Reynald Affeldt (Feb 11 2022 at 11:01):

Goal ((l : U -> V) + l') = ((l' : U -> V) + l).
by rewrite addrC.

but this is not satisfactory

Reynald Affeldt (Feb 11 2022 at 11:17):

Can you define this?
Canonical linear_zmodType (R : ringType) (T M : lmodType R) := ZmodType {linear T -> M} (linear_zmodMixin T M).

Reynald Affeldt (Feb 11 2022 at 11:22):

This would make your example go through but I cannot right now figure out the code for linear_zmodMixin.

Marie Kerjean (Feb 11 2022 at 11:23):

Yes, this is what I am doing now.

Reynald Affeldt (Feb 11 2022 at 11:24):

(It shouldn't be too hard if you are accustomed to ssralg, I am failing to use the notation correctly right now :-/)

Marie Kerjean (Feb 11 2022 at 11:24):

But I am rusted on on ssralg structure, so it's taking me some time :-)

Reynald Affeldt (Feb 11 2022 at 11:25):

Same here. Please let me know.

Marie Kerjean (Feb 11 2022 at 11:28):

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

Cyril Cohen (Feb 11 2022 at 12:05):

Hi, in mathcomp core, linear has to be distinguished from 'Hom(_, _) which is what I think you are looking for.

Cyril Cohen (Feb 11 2022 at 12:06):

linear is the structure to infer linearity, while 'Hom(_, _) is has algebraic structural properties (you can perform this addition you desperatly want on it)

Cyril Cohen (Feb 11 2022 at 12:06):

The correpondance is given by the linfun interface which gives you everything you need to go back and forth

Cyril Cohen (Feb 11 2022 at 12:08):

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)

Marie Kerjean (Feb 11 2022 at 12:08):

Haaaaa, that's it, great, thank you very much !

Marie Kerjean (Feb 11 2022 at 12:10):

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 ?

Cyril Cohen (Feb 11 2022 at 12:12):

That could totally be simplified, and I guess it would be worth it, even though it would create a lot of redundancy

Cyril Cohen (Feb 11 2022 at 12:12):

but that (redundancy) is a burden we already bear...

Cyril Cohen (Feb 11 2022 at 12:14):

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

Cyril Cohen (Feb 11 2022 at 12:15):

Do you think you could live with 'Hom(_, _) and use linfun and lfunE explicitly?

Marie Kerjean (Feb 11 2022 at 12:16):

Cyril Cohen said:

Do you think you could live with Hom(_, _) and use linfun and lfunE explicitly?

For the moment completely, it was more of a rhetorical question. Thank you for all the explanations !

Marie Kerjean (Feb 11 2022 at 12:17):

Still trying to make 'Hom(_, _) work though, is there something to be imported ?

Cyril Cohen (Feb 11 2022 at 12:30):

Just From mathcomp Require Import vector.

Cyril Cohen (Feb 11 2022 at 12:30):

What is your problem?

Cyril Cohen (Feb 11 2022 at 12:31):

oh, I see!!! You probably need a finite dimensional vector space as of today... you are not in a finite dimension context are you?

Marie Kerjean (Feb 11 2022 at 12:31):

I am working with lmodtype

Cyril Cohen (Feb 11 2022 at 12:32):

If not, there is no way around definition {linear _ -> _} as a zmodule

Marie Kerjean (Feb 11 2022 at 12:32):

ok, back to canonical definitions then :-)

Cyril Cohen (Feb 11 2022 at 12:34):

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

Cyril Cohen (Feb 11 2022 at 12:34):

We can make a short call to get you started with this technique, or you can build it from scratch, as you prefer

Marie Kerjean (Feb 11 2022 at 12:36):

I should be ok, thanks !

Marie Kerjean (Feb 11 2022 at 13:43):

What is the equivalent of FiniteSum.Build here ? Just Linear ?

Reynald Affeldt (Feb 11 2022 at 13:52):

(This is indeed the constructor.)

Cyril Cohen (Feb 11 2022 at 14:02):

Marie Kerjean said:

What is the equivalent of FiniteSum.Build here ? Just Linear ?

Linear is the equivalent of the 3 lines here https://github.com/math-comp/analysis/blob/18a3c6d315ffd425e13e6e9c19fce5e90f275d43/theories/lebesgue_integral.v#L631-L633

Marie Kerjean (Feb 11 2022 at 19:12):

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 ?

Julien Puydt (Feb 12 2022 at 08:27):

Your question seem to turn around the same ideas that I'm about in the mathcomp- users stream: how linearity works within mathcomp.

Marie Kerjean (Feb 24 2022 at 13:59):

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 ?

Zachary Stone (Feb 24 2022 at 22:47):

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.

Cyril Cohen (Feb 26 2022 at 13:36):

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: Aug 11 2022 at 01:03 UTC