Ssreflect Users Discussion List

[Georges Gonthier <>]

  Dear Florent and Assia,
  Many thanks for bringing a little life in this list with this interesting 
case study. Though the two of you have covered the topic quite well, there 
are a few observations I would like to add:
  - 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).
  - To answer Assia's main question, I think that in this particular case 
Florent's approach (#1) is the best one, since it lets him impose a specific 
enumeration of a specific representation.
  - As Assia points out, this is not convenient as it ought to be, because 
the generic countType construction afforded by an explicit enumeration is 
specialized to seq_sub in the library, for no good reason. To take advantage 
of it one would need to provide a bijection between subseqs and seq_sub 
(enum_subseqs w) and use the CanXxxMixin transfer functions (similarly to 
solution #2). That's not so much overhead (one lemma with a trivial proof), 
which would be partly redeemed by factoring out the two-line proof of 
val_seq_sub_enum (but with some fiddling with undup). However, I don't think 
that proof is sufficient grounds for duplicating seq_sub.
 - Enumerating subsequences via masks, as Assia suggests in #2 and #3, almost 
works: it would if the tuple library exposed the tuple enumeration: 
    Definition enum_tuples T n w :=
        iter n (fun e => [seq x :: s | x <- w, s <- e]) [:: Nil T].
    as Florent's definition
       Definition enum_subseqs T := foldr (fun x s => map (cons x) s ++ s) 
[:: Nil T].
   is provably equal to [seq mask m w | m <- enum_tuples (size w) [:: true; 
false]], using only (nested) induction and rewriting with the induction 
hypothesis.
   The tuple enumeration definition is only opaque for historical reasons: it 
was first made so when we encountered our first blocking problems with Coq's 
convertibility check, in the theory of permutations, and was not reversed 
when Finite.enum was made opaque.
 - Also, to remove a dummy undup in the enumeration via masks, one needs to 
show that it is duplicate-free, that is, that (fun m : (size w).-tuple bool 
=> mask m w) is injective. There's a rather ugly 3-line proof of that by 
induction on w - it doesn't compare favourably to the straightforward 4-line 
proof of uniq (enum_subseqs w).
 - Finally, let me recall some of the rationale for the 
eqType/choiceType/countType/finType hierarchy:
   + The first two (eqType and choiceType) are expected to hold for all data 
types, because they provably do so for concrete data (for which all objects 
have a finite description), and can be assumed for data types admitted 
axiomatically (such as real numbers). Therefore, we expect these structures 
will be inherited by subtypes.
  + The last (finType) definitely does not hold for all datatypes, so a 
subType could have either an inherited or an ad hoc finType structure. The 
finSubtype structure covers the two situations uniformly.
  + The middle (countType) structure is intermediate: it may not hold for 
axiomatized types, and its default definition for concrete datatypes may be 
impractically inefficient - so it may be useful to have an ad hoc counting 
function even for concrete datatypes.
 - 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.
 - 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.

 Cheers,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Florent Hivert
Sent: 22 September 2015 22:06
To: Assia Mahboubi
Cc: 

Subject: Re: [ssreflect] Fintype for the subsequences of a sequence

      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://na01.safelinks.protection.outlook.com/?url=https:%2f%2fwww.lri.fr%2f~hivert%2fCoq-Combi%2f&data=01%7C01%7Cgonthier%40064d.mgd.microsoft.com%7C3105caa3f8884fbde56708d2c3921195%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=7dkUSsAvsIddRHz7V3wcsKUdq24Ut6FNXVcc3rYY3KQ%3d>
 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