## Stream: math-comp users

### Topic: Length of ord_enum list

#### Julin Shaji (Oct 10 2023 at 16:51):

I was trying to prove this: forall n:nat, List.length (ord_enum n) = n.

How would we go about that?

I started with:

Goal forall n:nat,
length (ord_enum n) = n.
Proof.
move => n.
case: n => //.
move => n.
(*

1 subgoal

n : nat

========================= (1 / 1)

length (ord_enum n.+1) = n.+1
*)


#### Julin Shaji (Oct 10 2023 at 16:52):

I guess unfold-ing isn't that popular in mathcomp?

#### Paolo Giarrusso (Oct 10 2023 at 17:32):

generally, in math-comp you should probably use Search a lot more than you're used to

#### Julin Shaji (Oct 10 2023 at 17:36):

Knowing what (and how) to search for takes experience, I guess. :grimacing:

#### Paolo Giarrusso (Oct 10 2023 at 17:36):

re unfolding I've asked the same question, and people pointed out that both the rewrite tactic and by []/done will do some unfolding for you. But I think you're right that you use unfolding less than, say, in early Software Foundations or CPDT

#### Paolo Giarrusso (Oct 10 2023 at 17:39):

here's one approach:

1. open mathcomp/ssreflect/seq.v: searching length finds this:
(*         size s == the number of items (length) in s.                       *)
Fixpoint size s := if s is _ :: s' then (size s').+1 else 0.

1. so maybe we can split your goal into length xs = size xs and size (ord_enum n) = n

#### Paolo Giarrusso (Oct 10 2023 at 17:40):

length xs = size xs should work either by reflexivity/by [] (if you're lucky, because the definitions in fact coincide) or by induction on xs

#### Paolo Giarrusso (Oct 10 2023 at 17:55):

for the second I was expecting an existing lemma... I managed via the following (on math-comp 2), but this seems tricky enough that either (1) there's a much simpler proof (2) this should be upstreamed.

Set Warnings "-notation-overridden".
From mathcomp Require Import all_ssreflect.

Lemma length_size {A} (xs : seq A) : List.length xs = size xs.
Proof. by []. Qed.

Lemma size_ord_enum n : size (ord_enum n) = n.
Proof. by rewrite -{3}(size_iota 0 n) -val_ord_enum size_map. Qed.


lemmas used, for reference:

Lemma size_map s : size (map f s) = size s.
Lemma val_ord_enum : map val ord_enum = iota 0 n.
Lemma size_iota m n : size (iota m n) = n.


#### Paolo Giarrusso (Oct 10 2023 at 17:56):

Updated with both proofs.

#### Karl Palmskog (Oct 10 2023 at 18:34):

I agree size_ord_enum could be useful in MathComp itself, but is length_size really valuable? Not sure that connection to Stdlib is very interesting

#### Paolo Giarrusso (Oct 10 2023 at 20:53):

I wasn't suggesting length_size in math-comp, or the stdlib, but any devs that must talk to both might need it.

#### Paolo Giarrusso (Oct 10 2023 at 20:55):

I agree that in this stream often the answer is "you probably want size not length in your statement", unless you must interface with other libraries as well.

#### Paolo Giarrusso (Oct 10 2023 at 20:56):

(I've written such lemmas linking stdpp and stdlib).

#### Paolo Giarrusso (Oct 10 2023 at 20:58):

I hope somebody can upstream size_ord_enum or a better proof, and I release it under the needed license — I'm sorry I'm pretty sure I won't get to it

#### Emilio Jesús Gallego Arias (Oct 10 2023 at 22:33):

Just a different proof for fun:

Lemma size_ord_enum n : size (ord_enum n) = n.
Proof.
have/eq_in_count eqC : {in (iota 0 n), ltn^~n =1 predT}.
by move=> x; rewrite mem_iota.
by rewrite size_pmap_sub eqC count_predT size_iota.
Qed.


#### YAMAMOTO Mitsuharu (Oct 10 2023 at 23:21):

Yet another proof:

Lemma size_ord_enum n : size (ord_enum n) = n.
Proof. by move: (size_enum_ord n); rewrite enumT unlock. Qed.


#### Julin Shaji (Oct 11 2023 at 05:44):

Thanks! I was trying to have a way to convert 'M_(rows, cols) to a Vector.t (Vector.t cols) rows.
It looked as if length was needed for that. With the length_size and size_ord_enum lemmas, I could define it.
But not sure if it got defined correctly.

Definition mkRow {A:Type} {rows cols:nat}
(r: 'I_rows) (f: 'I_rows -> 'I_cols -> A): Vector.t A cols.
refine(
match r with
| @Ordinal _ r' _ =>
let cids := Vector.of_list (ord_enum cols) in (* list 'I_cols *)
let rw := Vector.map (fun cid => f r cid) cids in
_
end).
move: rw.
by rewrite length_size size_ord_enum.
Defined.

Definition mkMat {A:Type} {rows cols:nat}
(f: 'I_rows -> 'I_cols -> A): Vector.t (Vector.t A cols) rows.
Proof.
refine(
let rids := Vector.of_list (ord_enum rows) in (* list 'I_rows *)
let rws := Vector.map (fun rid => mkRow rid f) rids in
_).
move: rws.
by rewrite length_size size_ord_enum.
Defined.


Compute gives a complicated term. Is it possible to get a 'lean/slimmer' term? Without the things that ssreflect adds for proofs?

Example eg3 := \matrix_(i<3, j<7)
(fun i j => if i==j :> nat then 1 else 0%:Z).

Compute mkMat (fun_of_matrix eg3).
(*
= match
match
length_size
match
match idP with
| ssrbool.ReflectT _ x => Some (Ordinal (n:=3) (m:=0) x)
| ssrbool.ReflectF _ _ => None
end
with
| Some x =>
x
....
....
....
....
| ssrbool.ReflectF _ _ => None
end
with
| Some x => [:: x]
| None => [::]
end
end
end))
: Vector.t (Vector.t (nat -> nat -> int_Ring) 7) 3
*)


#### Julin Shaji (Oct 11 2023 at 05:49):

And I was also worried about the type of the last line being: Vector.t (Vector.t (nat -> nat -> int_Ring) 7) 3 instead of a simpler type.

#### Julin Shaji (Oct 11 2023 at 05:51):

Is refine not usually used in mathcomp proofs?

#### Julin Shaji (Oct 11 2023 at 05:51):

And is the fun_of_matrix of square matrices different than that of non-square matrices? As in when getting a specific element from the matrix.

#### Paolo Giarrusso (Oct 11 2023 at 06:29):

mathcomp provides tuple as a replacement for Vector

#### Paolo Giarrusso (Oct 11 2023 at 06:30):

re Compute, you probably need EAL for something that works well

#### Julin Shaji (Oct 11 2023 at 06:58):

I am trying to extract out the matrix after proving some theorems. Would converting \matrix to n.-tuple be a better option for that?
Any idea?

Also, could getting familiar with https://math-comp.github.io/htmldoc/mathcomp.algebra.vector.html be of help?

#### Paolo Giarrusso (Oct 11 2023 at 07:05):

Okay, I see you've discussed coqeal in the other stream, I don't know any better than the experts there. What I can say is that some of the things your proof is blocked on are in part due to vector — but not only: even if mkMat is Defined, using rewrite that way will produce a proof that tries to compute length_size when run

#### Paolo Giarrusso (Oct 11 2023 at 07:07):

OTOH, a tuple is a dependent pair of a list xs, and a proof that xs has the expected size: that way, if you're careful, you can write things so that the list reduces fully while the proof remains opaque (which is good for Coq performance).

#### Julin Shaji (Oct 11 2023 at 07:38):

Found this: https://hal.science/hal-01251943/document

There they represent vectors using n.-tuple like that. That sounds like something that could help. Reading it now.

#### Pierre Roux (Oct 11 2023 at 08:12):

Julin Shaji said:

I am trying to extract out the matrix after proving some theorems. Would converting \matrix to n.-tuple be a better option for that?
Any idea?

Using CoqEAL you could have two instances of your program: one with matrices for convenient proofs and another with lists of lists to compute/extract (but painful for proofs), any result proved on the first being valid on the second thanks to a refinement proof. This is probably much easier than trying to use Vector.t. The main drawback of CoqEAL being that the documentation is a bit scarce.

Julin Shaji said:

Also, could getting familiar with https://math-comp.github.io/htmldoc/mathcomp.algebra.vector.html be of help?

This is a theory of (finite dimension) vector fields, so maybe not what you're looking for.

#### Karl Palmskog (Oct 12 2023 at 10:56):

we need more demos and documentation for CoqEAL for sure. Maybe with MetaCoq it could be feasible to automate more of the refinement setup process

#### Cyril Cohen (Oct 12 2023 at 11:07):

Karl Palmskog said:

we need more demos and documentation for CoqEAL for sure. Maybe with MetaCoq it could be feasible to automate more of the refinement setup process

There is actually a generalization of CoqEAL on its way. More news soon.

#### Karl Palmskog (Oct 12 2023 at 11:09):

there was one notable recent use of MathComp to get easier proofs in program verification, but to my knowledge it didn't use CoqEAL

#### Julin Shaji (Oct 17 2023 at 08:27):

Paolo Giarrusso said:

generally, in math-comp you should probably use Search a lot more than you're used to

Is it possible to use notations as well with Search?

I was trying to see lemmas involving \sum_.

Search \sum_. didn't work (reference not found).

#### Julin Shaji (Oct 17 2023 at 08:42):

Oh, wait.. I had used it with quotes.

This kind worked.

    Search (\row_(_<_) _).


#### Ana de Almeida Borges (Oct 17 2023 at 10:07):

It is indeed possible, but you need to search for the full notation IIUC. So for sum it would be Search (\sum_(_ <- _ | _) _) or something like that.

#### Ana de Almeida Borges (Oct 17 2023 at 10:08):

And since such a large number of results for sums are actually valid for other big operators and thus stated in more general cases, you won't find them if searching only for \sum, but you can try Search (\big[_/_]_(_ <- _ | _) _).

#### Pierre Roux (Oct 17 2023 at 10:45):

In the end, it's probably easier to equivalently Search bigop.

#### Julin Shaji (Oct 17 2023 at 14:15):

What's \big? Is it just a way to say 'something big' while searching?

Or is there something more to it?
https://math-comp.github.io/htmldoc/mathcomp.ssreflect.bigop.html

#### Julin Shaji (Oct 17 2023 at 14:18):

bigop does match \sum. Is it they are defined with it?

#### Julin Shaji (Oct 17 2023 at 17:41):

Paolo Giarrusso said:

re unfolding I've asked the same question, and people pointed out that both the rewrite tactic and by []/done will do some unfolding for you.

I guess rewrite /name is similar to unfold name as well.

#### Paolo Giarrusso (Oct 17 2023 at 18:36):

Yes, but unfolding a definition from other libraries can make your proof more fragile

#### Paolo Giarrusso (Oct 17 2023 at 18:38):

Re bigop, this name is used because bigops generalize various folds which are usually written using big Greek letters, like Σ and \Pi for big sums and big products

#### Julin Shaji (Oct 18 2023 at 04:15):

Paolo Giarrusso said:

Yes, but unfolding a definition from other libraries can make your proof more fragile

Is there a way to simplify without explicit unfolding? Generally speaking.

#### Paolo Giarrusso (Oct 18 2023 at 08:29):

simpl / /= and rewrite ?

#### Paolo Giarrusso (Oct 18 2023 at 08:30):

Instead of unfolding foo try to use lemmas about it, especially rewrite with them

Last updated: Jul 25 2024 at 15:02 UTC