Stream: math-comp users

Topic: Useful lemmas about the free predicate?


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

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

view this post on Zulip Pierre Boutry (Dec 13 2023 at 14:53):

Because there is no linearly independent sequence of vectors v1v_1, v2v_2, ... vn+2v_{n+2} in Rn+1R^{n+1}?

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

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

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

view this post on Zulip Pierre-Yves Strub (Dec 13 2023 at 15:16):

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

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

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

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

view this post on Zulip Laurent Théry (Dec 14 2023 at 14:40):

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

view this post on Zulip Laurent Théry (Dec 14 2023 at 14:58):

the PR


Last updated: Jul 25 2024 at 15:02 UTC