As Thomas said, the key is rewriting (or simplification). I suggested to use fs, not STRIP_ASSUME_TAC.
On 16 December 2015 at 01:14, 康漫 <[email protected]> wrote: > Thank everyone! > This problem has been resolved. I added following steps: > > e (ASM_REWRITE_TAC [*TAKE_0*]) ; > e (ONCE_ASM_REWRITE_TAC [boolTheory.EQ_SYM_EQ]) ; > e (PROVE_TAC[listTheory.LENGTH_NIL]); > Thanks! > > ------------------ Original ------------------ > *From: * "hol-info-request";<[email protected]>; > *Date: * Tue, Dec 15, 2015 08:48 PM > *To: * "hol-info"<[email protected]>; > *Subject: * hol-info Digest, Vol 115, Issue 7 > > Send hol-info mailing list submissions to > [email protected] > > 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 > [email protected] > > You can reach the person managing the list at > [email protected] > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of hol-info digest..." > > > Today's Topics: > > 1. Re: [SPAM] some questions about the proving process in HOL4 > (Jeremy Dawson) > 2. [SPAM] Re: some questions about the proving process in HOL4 ( ?? ) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 15 Dec 2015 14:54:48 +1100 > From: Jeremy Dawson <[email protected]> > Subject: Re: [Hol-info] [SPAM] some questions about the proving > process in HOL4 > To: <[email protected]> > Message-ID: <[email protected]> > Content-Type: text/plain; charset="windows-1252"; format=flowed > > Hi Ada, > > You need to search for suitable theorems. > > In this case > > > apropos ``TAKE 0`` ; > <<HOL message: inventing new type variable names: 'a>> > val it = > [(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)), > > so from the initial goal > > e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); > > e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ; > > This should work but doesn't - when all else fails, look at the types: > show_types := true ; > and you see that they are different. > Do it this way instead. > > e (ASM_REWRITE_TAC [listTheory.TAKE_0, listTheory.LENGTH_EQ_NUM_compute]) ; > > then you're almost there. > > If you didn't have the theorem TAKE_0 you would have to use the > definition of TAKE, namely listTheory.TAKE_def, and use > Cases_on `p` > > Cheers, > > Jeremy > > > > On 15/12/15 14:27, Ada wrote: > > Hey guys, > > > > I am learning to use HOL4. There is a function named "TAKE" in HOL4, > > which can get the first n elements in a list. > > When I was proving one property of TAKE, I find an interesting thing. As > > follows: > > - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `; > > - e (REPEAT STRIP_TAC); > > OK.. > > 1 subgoal: > >> val it = > > TAKE 0 p = p > > ------------------------------------ > > LENGTH p = 0 > > : proof > > - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); > > OK.. > > 1 subgoal: > > > val it = > > TAKE 0 p = p > > ------------------------------------ > > 0. LENGTH p = 0 > > 1. !l. (LENGTH l = 0) <=> (l = []) > > 2. !l n. > > (LENGTH l = NUMERAL (BIT1 n)) <=> > > ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l') > > 3. !l n. > > (LENGTH l = NUMERAL (BIT2 n)) <=> > > ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l') > > 4. !l n1 n2. > > (LENGTH l = n1 + n2) <=> > > ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ > l2) > > : proof > > The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])" > > have already been in assumption list, so I think it is natural to get > > "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove > > that. Could anyone prove it? > > Thanks! --Wish. > > > > > > > ------------------------------------------------------------------------------ > > > > > > > > _______________________________________________ > > hol-info mailing list > > [email protected] > > https://lists.sourceforge.net/lists/listinfo/hol-info > > > > > > ------------------------------ > > Message: 2 > Date: Tue, 15 Dec 2015 20:48:18 +0800 > From: " ?? " <[email protected]> > Subject: [Hol-info] [SPAM] Re: some questions about the proving > process in HOL4 > To: " hol-info " <[email protected]> > Message-ID: <[email protected]> > Content-Type: text/plain; charset="gb18030" > > > Hi,Ramana,Thanks for your reply! > after I used listTheory.LENGTH_NIL, I get that: > - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL); > OK.. > 1 subgoal: > > val it = > first 0 p = p > ------------------------------------ > 0. LENGTH p = 0 > 1. !l. (LENGTH l = 0) <=> (l = []) > : proof > Then Which tactic could be used to prove the goal? I tried many times > , but it failed. > Thanks! -Wish > > > > > ------------------------------ > > Message: 3 > Date: Tue, 15 Dec 2015 11:27:35 +0800 > From: " Ada " <[email protected]> > Subject: [Hol-info] [SPAM] some questions about the proving process in > HOL4 > To: " hol-info " <[email protected]> > Message-ID: <[email protected]> > Content-Type: text/plain; charset="iso-8859-1" > > Hey guys, > > I am learning to use HOL4. There is a function named "TAKE" in HOL4, > which can get the first n elements in a list. > When I was proving one property of TAKE, I find an interesting thing. As > follows: > - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `; > - e (REPEAT STRIP_TAC); > OK.. > 1 subgoal: > > val it = > TAKE 0 p = p > ------------------------------------ > LENGTH p = 0 > : proof > - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); > OK.. > 1 subgoal: > > val it = > TAKE 0 p = p > ------------------------------------ > 0. LENGTH p = 0 > 1. !l. (LENGTH l = 0) <=> (l = []) > 2. !l n. > (LENGTH l = NUMERAL (BIT1 n)) <=> > ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l') > 3. !l n. > (LENGTH l = NUMERAL (BIT2 n)) <=> > ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l') > 4. !l n1 n2. > (LENGTH l = n1 + n2) <=> > ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2) > : proof > The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])" > have already been in assumption list, so I think it is natural to get > "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove that. > Could anyone prove it? > > Thanks! --Wish. > -------------- next part -------------- > An HTML attachment was scrubbed... > > ------------------------------ > > Message: 4 > Date: Tue, 15 Dec 2015 14:34:44 +1100 > From: Ramana Kumar <[email protected]> > Subject: Re: [Hol-info] [SPAM] some questions about the proving > process in HOL4 > To: Ada <[email protected]> > Cc: hol-info <[email protected]> > Message-ID: > <CAMej=26SaPqq_x7cFoiHfSQVvuUks9GXazvn0=x0yvjzpv2...@mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > fs[LENGTH_NIL,TAKE_def] > > On 15 December 2015 at 14:27, Ada <[email protected]> wrote: > > > Hey guys, > > > > I am learning to use HOL4. There is a function named "TAKE" in HOL4, > > which can get the first n elements in a list. > > When I was proving one property of TAKE, I find an interesting thing. As > > follows: > > - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `; > > - e (REPEAT STRIP_TAC); > > OK.. > > 1 subgoal: > > > val it = > > TAKE 0 p = p > > ------------------------------------ > > LENGTH p = 0 > > : proof > > - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); > > OK.. > > 1 subgoal: > > > val it = > > TAKE 0 p = p > > ------------------------------------ > > 0. LENGTH p = 0 > > 1. !l. (LENGTH l = 0) <=> (l = []) > > 2. !l n. > > (LENGTH l = NUMERAL (BIT1 n)) <=> > > ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l') > > 3. !l n. > > (LENGTH l = NUMERAL (BIT2 n)) <=> > > ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l') > > 4. !l n1 n2. > > (LENGTH l = n1 + n2) <=> > > ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ > l2) > > : proof > > The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])" > > have already been in assumption list, so I think it is natural to get > > "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove > that. > > Could anyone prove it? > > > > Thanks! --Wish. > > > > > > > ------------------------------------------------------------------------------ > > > > _______________________________________________ > > hol-info mailing list > > [email protected] > > https://lists.sourceforge.net/lists/listinfo/hol-info > > > > > -------------- next part -------------- > An HTML attachment was scrubbed... > > ------------------------------ > > > ------------------------------------------------------------------------------ > > > ------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > > End of hol-info Digest, Vol 115, Issue 6 > **************************************** > -------------- next part -------------- > An HTML attachment was scrubbed... > > ------------------------------ > > > ------------------------------------------------------------------------------ > > > ------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > > End of hol-info Digest, Vol 115, Issue 7 > **************************************** > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
