Stream: math-comp users

Topic: Length of ord_enum list


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

view this post on Zulip Julin Shaji (Oct 10 2023 at 16:52):

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

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

view this post on Zulip Julin Shaji (Oct 10 2023 at 17:36):

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:56):

Updated with both proofs.

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 20:56):

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

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

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

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

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

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

view this post on Zulip Julin Shaji (Oct 11 2023 at 05:51):


Is refine not usually used in mathcomp proofs?

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

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 06:29):

mathcomp provides tuple as a replacement for Vector

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 06:30):

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Julin Shaji (Oct 17 2023 at 08:42):

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

This kind worked.

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

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

view this post on Zulip 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[_/_]_(_ <- _ | _) _).

view this post on Zulip Pierre Roux (Oct 17 2023 at 10:45):

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

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

view this post on Zulip Julin Shaji (Oct 17 2023 at 14:18):

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

view this post on Zulip Pierre Roux (Oct 17 2023 at 14:29):

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

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

view this post on Zulip Paolo Giarrusso (Oct 17 2023 at 18:36):

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 08:29):

simpl / /= and rewrite ?

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 08:30):

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


Last updated: Oct 13 2024 at 01:02 UTC