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> 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>; > Date: Mon, Feb 29, 2016 01:08 PM > To: "hol-info"<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 > > 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 > > You can reach the person managing the list at > 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> > Subject: [Hol-info] How to transform list format from "(cx l q p)" to > "l" > To: " hol-info " <hol-info@lists.sourceforge.net> > Message-ID: <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> > Subject: Re: [Hol-info] How to transform list format from "(cx l q p)" > to "l" > To: <hol-info@lists.sourceforge.net> > Message-ID: <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 > > https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ 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 https://lists.sourceforge.net/lists/listinfo/hol-info
