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
*)
```

I guess `unfold`

-ing isn't that popular in mathcomp?

generally, in math-comp you should probably use `Search`

a lot more than you're used to

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

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

here's one approach:

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

- so maybe we can split your goal into
`length xs = size xs`

and`size (ord_enum n) = n`

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

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

Updated with both proofs.

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

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

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.

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

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

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

Yet another proof:

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

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
*)
```

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.

Is `refine`

not usually used in mathcomp proofs?

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.

mathcomp provides `tuple`

as a replacement for `Vector`

re `Compute`

, you probably need EAL for something that works well

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?

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

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

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.

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.

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

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.

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

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

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

This kind worked.

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

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.

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[_/_]_(_ <- _ | _) _).`

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

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

`bigop`

does match `\sum`

. Is it they are defined with it?

Yes, those are just notations

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/bigop.v#L662

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/bigop.v#L629

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.

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

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

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.

simpl / `/=`

and rewrite ?

Instead of unfolding `foo`

try to use lemmas about it, especially rewrite with them

Last updated: Jul 25 2024 at 15:02 UTC