Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Great! sure, I’ll do that! —Chun

> Il giorno 05 ott 2017, alle ore 23:16, Ramana Kumar 
>  ha scritto:
> 
> I think it would be good to add this UNIQUE constant to listTheory, if you 
> have time to make a pull request.
> 
> On 6 October 2017 at 01:49, Chun Tian (binghe)  wrote:
> Let me close this question (further comments are welcome, of course).
> 
> I actually got another good definition from Robert Beers in a private email:
> 
>[UNIQUE_DEF]  Definition
> 
>   |- ∀x L.
>UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2
> 
> This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is exactly 
> what I needed from the uniqueness. Then I tried to prove the following two 
> alternative definitions using above definition, with success:
> 
>[UNIQUE_ALT]  Theorem
> 
>   |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])
> 
>[UNIQUE_ALT_COUNT]  Theorem
> 
>   |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)
> 
> where LIST_ELEM_COUNT is a constant defined in rich_listTheory:
> 
> [LIST_ELEM_COUNT_DEF]  Definition
> 
>   |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
> 
> From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other direction 
> is more difficult. I attached my proof scripts in case anyone needs it. But 
> I’m new to listTheory, my scripts are very ugly, sorry for that (they will 
> become better once I’ve learnt more).
> 
> Regards,
> 
> Chun Tian
> 
> 
> 
> > Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) 
> >  ha scritto:
> >
> > Hi,
> >
> > (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> > possibly duplicated elements, and I want to express certain element X is 
> > unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> > "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> >
> > Regards,
> >
> > Chun Tian
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
> 
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Ramana Kumar]

I think it would be good to add this UNIQUE constant to listTheory, if you
have time to make a pull request.

On 6 October 2017 at 01:49, Chun Tian (binghe) 
wrote:

> Let me close this question (further comments are welcome, of course).
>
> I actually got another good definition from Robert Beers in a private
> email:
>
>[UNIQUE_DEF]  Definition
>
>   |- ∀x L.
>UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2
>
> This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is
> exactly what I needed from the uniqueness. Then I tried to prove the
> following two alternative definitions using above definition, with success:
>
>[UNIQUE_ALT]  Theorem
>
>   |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])
>
>[UNIQUE_ALT_COUNT]  Theorem
>
>   |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)
>
> where LIST_ELEM_COUNT is a constant defined in rich_listTheory:
>
> [LIST_ELEM_COUNT_DEF]  Definition
>
>   |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
>
> From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other
> direction is more difficult. I attached my proof scripts in case anyone
> needs it. But I’m new to listTheory, my scripts are very ugly, sorry for
> that (they will become better once I’ve learnt more).
>
> Regards,
>
> Chun Tian
>
>
>
> > Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > (I'm new to HOL's listTheory). Suppose I have a list L which contains
> possibly duplicated elements, and I want to express certain element X is
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> >
> > Regards,
> >
> > Chun Tian
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Let me close this question (further comments are welcome, of course).

I actually got another good definition from Robert Beers in a private email:

   [UNIQUE_DEF]  Definition

  |- ∀x L.
   UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2

This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is exactly 
what I needed from the uniqueness. Then I tried to prove the following two 
alternative definitions using above definition, with success:

   [UNIQUE_ALT]  Theorem

  |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])

   [UNIQUE_ALT_COUNT]  Theorem

  |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)

where LIST_ELEM_COUNT is a constant defined in rich_listTheory:

[LIST_ELEM_COUNT_DEF]  Definition

  |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)

From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other direction 
is more difficult. I attached my proof scripts in case anyone needs it. But I’m 
new to listTheory, my scripts are very ugly, sorry for that (they will become 
better once I’ve learnt more).

Regards,

Chun Tian



extra_listScript.sml
Description: application/smil

> Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> possibly duplicated elements, and I want to express certain element X is 
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> 
> Regards,
> 
> Chun Tian
> 
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

OK, thanks everyone!  So FILTER is what I must use.

I think I’m going to use ``(FILTER (\e. e = X) L = [X])`` to assert the unique 
appearance of X in list L, and after I split the list using MEM_SPLIT, my 
target props (~MEM X l1) could be re-expressed by EVERY and FILTER, then it may 
be provable for me.

—Chun

> Il giorno 05 ott 2017, alle ore 17:03, Scott Owens  ha 
> scritto:
> 
> Among others, LENGTH (FILTER (\e. X = e)) = 1
> 
> Scott
> 
>> On 2017/10/05, at 15:55, Chun Tian (binghe)  wrote:
>> 
>> But my list is not ALL_DISTINCT … there’re duplicated elements for sure, 
>> just the appearance of certain element is only one. —Chun
>> 
>>> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind 
>>>  ha scritto:
>>> 
>>> Hi Chun Tian,
>>> 
>>> The constant ALL_DISTINCT in listTheory is what you are looking for, I 
>>> think.
>>> 
>>> Konrad.
>>> 
>>> 
>>> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe)  
>>> wrote:
>>> Hi,
>>> 
>>> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
>>> possibly duplicated elements, and I want to express certain element X is 
>>> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
>>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>>> 
>>> Regards,
>>> 
>>> Chun Tian
>>> 
>>> --
>>> Chun Tian (binghe)
>>> University of Bologna (Italy)
>>> 
>>> 
>>> --
>>> Check out the vibrant tech community on one of the world's most
>>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>>> ___
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> 
>>> 
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! 
>> http://sdm.link/slashdot___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Scott Owens]

Among others, LENGTH (FILTER (\e. X = e)) = 1

Scott

> On 2017/10/05, at 15:55, Chun Tian (binghe)  wrote:
> 
> But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just 
> the appearance of certain element is only one. —Chun
> 
>> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind  
>> ha scritto:
>> 
>> Hi Chun Tian,
>> 
>>  The constant ALL_DISTINCT in listTheory is what you are looking for, I 
>> think.
>> 
>> Konrad.
>> 
>> 
>> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe)  
>> wrote:
>> Hi,
>> 
>> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
>> possibly duplicated elements, and I want to express certain element X is 
>> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>> 
>> Regards,
>> 
>> Chun Tian
>> 
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>> 
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> 
>> 
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! 
> http://sdm.link/slashdot___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just 
the appearance of certain element is only one. —Chun

> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind  
> ha scritto:
> 
> Hi Chun Tian,
> 
>   The constant ALL_DISTINCT in listTheory is what you are looking for, I 
> think.
> 
> Konrad.
> 
> 
> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe)  
> wrote:
> Hi,
> 
> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> possibly duplicated elements, and I want to express certain element X is 
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> 
> Regards,
> 
> Chun Tian
> 
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
> 
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Hi Anthony,

Thanks. This definition may work (at least I can see it’s correct), at least 
that’s what I can start with. But in my proof the next move will be using 
MEM_SPLIT to divide the list into three pieces:

[MEM_SPLIT]  Theorem

  |- ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ⧺ x::l2

and what I finally need are ``~MEM X l1`` and ``~MEM X l2``. But from FILTER 
and LENGTH how can I reach my targets? A little hints may help me a lot …

Regards,

Chun

> Il giorno 05 ott 2017, alle ore 16:21, Anthony Fox  ha 
> scritto:
> 
> Perhaps something like
> 
> val unique_def = Define`unique x l = LENGTH (FILTER ($= x) l) = 1`
> 
> is what you’re after?
> 
> Anthony
> 
>> On 5 Oct 2017, at 15:03, Chun Tian (binghe)  wrote:
>> 
>> Hi,
>> 
>> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
>> possibly duplicated elements, and I want to express certain element X is 
>> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>> 
>> Regards,
>> 
>> Chun Tian
>> 
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! 
>> http://sdm.link/slashdot___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Konrad Slind]

Hi Chun Tian,

  The constant ALL_DISTINCT in listTheory is what you are looking for, I
think.

Konrad.


On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) 
wrote:

> Hi,
>
> (I'm new to HOL's listTheory). Suppose I have a list L which contains
> possibly duplicated elements, and I want to express certain element X is
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>
> Regards,
>
> Chun Tian
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Hi,

(I'm new to HOL's listTheory). Suppose I have a list L which contains
possibly duplicated elements, and I want to express certain element X is
unique (i.e. has only one copy) in that list.  How can I do this?  It seems
"?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.

Regards,

Chun Tian

-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info