ssreflect - Re: [ssreflect] Expected behavior of partition

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Expected behavior of partition

From: BEGAY Pierre-leo <>
To:
Subject: Re: [ssreflect] Expected behavior of partition
Date: Mon, 16 Dec 2019 16:59:50 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
Ironport-phdr: 9a23:i8Yp/hLDeqZLbTGg79mcpTZWNBhigK39O0sv0rFitYgRI/jxwZ3uMQTl6Ol3ixeRBMOHsqkC0bKL+PC5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMhm6sQXcusYVjId/N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqJFrhy8qRxwwYDbb52aO/Vjca3QZs8aSGldUspNSyBMGIGxYo0SBOQBJ+ZYqIz9qkMToBWxBAehGOHgwSJSiH/3w6I6yf4hHh/f0AwkAd0Ot2nfodLtNKgJT++1w7PHzDXYYvxI3zf985HEfQw7rv6QXbJ/a8zRxVMhFwPfl1idr5HuMT2S1uQIqWeb7uxgWPqgi24mtwFxoiWvydw2hobVgYIVz1bJ/jh6zoYtPdC0VUB2bN2+HJdOuSyWKpF6Tt4gTmxpoio3yrILtYa4cSQX0pgqxxDSZ+aZf4SW+B7uWuKcLDFlj3x/Yr2/nQy98U24x+38SMa01FFKozJfndnWt3ACzRrT5daZRvdn4Eih3y2P2xnP5e5ePU80lbDUK5g7zr4+jJofqUXDHinol0XqlKKaa0sp9+uy5+j5bLjqu4WQO5J2hwz/KKgjmsOyDfw9MgcUXmib/eq81Kfk/U38WLhKluY5nbfWsJ/AJcUWvbC2AwlO0oo69xmwFSup0NQCknkBNl5FdgiHg5DzO17SOPD4Eeu/g1O0nTdw3PDGJKPuApvJLnfdjLjhYa1w61VcyQo21dBQ/YhYCrAHIPLpW0/+rsbUDhEjM1/8/+GyE85n240aVGmTKqqCKubTt0WJ76QuJfONbckbomXTMf8gstTDolYI0WcccLOz0N4TZXfwSuxsLkqQcFLhhMxEGm4BvgM4CuLw3g7RGQVPbmq/CvpvrgowD5irWN+aG9KdxYeZ1SL+JaV4I2BLDlfWSiXhbYSNXfpWLi+UOYpqmzcEXL7nRZVzjEjy5j+/8KJuK6/vwgNdrYjqjYUn6uvI0Bo7/jx9CYKTyTPVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUFR9FV/LZCWww6PJiawfYoUt0=

Okay, I now see I tricked myself the moment I wrote a set as {x,x}.

Thanks for you reply,
Pierre-Léo

Florent Hivert
<>
a écrit :

There can't be multiple occurrences of an element in a set, ie duplicates are
removed automatically by definition.

By the way you might want to have a look at

https://github.com/hivert/Coq-Combi/blob/master/theories/LRrule/Greene.v

where I defined a similar notion for a sequence:

Definition trivIseq (u : seq {set T}) : Prop :=
forall i j, i < j < size u -> [disjoint (nth set0 u i) & (nth set0 u j)].

Best,

Florent

[ssreflect] Expected behavior of partition, BEGAY Pierre-leo, 12/16/2019
- Re: [ssreflect] Expected behavior of partition, Florent Hivert, 12/16/2019
  - Re: [ssreflect] Expected behavior of partition, Florent Hivert, 12/16/2019
    - Re: [ssreflect] Expected behavior of partition, BEGAY Pierre-leo, 12/16/2019
- Re: [ssreflect] Expected behavior of partition, Georges Gonthier, 12/16/2019
  - Re: [ssreflect] Expected behavior of partition, BEGAY Pierre-leo, 12/16/2019

List archive

Re: [ssreflect] Expected behavior of partition