ssreflect - [ssreflect] count of subsequence (different lists)

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] count of subsequence (different lists)

From: Felipe Cerqueira <>
To: "" <>
Subject: [ssreflect] count of subsequence (different lists)
Date: Tue, 19 Jan 2016 11:59:06 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:U+J7yh05v6HPZYmssmDT+DRfVm0co7zxezQtwd8ZsegeKfad9pjvdHbS+e9qxAeQG96LtbQV2qGO7+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6MyZXmnLjus7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKSr7gcqo8QLdEJDE9KSU04tfqvF/CSxGO7z0SSC9exgFTGQXL6BzxQr/0qTG/t+xn2SDcPMvsTLlyVy70vIlxTxq9pioDNiY0uErakNVtgaNBqVr1qRF7wpbZa6mQLPs7ZbzGO9QASjwSDY5qSyVdD9bkPMM0BO0bMLMAog==

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

[ssreflect] count of subsequence (different lists), Felipe Cerqueira, 01/19/2016
- RE: [ssreflect] count of subsequence (different lists), Georges Gonthier, 01/19/2016

List archive

[ssreflect] count of subsequence (different lists)