Stream: math-comp analysis

Topic: linear_zmodtype


view this post on Zulip 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 ?

view this post on Zulip Reynald Affeldt (Feb 11 2022 at 10:39):

U and V are expected to be lmodType R

view this post on Zulip 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.           *)

view this post on Zulip Reynald Affeldt (Feb 11 2022 at 10:40):

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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Marie Kerjean (Feb 11 2022 at 11:23):

Yes, this is what I am doing now.

view this post on Zulip 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 :-/)

view this post on Zulip Marie Kerjean (Feb 11 2022 at 11:24):

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

view this post on Zulip Reynald Affeldt (Feb 11 2022 at 11:25):

Same here. Please let me know.

view this post on Zulip 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) ?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Marie Kerjean (Feb 11 2022 at 12:08):

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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Feb 11 2022 at 12:12):

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

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Feb 11 2022 at 12:15):

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

view this post on Zulip 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 !

view this post on Zulip Marie Kerjean (Feb 11 2022 at 12:17):

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

view this post on Zulip Cyril Cohen (Feb 11 2022 at 12:30):

Just From mathcomp Require Import vector.

view this post on Zulip Cyril Cohen (Feb 11 2022 at 12:30):

What is your problem?

view this post on Zulip 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?

view this post on Zulip Marie Kerjean (Feb 11 2022 at 12:31):

I am working with lmodtype

view this post on Zulip Cyril Cohen (Feb 11 2022 at 12:32):

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

view this post on Zulip Marie Kerjean (Feb 11 2022 at 12:32):

ok, back to canonical definitions then :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Marie Kerjean (Feb 11 2022 at 12:36):

I should be ok, thanks !

view this post on Zulip Marie Kerjean (Feb 11 2022 at 13:43):

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

view this post on Zulip Reynald Affeldt (Feb 11 2022 at 13:52):

(This is indeed the constructor.)

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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