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?

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

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

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.

Maybe using `free_cons`

, `basisEfree`

and `span_basis`

(but I don't know that part of the library very well either).

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

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

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

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

Even so, I find surprising that one has to unfold the definition of `free`

. It kinds of break the abstraction.

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

the PR

Last updated: Jul 25 2024 at 15:02 UTC