Hi Ada, there are many ways to do it. But essentially what you want is rewriting.
Bird's eye view: You want to prove ``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)`` STEP 1 : You show that "p" is "[]" with theorem LENGTH_NIL. STEP 2 : You use the theorem TAKE_0 to simplify "TAKE 0 p" to "[]" STEP 3 : You combine STEP 1 and STEP 2 There are plenty of ways to do it. Essentially, you want to use LENGTH_NIL and TAKE_0 as rewrites. This can (rather verbosely) be done via e.g. val thm1 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``, REWRITE_TAC[LENGTH_NIL, TAKE_0] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]) However, a simple call to the simplifier is sufficient (it uses the antecedent of the implication automatically and list_ss contains TAKE_0) val thm2 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``, SIMP_TAC list_ss [LENGTH_NIL]) One could also use first order automatic reasoners, but this is a bit much here. val thm3 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``, REPEAT STRIP_TAC THEN `p = []` by PROVE_TAC[LENGTH_NIL] THEN ASM_REWRITE_TAC[TAKE_0]) val thm4 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``, PROVE_TAC [TAKE_0, LENGTH_NIL]) There are plenty more ways for doing it. The core operation is rewriting here. So, perhaps have a look at the rewrite tactics and the simplifier. Best Thomas Tuerk On 15.12.2015 13:48, 康漫 wrote: > 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 " <ada.k...@qq.com> > Subject: [Hol-info] [SPAM] some questions about the proving process in > HOL4 > To: " hol-info " <hol-info@lists.sourceforge.net> > Message-ID: <tencent_7f77ca956510ebe87ffaf...@qq.com> > 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 <ramana.ku...@cl.cam.ac.uk> > Subject: Re: [Hol-info] [SPAM] some questions about the proving > process in HOL4 > To: Ada <ada.k...@qq.com> > Cc: hol-info <hol-info@lists.sourceforge.net> > 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 <ada.k...@qq.com> 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 >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> > -------------- next part -------------- > An HTML attachment was scrubbed... > > ------------------------------ > > ------------------------------------------------------------------------------ > > > ------------------------------ > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > End of hol-info Digest, Vol 115, Issue 6 > **************************************** > > > ------------------------------------------------------------------------------ > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
