Uniqueness of list elements (UNIQUE) and 3 alternative definitions

[binghe]

Currently HOL's listTheory lack of the definition for testing the uniqueness of an element in a list. I've learnt several equivalent definitions from the mailing list, one (the most useful form for me) is from Robert Beers robert@beers.org:

   [UNIQUE_DEF]  Definition

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

The most common alternative definitions (suggested by Scott Owens and Anthony Fox) are based on FILTER and LENGTH. Or it can be based on LIST_ELEM_COUNT (in rich_listTheory):

   [UNIQUE_ALT]  Theorem

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

   [UNIQUE_ALT_COUNT]  Theorem

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

   [UNIQUE_ALT_LENGTH]  Theorem

      |- ∀e L. UNIQUE e L ⇔ (LENGTH (FILTER ($= e) L) = 1)

I have put UNIQUE_DEF into listTheory, and 3 alternative definitions (as theorems) into rich_listTheory.

[binghe]

What about changing the names of theorems in this way?

• UNIQUE_ALT -> UNIQUE_FILTER
• UNIQUE_ALT_COUNT -> UNIQUE_LIST_ELEM_COUNT
• UNIQUE_ALT_LENGTH -> UNIQUE_LENGTH_FILTER

[xrchz]

The proposed name changes sound good.

[xrchz]

I think the theorems based on LENGTH and FILTER should be in listTheory, not rich_listTheory.

[xrchz]

#98 is related

[binghe]

I have renamed those 3 theorems.

But I don't know how to move UNIQUE_FILTER and UNIQUE_LENGTH_FILTER to listTheory, because in their proofs I have used some FULL_SIMP_TAC list_ss [], in which list_ss is only defined in rich_listTheory. list_ss is based on listSimps which in turn depends on listTheory. I don't know how to remove these FULL_SIMP_TAC because I don't know which low-level list theorems were actually used ...

[xrchz]

OK I guess they can be moved around later, maybe when we make progress on #98.

[konrad-slind]

You could also try simpLib.track (which uses simpLib.used_rewrites and simpLib.track_rewrites). It doesn't track names, but accumulates the actual instantiated rules used. Example: Initial goal: MAP LENGTH [[1; 2; 3]; [4; 5; 6; 7]] = X : proof

e (simpLib.track (rw_tac list_ss []));

OK.. 1 subgoal: val it = [3; 4] = X : proof

simpLib.used_rewrites;

val it = ref [|- MAP f (h::t) = f h::MAP f t, |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH [] = 0, |- MAP f (h::t) = f h::MAP f t, |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH [] = 0, |- MAP f [] = []]: thm list ref

…

On Fri, Oct 6, 2017 at 8:36 AM, Ramana Kumar ***@***.***> wrote: Merged #470 <#470>. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#470 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABDgDyHjcrtvLyx12nbIqRyasevwX3j8ks5spiz2gaJpZM4Pv0lC> .

[binghe]

Hi Konrad, Thank you so much! I wanted to know how to track simpLib tacticals for long time, just haven’t got chance to ask in the mailing list. With your help now I’m able to remove all those “list_ss” in my previous proofs of the 3 theorems, I’ll create a new PR for moving 2 of them back to listTheory, as suggested by Ramana. Being able to track simpLib, now I’ve learnt more about listTheory (and other HOL theories). Regards, Chun Tian

…

Il giorno 06 ott 2017, alle ore 16:10, Konrad Slind ***@***.***> ha scritto: You could also try simpLib.track (which uses simpLib.used_rewrites and simpLib.track_rewrites). It doesn't track names, but accumulates the actual instantiated rules used. Example: Initial goal: MAP LENGTH [[1; 2; 3]; [4; 5; 6; 7]] = X : proof > e (simpLib.track (rw_tac list_ss [])); OK.. 1 subgoal: val it = [3; 4] = X : proof > simpLib.used_rewrites; val it = ref [|- MAP f (h::t) = f h::MAP f t, |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH [] = 0, |- MAP f (h::t) = f h::MAP f t, |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH (h::t) = SUC (LENGTH t), |- LENGTH [] = 0, |- MAP f [] = []]: thm list ref > On Fri, Oct 6, 2017 at 8:36 AM, Ramana Kumar ***@***.***> wrote: > Merged #470 <#470>. > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#470 (comment)>, or mute > the thread > <https://github.com/notifications/unsubscribe-auth/ABDgDyHjcrtvLyx12nbIqRyasevwX3j8ks5spiz2gaJpZM4Pv0lC> > . > — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[konrad-slind]

I'm glad it helped. I originally created the functionality for students who were trying to learn the simplifier, but it can be useful even for experts. Konrad.

…

On Fri, Oct 6, 2017 at 11:08 AM, Chun Tian ***@***.***> wrote: Hi Konrad, Thank you so much! I wanted to know how to track simpLib tacticals for long time, just haven’t got chance to ask in the mailing list. With your help now I’m able to remove all those “list_ss” in my previous proofs of the 3 theorems, I’ll create a new PR for moving 2 of them back to listTheory, as suggested by Ramana. Being able to track simpLib, now I’ve learnt more about listTheory (and other HOL theories). Regards, Chun Tian > Il giorno 06 ott 2017, alle ore 16:10, Konrad Slind < ***@***.***> ha scritto: > > You could also try simpLib.track (which uses simpLib.used_rewrites and > simpLib.track_rewrites). > It doesn't track names, but accumulates the actual instantiated rules used. > > Example: > > Initial goal: > > MAP LENGTH [[1; 2; 3]; [4; 5; 6; 7]] = X > : proof > > > e (simpLib.track (rw_tac list_ss [])); > OK.. > 1 subgoal: > val it = > > [3; 4] = X > > : proof > > > simpLib.used_rewrites; > val it = > ref > [|- MAP f (h::t) = f h::MAP f t, > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH [] = 0, > |- MAP f (h::t) = f h::MAP f t, > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH (h::t) = SUC (LENGTH t), > |- LENGTH [] = 0, > |- MAP f [] = []]: > thm list ref > > > > > On Fri, Oct 6, 2017 at 8:36 AM, Ramana Kumar ***@***.***> > wrote: > > > Merged #470 <#470>. > > > > — > > You are receiving this because you are subscribed to this thread. > > Reply to this email directly, view it on GitHub > > <#470 (comment)>, or mute > > the thread > > <https://github.com/notifications/unsubscribe-auth/ ABDgDyHjcrtvLyx12nbIqRyasevwX3j8ks5spiz2gaJpZM4Pv0lC> > > . > > > — > You are receiving this because you authored the thread. > Reply to this email directly, view it on GitHub, or mute the thread. > — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#470 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABDgDzk33yNY4kgOGMTw8hQM4C8dSlGsks5splB5gaJpZM4Pv0lC> .