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:
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.
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
ton.-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 andby []
/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: Oct 13 2024 at 01:02 UTC