Ssreflect Users Discussion List

[Assia Mahboubi <>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear list,

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.

We have at least three options, and I would be glad to hear about other
suggestions and/or comments about these.

1) Florent's solution
(https://github.com/hivert/Coq-Combi/blob/master/theories/Combi/subseq.v)

- - Define this finite type as the boolean sigma-type:

  Structure subseqs : predArgType :=
     Subseqs {subseqsval :> seq T; _ : subseq subseqsval s}.

- - Implement a function enumerating the sub-sequences of its argument 
(possibly
with duplicates):
  Fixpoint enum_subseqs w :=
    if w is w0 :: w' then
      let rec := enum_subseqs w' in [seq w0 :: s | s <- rec ] ++ rec
    else [:: [::] ].

- - Prove that (undup (enum_subseqs s)) enumerates the elements of subseqs and
use this fact to forge the finType structure.

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.

Cons: Almost no reuse of existing machinery (but not very expensive either).
Worst, because of the inheritance graph of the hierarchy, imposing to
construct a choice and count mixin before the finite one, we hit the problem
of non canonicity of the choice structure on (seq T). In fact, to make this
work easily, Florent relaxed (T : eqType) to
(T : countType) and used some ad hoc constructions of  finType of his own
(https://github.com/hivert/Coq-Combi/blob/master/theories/Combi/combclass.v),
that kind of emulate seq_sub (see below).


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.

  Lemma subofmaskP t : subseq (subofmask t) s.

  Lemma codom_subofmask w : w \in codom subofmask = subseq w s.

  Definition subOfMask : (size s).-tuple bool -> subseqs :=
    fun t => Subseqs (subofmaskP t).

  Definition maskOfSub (w : subseqs) : (size s).-tuple bool :=
    iinv (subOfMask_surj w).

  Lemma maskOfSubK : cancel maskOfSub subOfMask.

Pros: rather cheap.
Cons: The automation by computation is lost.

3) Adopt a different definition, using the encoding as the primitive
definition and use the seq_sub construction provided by the fintype library:

  Variable (T : choiceType).
  Variable s : seq T.

  Definition subofmask : (size s).-tuple bool -> seq T := fun m => mask m s.

  Definition subseqs_seq : seq (seq T) := codom subofmask.

  Notation subseqs := (seq_sub subseqs_seq).

That's it. We have equality, choice and finite structures canonically:

  Variables (t : subseqs) (p : pred subseqs).
  Check ((t == t) && (#|p| == 0)).

Pros: very cheap.
Cons: Still no computation. Also it is only a little bit cheaper than 2) as we
still need to exhibit some lemmas to relate subseqs and the subseq predicate,
for instance the codom_subofmask and subseqs_seqP lemmas. But we are saved
from the boilerplate code.
Finally, we had to promote T to a choice type, as again the mixins are  not
canonical. And I did not manage to see how to benefit from the
adhoc_seq_sub_choiceType and adhoc_seq_sub_finType (and mixin) definitions
available in fintype.v in case we keep T an eqType...

Kind regards,

assia
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)

iQIcBAEBAgAGBQJWAUHuAAoJEFY7bbrolXGxEhEP/3zEKtQmjdz88jSuKrr4rKqt
lTj/OcJ4CEVgkab12SqOJCp8tGqzvF1UXRKQjis+fY+f0mFtalI7M5rP5dYGcR1V
SUZ9dC8bjCOQJLFxg6R+p8VFUAJtdvcSEHnMNkSxHt3x/JfKiViJ8xB57nxwVwmF
wjlCFsVaCr/JfNPr5WAMl/Ldwj+rZpcP1mzxFr5xmqidYk4xo1QKZUmjuJXgpixI
wb6VKV2Qtqipe5++8zV7cZizeskzrp+2Sk4sDj0jFRzUURMI5pd2IeiGYAl02NS/
GOr0Q5ZS6v/3hCrC66fjzRXcodMD+X4wWT6HkWVe61uYxTgKTK4DAz/Whx6I/CYG
mF7sZpiacGCs+7/4Y0hpCCbaYscI3E7RiIK7eeJfirxyiXMyMaD3DUNFkxqnpDEL
LIAW+7+OLVnD1bBEayXyWNJmw4a+ZQhNNDp7EWxIA0D5Nig3rxQnadSwtrnBNuqQ
ZETdufEXNDyhG91dYi2jMMKFnZgWPheIVDr3xCVHo7PLqoDsWbUuWDGKhYJPbvYA
0OmkamkEVHXuGsiSYLoIenTijDqAQbMAvtK0uWUGgfr7/dUIwPc1DUzzpK+F7G2I
ZqJ4/X/gQE96kbAHwcbl9d6B16/131RU9zDRmaJdLSYE0p4wLPNAYcTJvYb+F/rf
5anqwPS8kVQcxK3iahCM
=YL8k
-----END PGP SIGNATURE-----