It is true that LENGTH_TAKE_EQ is not in Kananaskis-10 (it appeared in the
repository on 14 August 2015).
You could add it to your development manually: its conclusion is
LENGTH (TAKE n xs) = if n <= LENGTH xs then n else LENGTH xs
Michael
On 2 Mar 2016, at 13:18, 康漫 <956066...@qq.com<mailto:956066...@qq.com>> wrote:
Thank you for your reply!
My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 14:27:30
2014)], where Moscow ML version 2.01 (January 2004). Then from
https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and pointed
""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon Feb 29
21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ, it
responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had downloaded
the files in https://github.com/HOL-Theorem-Prover/HOL. How to add it to HOL4's
directory? After that ,I could print "open listTheory;" in HOL4, and use
LENGTH_TAKE_EQ.
Thanks.
------------------ Original ------------------
From:
"hol-info-request";<hol-info-requ...@lists.sourceforge.net<mailto:hol-info-requ...@lists.sourceforge.net>>;
Date: Wed, Mar 2, 2016 06:31 AM
To:
"hol-info"<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>;
Subject: hol-info Digest, Vol 118, Issue 1
Send hol-info mailing list submissions to
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.sourceforge.net/lists/listinfo/hol-info
or, via email, send a message with subject or body 'help' to
hol-info-requ...@lists.sourceforge.net<mailto:hol-info-requ...@lists.sourceforge.net>
You can reach the person managing the list at
hol-info-ow...@lists.sourceforge.net<mailto:hol-info-ow...@lists.sourceforge.net>
When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."
Today's Topics:
1. Re: How to transform list format from "(cx l q p)" to "l"
(Anthony Fox)
2. Re: Existential quantifier length (Michael Norrish)
3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
Croatia (Veelasha)
----------------------------------------------------------------------
Message: 1
Date: Mon, 29 Feb 2016 10:25:51 +0000
From: Anthony Fox <ac...@cam.ac.uk<mailto:ac...@cam.ac.uk>>
Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
to "l"
To: ?? <956066...@qq.com<mailto:956066...@qq.com>>
Cc: hol-info
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Message-ID:
<6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk<mailto:6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>>
Content-Type: text/plain; charset=utf-8
Which version of HOL4 are you using? The definitions of TAKE and DROP were
altered in Jan 2008 (around about the time of kananaskis-5).
With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for me.
The proof seems to be trivial. (I?ve not tried it with older versions of HOL4.)
How exactly did you define ?cx??
With
val cx_def = Define`
(cx [] p q = p) /\
(cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`
we have
val th = Q.prove(
`!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])
To get something closer to your definition of ?cx? I did
val cx_def = tDefine "cx" `
(cx [] p q = p) /\
(cx (h :: t) p q =
TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
(WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])
but the proof worked without modification.
Regards,
Anthony
> On 29 Feb 2016, at 07:38, ?? <956066...@qq.com<mailto:956066...@qq.com>>
> wrote:
>
> Hi,Jeremy
> Thank you for your reply!
> I tried. But it can't work.
> It responsed:
> - e (RW_TAC list_ss [LENGRH_DROP]);
> OK..
> Exception raised at Tactical.VALID:
> Invalid tactic
> ! Uncaught exception:
> ! HOL_ERR
> I think the reason is that the format of "(cx l q p)" is not equal to "l",
> though they are the same type "bool list".
> Thank you!
>
> ------------------ Original ------------------
> From:
> "hol-info-request";<hol-info-requ...@lists.sourceforge.net<mailto:hol-info-requ...@lists.sourceforge.net>>;
> Date: Mon, Feb 29, 2016 01:08 PM
> To:
> "hol-info"<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>;
> Subject: hol-info Digest, Vol 117, Issue 9
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net<mailto:hol-info-requ...@lists.sourceforge.net>
>
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net<mailto:hol-info-ow...@lists.sourceforge.net>
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
>
>
> Today's Topics:
>
> 1. How to transform list format from "(cx l q p)" to "l" ( Ada )
> 2. Re: How to transform list format from "(cx l q p)" to "l"
> (Jeremy Dawson)
> 3. Two postdoc positions - Reasoning about concurrency and
> distribution - Imperial College London (Petar Maksimovic)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sun, 28 Feb 2016 19:48:56 +0800
> From: " Ada " <ada.k...@qq.com<mailto:ada.k...@qq.com>>
> Subject: [Hol-info] How to transform list format from "(cx l q p)" to
> "l"
> To: " hol-info "
> <hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
> Message-ID:
> <tencent_6526cfdf05ecaae746588...@qq.com<mailto:tencent_6526cfdf05ecaae746588...@qq.com>>
> Content-Type: text/plain; charset="gb18030"
>
> Hey,guys
>
> I am learning to use HOL4. Here are some questions about my proving:
>
>
>
> g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) =
> LENGTH p) `;
>
> e (Induct_on `l`);
>
> e (RW_TAC list_ss [cx_defn]);
>
> - e (RW_TAC list_ss [cx_defn]);
>
> OK..
>
> 1 subgoal:
>
> > val it =
>
>
>
> LENGTH (DROP h (cx l q p)) +
>
> LENGTH (TAKE h (cx l p q)) =
>
> LENGTH q
>
> ------------------------------------
>
> 0. !p q.
>
> (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
>
> 1. LENGTH p = LENGTH q
>
> : proof
>
>
>
> The definition of ?cx? is following:
>
>
>
> |- (!q p. cx [] p q = p) /\
>
> !v5 v4 q p.
>
> cx (v4::v5) p q =
>
> TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
>
> DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
>
>
>
> Where, ?TAKE? is in listtheory in HOL4. It means that get firs n elements,
> ?DROP? is in listtheory in HOL4. It means that get after n elements,
>
>
>
> I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==> (LENGTH
> (DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named ?TAKE_DROP_LENGTH?.
>
>
>
> But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH p =
> LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the problem is
> that in the goal the form is ?DROP h (cx l q p)?, but the actual form is
> ?DROP h l?, where the format of ?(cx l q p)? is not equal to ?l?. But I can?t
> find a good transform between them.
>
>
>
> Could anyone give me some advices?
>
> Thank you!
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
> Message: 2
> Date: Mon, 29 Feb 2016 00:49:29 +1100
> From: Jeremy Dawson
> <jeremy.daw...@anu.edu.au<mailto:jeremy.daw...@anu.edu.au>>
> Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> to "l"
> To: <hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
> Message-ID: <56d2fae9.2080...@anu.edu.au<mailto:56d2fae9.2080...@anu.edu.au>>
> Content-Type: text/plain; charset="windows-1252"; format=flowed
>
>
> It might be easier to avoid using TAKE_DROP_LENGTH
> but instead try to simplify your subgoal using
> LENGTH_TAKE_EQ and LENGTH_DROP
>
> Then I think you'll have to instantiate your subgoal 0 once with p,q
> and once with q,p
>
> Cheers,
>
> Jeremy
>
> On 28/02/16 22:48, Ada wrote:
> > Hey,guys
> >
> > I am learning to use HOL4. Here are some questions about my proving:
> >
> > g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p
> > q) = LENGTH p) `;
> >
> > e (Induct_on `l`);
> >
> > e (RW_TAC list_ss [cx_defn]);
> >
> > - e (RW_TAC list_ss [cx_defn]);
> >
> > OK..
> >
> > 1 subgoal:
> >
> >> val it =
> >
> > LENGTH (DROP h (cx l q p)) +
> >
> > LENGTH (TAKE h (cx l p q)) =
> >
> > LENGTH q
> >
> > ------------------------------------
> >
> > 0.!p q.
> >
> > (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
> >
> > 1.LENGTH p = LENGTH q
> >
> > : proof
> >
> > The definition of ?cx? is following:
> >
> > |- (!q p. cx [] p q = p) /\
> >
> > !v5 v4 q p.
> >
> > cx (v4::v5) p q =
> >
> > TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
> >
> > DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
> >
> > Where,?TAKE? is in listtheory in HOL4. It means that get firs n
> > elements,?DROP? is in listtheory in HOL4. It means that get after n
> > elements,
> >
> > I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==>
> > (LENGTH (DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named
> > ?TAKE_DROP_LENGTH?.
> >
> > But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH
> > p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the
> > problem is that in the goal the form is ?DROP h (cx l q p)?, but the
> > actual form is ?DROP h l?, where the format of ?(cx l q p)? is not equal
> > to ?l?. But I can?t find a good transform between them.
> >
> > Could anyone give me some advices?
> >
> > Thank you!
> >
> >
> >
> > ------------------------------------------------------------------------------
> > Site24x7 APM Insight: Get Deep Visibility into Application Performance
> > APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> > Monitor end-to-end web transactions and take corrective actions now
> > Troubleshoot faster and improve end-user experience. Signup Now!
> > http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> >
> >
> >
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
------------------------------
Message: 2
Date: Mon, 29 Feb 2016 23:30:30 +0000
From: Michael Norrish
<michael.norr...@nicta.com.au<mailto:michael.norr...@nicta.com.au>>
Subject: Re: [Hol-info] Existential quantifier length
To: hol-info
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Message-ID:
<e632870e-78db-4885-bbe8-282d2d6a1...@nicta.com.au<mailto:e632870e-78db-4885-bbe8-282d2d6a1...@nicta.com.au>>
Content-Type: text/plain; charset="us-ascii"
I agree: your theorem is hard to prove because you don't have enough
information about FA etc. Can you prove that
mux_list_imp a b sel y ==> (LENGTH y = something)
If you can't, why not adjust mux_list_imp's definition so that you can?
Similarly, it would seem reasonable to have the same property be true of the
_spec version.
Michael
On 25 Feb 2016, at 20:53, Sumayya Shiraz
<sumayya.shi...@seecs.edu.pk<mailto:sumayya.shi...@seecs.edu.pk><mailto:sumayya.shi...@seecs.edu.pk>>
wrote:
Dear all
Is it possible to specify length of bool list of the existential quantifier.
I have following proof
(?FA FB FC.
mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 a) + 1))) a F
FA /\
mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 b) + 1))) b F
FB /\
mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 c) + 1))) c F
FC /\
Adder_imp_n (LENGTH y + LENGTH y)
(num_BV_f (LENGTH FA + LENGTH FB) (BV_n FA * BV_n FB))
(make_list_F (LENGTH y) ++ FC) F y co) <=>
(co :: y =
(num_BV_f (SUC (LENGTH y + LENGTH y)) (BV_n a * BV_n b + BV_n c)))
------------------------------------
0. LENGTH a = LENGTH y
1. LENGTH b = LENGTH y
2. LENGTH c = LENGTH y
3. !n a.
num_BV_f (SUC n) a =
HD (num_BV_f (SUC n) a)::TL (num_BV_f (SUC n) a)
: proof
In above code, i want to apply the verified theorem
mux_list_thm;
> val it =
|- !a b sel y.
(LENGTH b = LENGTH a) /\ (LENGTH y = LENGTH a) ==>
(mux_list_imp a b sel y <=> mux_list_spec a b sel y) : thm
Now the problem is that i dont know length of FA. FB and FC in the above goal
to apply the mux_lixt_thm.
How can i find or describe its length and apply the above theorem to simplify
my goal
kindly reply me soon.
thanks a lot
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
-------------- next part --------------
An HTML attachment was scrubbed...
------------------------------
Message: 3
Date: Tue, 1 Mar 2016 14:51:01 +0100
From: Veelasha <veelasha2...@gmail.com<mailto:veelasha2...@gmail.com>>
Subject: [Hol-info] ? Summer School on Real-World Crypto and Privacy,
June 5-10, Croatia
To: undisclosed-recipients:;
Message-ID:
<CAPYFFjpOzZEVPqvDLzKfiR=z0Kv=Hrn9Tua9v3=_nemeghl...@mail.gmail.com<mailto:CAPYFFjpOzZEVPqvDLzKfiR=z0Kv=Hrn9Tua9v3=_nemeghl...@mail.gmail.com>>
Content-Type: text/plain; charset="utf-8"
[Apologies to those who receive multiple copies of this announcement]
****************************************************************************
? ?
? ?
Call for Participation
??
Summer School on Real-World Crypto and Privacy
? ?
June 5-10, 2016, Sibenik (Croatia)
http://summerschool-croatia.cs.ru.nl/2016/
****************************************************************************
After the big success of the Summer School on Real-World Crypto and
Privacy in 2015, we are planning the next edition for June 5-10, 2016 in
Sibenik, Croatia.
The purpose of the School is to attract not only Ph.D. students and
postdocs, but also people from industry who are interested in recent
developments in cryptography. The program will start with 2 days of
plenary talks followed by an excursion to the Kornati National Park on
June 8. The last 2 days will include more advanced talks on recent
topics organized in two parallel sessions.
List of confirmed invited speakers:
- Lejla Batina, Radboud University, The Netherlands and KU Leuven, Belgium
- Gilles Barthe, IMDEA Software Institute, Spain
- David Basin, ETH Zurich, Switzerland
- Daniel J. Bernstein, Technische Universiteit Eindhoven, The
Netherlands and University of Illinois at Chicago, USA
- Joppe Bos, NXP Semiconductors, Belgium
- Srdjan Capkun, ETH Zurich, Switzerland
- Joan Daemen, STMicroelectronics and Radboud University
- Claudia Diaz, KU Leuven, Belgium
- Roger Dingledine, The Tor Project, USA
- Rachel Greenstadt, Drexel University, USA
- J. Alex Halderman, University of Michigan, USA
- Nadia Heninger, University of Pennsylvania, USA
- Ari Juels, Cornell University, USA
- Tanja Lange, Technische Universiteit Eindhoven, The Netherlands
- Nele Mentens, KU Leuven, Belgium
- Guevara Noubir, Northeastern University, USA
- Kenny Paterson, RHUL, UK
- Adrian Perrig, ETH Zurich, Switzerland
- Bart Preneel, KU Leuven, Belgium
- Phillip Rogaway, University of California, Davis, USA
- Peter Schwabe, Radboud University, The Netherlands
- Benjamin Smith, INRIA and ?cole Polytechnique, France
- Martijn Stam, University of Bristol, UK
- Fran?ois-Xavier Standaert, Universit? catholique de Louvain, Belgium
- Carmela Troncoso, IMDEA Software Institute, Spain
- Ingrid Verbauwhede, KU Leuven, Belgium
Early registration is open until May 01.
Stipends for students are also available.
For more information, see http://summerschool-croatia.cs.ru.nl/2016/
-------------- next part --------------
An HTML attachment was scrubbed...
------------------------------
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
End of hol-info Digest, Vol 118, Issue 1
****************************************
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://makebettercode.com/inteldaal-eval
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
