Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Georges,

Many thanks for your detailed answer.

> - First, from the description of Florent's needs, it seems that his needs
> would be better addressed with Cyril Cohen's (still) forthcoming finmap
> library. The latter would let him represent sets of subsequences as finite
> sets over a choiceType, allowing him to combine them freely (say, to talk
> about the number of common subsequences of two different words), while also
> being able to use them as finTypes (say, for indexing a bigop).

Looks very promising for me ! Working in (Algebraic) Combinatorics, I always
have to consider finite subset of a countable set. So from what I just seen It
seems to fulfill my need.

>  - Finally, let me recall some of the rationale for the 
> eqType/choiceType/countType/finType hierarchy:
>  - The adhoc_choiceType for seq_sub should be used with the cloning 
> construct:
>      Definition subseqs w := seq_sub (enum_subseqs w).
>      ...
>     Canonical subseqs_choiceType w := [choiceType of subseqs w for 
> adhoc_seq_sub_choiceType _].
>     Canonical subseqs_countType w := [countType of subseqs w for 
> adhoc_seq_sub_finType _].
>     Canonical subseqs_finType w := [countType of subseqs w for 
> adhoc_seq_sub_finType _].
>     ...
>    As explained in the documentation, using an ad hoc structure may cause 
> issues in contexts that use both choiceType and subType operations, e.g., 
> sigW and val.

I'm not following you. It seems from you and Assia's email that there is this
'adhoc_choiceType' structure but I can't find it (I'm using SSreflect and
MathComp 1.5 from <http://ssr.msr-inria.inria.fr/>). Is it in some development
version ? If so it this version accessible ?

>  - Finally, I have to disagree with Florent's long proof of 
> enum_subseqs_nil. There are very short non-computational proofs, using 
> either enum1 and eq_enum, or perm_eq_small.

Thanks ! I missed those possibilities.

Regards,

Florent