Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Assia, dear SSReflect experts,

First of all, I'd like to take to opportunity of my first message on this
mailing list to thank you all for the tremendous work ! It changed me from a
"know a little about coq" to a real Coq-Addict ;-)

> Florent Hivert (cc-ed) asked me about the best way to construct a 
> canonically
> finite type whose elements are the sub-sequences of a given sequence
> (s : seq T), where (T : eqType).
> 
> I have not yet understood why he needs this to be a *type* (as opposed to a
> simple sequence or tuple), but may be he will be able to comment this point
> better than I can.

I'm not sure either I really need a type for the particular use case we spoke
about last Friday. Maybe It's something like I'd rather write a statement
saying that two sets have the same cardinality than that a statement saying
that two sequence have the same length and then that they enumerate the
correct sets. However the pattern of building a boolean subtype sigma-type
(see below) knowing the list of its elements is quite common in my code, with
probably a dozen of instance. Writing recursive code enumerating all the
elements of a set is the B-A-BA of writing code in combinatorics. Proving such
a code correct is quite routine.

By the way, I'm in the process of commenting my code. You may want to consult
<https://www.lri.fr/~hivert/Coq-Combi/> which will be the documented version
of my code. Lot's of file needs more doc. This is a work in progress.

> Pros: automation. For Florent, it seems very useful to have a computational
> behaviour for the enumeration of the sub-sequences. Like in:
>
>   Goal perm_eq (undup (enum_subseqs [:: 1; 1]))  [:: [::]; [:: 1]; [:: 1; 
> 1]].
>   by [].
>   Qed.

Let me comment more about that point using the mask solution:

> 2) With the same definition for type subseqs, obtain all the mixins ans
> structures needed by encoding this type into tuples of booleans.
> 
>   Definition subofmask : (size s).-tuple bool -> seq T := fun m => mask m s.

Admittedly my first example is quite exotic. The following is clearly the
first application. In my opinion, It should be automatic:

Lemma enum_subseqs_nil (T : eqType) : @enum_subseqs T [::] = [:: [::]].
Proof.
  case H: (enum_subseqs [::]) => [//=| s0 [//= | s1 s]].
  - have := @sub0seq T [::]; by rewrite -mem_enum_subseqs H.
  - have := @sub0seq T [::]; by rewrite -mem_enum_subseqs H inE => /eqP <-.
  - exfalso.
    have := undup_uniq (codom (@subofmask T [::])).
    rewrite -/(@enum_subseqs T [::]) H /= => /and3P [].
    rewrite negb_or => /andP [] Habs _ _ _.
    move: Habs.
    have -> : s0 = [::].
      apply /eqP; by rewrite -subseq0 -mem_enum_subseqs H inE eq_refl.
    have -> : s1 = [::].
      apply /eqP; by rewrite -subseq0 -mem_enum_subseqs H !inE eq_refl orbT 
/=.
    by rewrite eq_refl.
Qed.

Let's give a though about the corresponding statement for enum_subseqs (w0 ::
w). Using mask below, I'm not sure I can rely on having tuple enumerated in a
specific order. Even more, I don't know if the order of the enumeration
explicit or is it hidden behind some abstraction ? If it's hidden, I'll end up
with a statement as

   perm_eq
     (enum_subseqs w0 :: w')
     (undup [seq w0 :: s | s <- enum_subseq w'] ++ (enum_subseq w'))

which tells the same recursion as my fixpoint definition:

>   Fixpoint enum_subseqs w :=
>     if w is w0 :: w' then
>       let rec := enum_subseqs w' in [seq w0 :: s | s <- rec ] ++ rec
>     else [:: [::] ].

So that it seems to me much simpler to first write this fixpoint and then show
that it correctly enumerate subseq (with duplicate it there are some in w).

Thanks for any comments ! I hope to have soon finished to comment my code and
not too later to have a paper about it.

Cheers,

Florent