## Stream: math-comp users

### Topic: Vector spaces -- not finite dimensional

#### Julien Puydt (Feb 07 2022 at 08:21):

Are abstract vector spaces where "free L" doesn't require a finite L and use dimension computations to define the notion available somewhere?

#### Julien Puydt (Feb 10 2022 at 09:16):

I'm trying my hand at something simple, but not managing to get along that well:

``````  Lemma free_by_inj: forall n: nat, forall L:n.-tuple E, injective u -> free L -> free (map u L).
Proof.
move=> n L inju.
move/freeP => freeL.
apply/freeP.
move=> k lincomb0.
``````

and here I'm stuck because I don't know how to express that lincomb(f)=f(lincomb). Then I'll probably be stuck expressing that f(lincomb)=0 means lincomb=0... but then I'll know I'll be able to apply my freeL hypothesis and win.

#### Cyril Cohen (Feb 10 2022 at 17:36):

Julien Puydt said:

Are abstract vector spaces where "free L" doesn't require a finite L and use dimension computations to define the notion available somewhere?

No at the current time there is no such development, if there were, it would be in a library which accept classical logic (such as mathcomp/analysis)...

#### Cyril Cohen (Feb 10 2022 at 17:38):

Julien Puydt said:

I'm trying my hand at something simple, but not managing to get along that well:

``````  Lemma free_by_inj: forall n: nat, forall L:n.-tuple E, injective u -> free L -> free (map u L).
Proof.
move=> n L inju.
move/freeP => freeL.
apply/freeP.
move=> k lincomb0.
``````

and here I'm stuck because I don't know how to express that lincomb(f)=f(lincomb). Then I'll probably be stuck expressing that f(lincomb)=0 means lincomb=0... but then I'll know I'll be able to apply my freeL hypothesis and win.

I miss some context to answer this...
(I mean, litterally the context variables)

#### Cyril Cohen (Feb 10 2022 at 17:46):

OK, I guessed your context, here is one way to continue your proof:

#### Cyril Cohen (Feb 10 2022 at 17:46):

``````From mathcomp Require Import all_ssreflect all_algebra.

Local Open Scope ring_scope.
Import GRing.Theory.

Section test.
Variables (R : fieldType) (E : vectType R).

Lemma map_free (u : {linear E -> E}) (n : nat) (vs : n.-tuple E) :
injective u -> free vs -> free (map u vs).
Proof.
move=> inju freeL; apply/freeP => k /= /eqP.
under eq_bigr do rewrite (nth_map 0) ?size_tuple// -linearZ.
by rewrite -linear_sum raddf_eq0// => /eqP; apply: freeP.
Qed.

End test.
``````

#### Cyril Cohen (Feb 10 2022 at 17:48):

Thus, the missing pieces you were asking for were `linear_sum` and `raddf_eq0`, which are both generic theorems about linear and additive maps.

#### Julien Puydt (Feb 10 2022 at 22:09):

Thanks! I'll have to study it: I think (nth_map 0) makes no sense for me, the "under eq_bigr do ..." isn't familiar, and I'm pretty sure at some point I knew why apply and apply: were different. You guessed my environment quite right ; the only difference is that I had (R: fieldType) (E F: vectType R) (u: 'Hom(E, F)) because I didn't want an endomorphism.

#### Julien Puydt (Feb 11 2022 at 15:43):

Ok, why is the freeP lemma expressed with = 0 while the raddf_eq0 is expressed with == 0?

That is the reason why the proof has several /eqP. That's not what bothers me the most, but I'm starting with what seem more low-hanging fruits

#### Julien Puydt (Feb 11 2022 at 17:16):

Let me rewrite the example with comments to be clearer on what I get (or not) from the various steps:

``````From mathcomp Require Import all_ssreflect all_algebra.

Local Open Scope ring_scope.
Import GRing.Theory.

Section rewrite_from_Cyril_Cohen.

Variables (R : fieldType) (E F : vectType R) (u : 'Hom(E, F)).

Lemma map_free (n : nat) (vs : n.-tuple E) : injective u -> free vs -> free (map u vs).
Proof.
move=> inju freeL. (* usual introductions *)
apply/freeP => k. (* classical freeness, introducing a family of scalars *)
move => /eqP. (* switch = 0 to == 0 *)
under eq_bigr do rewrite (nth_map 0) ?size_tuple//. (* unclear sum manipulation *)
under eq_bigr do rewrite -linearZ. (* linear maps are homogeneous *)
rewrite -linear_sum. (* linear maps are additive *)
rewrite raddf_eq0 //. (* classical injectivity -- uses == 0 *)
move => /eqP. (* switch back from == 0 to = 0 *)
by apply:freeP. (* recognize the goal as expressing a freeness *)
Qed.

End rewrite_from_Cyril_Cohen.
``````

#### Cyril Cohen (Feb 14 2022 at 10:06):

Ok, why is the freeP lemma expressed with = 0 while the raddf_eq0 is expressed with == 0?

This is again because of the constructive setting in mathcomp, boolean equality makes reasoning easier since equivalences are equalities (and thus can be rewritten with) and the excluded middle holds. Sometimes it is thus preferable to use `_ == _` and sometimes `_ = _`.

Last updated: Feb 08 2023 at 07:02 UTC