## Stream: math-comp users

### Topic: Useful lemmas about the free predicate?

#### Pierre Boutry (Dec 13 2023 at 14:43):

Hello everyone,

For a proof of negation that I am doing, I think I can obtain that there is a free n.+2.-tuple 'rV_(n.+1). I believe this should let me obtain false in the context thus allowing me to complete the proof. However, from a quick look at the available lemmas, I don't see an obvious way to do it. @Reynald Affeldt suggested that asking here might be a good idea. Could someone point me to some useful lemmas?

#### Pierre Roux (Dec 13 2023 at 14:45):

Why do you expect false? A n.+2 tuple of n.+1 vectors is mostly a n.+2 x n.+1 matrix isn it?

#### Pierre Boutry (Dec 13 2023 at 14:53):

Because there is no linearly independent sequence of vectors $v_1$, $v_2$, ... $v_{n+2}$ in $R^{n+1}$?

#### Quentin VERMANDE (Dec 13 2023 at 15:00):

I only gave a quick look at vector.v, but it looks like you can unfold free to make the dimension of the subspace your tuple generates appear. Then you can probably assert that this subspace is included in the full space and take the dimensions.

#### Pierre Roux (Dec 13 2023 at 15:02):

Maybe using free_cons, basisEfree and span_basis (but I don't know that part of the library very well either).

#### Pierre-Yves Strub (Dec 13 2023 at 15:15):

From mathcomp Require Import all_ssreflect all_algebra.

Parameter (k : fieldType).

Lemma where_the_hell_is_it {n : nat} : dim 'rV[k]_n = n.
Proof. by rewrite /dim /= mul1n. Qed.

Lemma L {n : nat} (t : n.+1.-tuple 'rV[k]_n) : ~~ free t.
Proof.
rewrite /free size_tuple ltn_eqF // ltnS.
apply: (leq_trans (dimvS (subvf <<t>>))).
by rewrite dimvf where_the_hell_is_it.
Qed.


#### Pierre-Yves Strub (Dec 13 2023 at 15:16):

This gives me the opportunity to say how I hate this part of mathcomp :)

#### Pierre Boutry (Dec 13 2023 at 15:24):

Pierre-Yves Strub said:

From mathcomp Require Import all_ssreflect all_algebra.

Parameter (k : fieldType).

Lemma where_the_f_ck_is_it {n : nat} : dim 'rV[k]_n = n.
Proof. by rewrite /dim /= mul1n. Qed.

Lemma L {n : nat} (t : n.+1.-tuple 'rV[k]_n) : ~~ free t.
Proof.
rewrite /free size_tuple ltn_eqF // ltnS.
apply: (leq_trans (dimvS (subvf <<t>>))).
by rewrite dimvf where_the_f_ck_is_it.
Qed.


Thanks :) I did not expect you to do the proof for me, just giving me a pointer. I'll go back to packing...

#### Laurent Théry (Dec 14 2023 at 14:30):

@Pierre-Yves Strub
Yes the dimension of the matrix space could deserve an explicit ittle lemma I will make a PR.
An inlined version of your proof is

Lemma L {n : nat} (t : n.+1.-tuple 'rV[k]_n) : ~~ free t.
Proof.
rewrite neq_ltn size_tuple ltnS (leq_trans (dimvS (subvf <<t>>))) // dimvf [X in X <= _]mul1n.
Qed.


#### Pierre-Yves Strub (Dec 14 2023 at 14:33):

Even so, I find surprising that one has to unfold the definition of free. It kinds of break the abstraction.

#### Laurent Théry (Dec 14 2023 at 14:40):

you would like the definition of free to be explicitely a lemma too?

#### Laurent Théry (Dec 14 2023 at 14:58):

the PR

Last updated: Jul 25 2024 at 15:02 UTC