ssreflect - Re: [ssreflect] Expected behavior of partition

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Expected behavior of partition

From: Florent Hivert <>
To: BEGAY Pierre-leo <>,
Subject: Re: [ssreflect] Expected behavior of partition
Date: Mon, 16 Dec 2019 16:56:21 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:5HVR7hz+7TaD2f7XCy+O+j09IxM/srCxBDY+r6Qd2+kTIJqq85mqBkHD//Il1AaPAdyAragc1qGG6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe61+IAm2oAnetcQanJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLzliwJKyA2/33WisxojaJUvhShpwBkw4XJZI2ZLedycr/Bcd8fQ2dKQ8RfWDFbAo6kYYUBD/QPM/tboYnzqFQBsQaxCguiC+701j9EmmP60bEm3+k7Dw3L2hErEdIUsHTTqdX4LKccUeSyzKnS0zrDae9W0ir/5ojJbBAuv+uMXa5tesfWyUcvEwTFjk+OpozjIzOZzOYDs2mF7+V+T+Kvl3UqqwVrojiu3MsshJPJi5sTx1vZ+yt5x4M1Kse5SE59edOkH5pQtz2aN4trWcwuWX1nuCE/yrAApJW1fzAKxYw6yxLBb/GLaZWE7xDjWeqLPDt1hGhpdK+jixu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL78iIUPp9/kO/1jeAywDf8OVEIVo1labBJZ4h2KY8lpsVsUvdAi/7gFj6gLGSe0k+5+Sl6eTqbq/7qpKcLYN4lx3yPrwrmsOlAOQ4NgYOX3Kc+eS5zLDt/Un5QLJQjvIolKnZrIrWK8Yapq6nHQBVyJoj5g27Dze80dQUh3cHLEhddBKdk4fpI03OIOz/DfqnmFSsiy1ryO7IPr3lHJrCMmTDnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tNzCXVcFNFme7snOOZ1F144EQ2/KBqKeePfKu1KH7/MHLu+XIYQcszb0Lb4r/aiqxWQig1ITeaSiwbMSc2r9H/J8IkzfYHz2g95HH31ZkBA5SbnEjFqYXDhPL1azQa8m+nlvJoahF4rFWsaNgaKMxjuTGodXIG5cXAPfWUz0fpmJDq9fIBmZJdVsx3ldDeD4Ft0RkCq2vQq/8IJJa+rZ/ipB68Dm3dlx6v3P0xUo9Hp6FZbFij3ffyRPhmoNAgQO8uVnu0UtmFOZ0O52ma4ATI0B17ZySg4/cKXk4al/AtH2VBjGe4fbTEynBNu8U2g8

> 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