Ssreflect Users Discussion List

[Georges Gonthier <>]

  The lemma you're looking for is count_filter, which doesn't have count in 
its name but does show up in 
      Search count filter.
This give the following script:
       rewrite -!size_filter uniq_leq_size ?filter_uniq // => x.
       by rewrite !mem_filter => /andP[-> /SUB].
  Also note you can state your SUB assumption more elegantly as {subset l1 <= 
l2}, and that your lemma name should include an "r" suffix to indicate the 
inclusion is for the right argument (suffixless lemmas in the library are for 
predicate inclusion, e.g., has_sub, all_sub, etc; right inclusions are not 
well covered).
    Cheers,
Georges

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

 
[mailto:]
 On Behalf Of Felipe Cerqueira
Sent: 19 January 2016 10:59
To: 

Subject: [ssreflect] count of subsequence (different lists)

Hi,

I'm having troubles to prove the following lemma about count.
Could you point me to the right direction?

Lemma count_sub_uniq :
   forall (T: eqType) (l1 l2: seq T) P,
     uniq l1 ->
     subpred (mem l1) (mem l2) ->
     count P l1 <= count P l2.

The closest I got to the proof was this:

  UNIQ : uniq l1
   SUB : subpred (T:=T) (mem l1) (mem l2)
   ============================
    count (fun x : T => P x && (mem l2) x) l1 <= count P l2

At this point, I though about using the subseq/filter lemmas, but I didn't 
know what to do.

Thanks,
Felipe