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";<hol-info-requ...@lists.sourceforge.net>;
Date: Tue, Dec 15, 2015 08:48 PM
To: "hol-info"<hol-info@lists.sourceforge.net>;
Subject: hol-info Digest, Vol 115, Issue 7
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. 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 <jeremy.daw...@anu.edu.au>
Subject: Re: [Hol-info] [SPAM] some questions about the proving
process in HOL4
To: <hol-info@lists.sourceforge.net>
Message-ID: <566f8f08.9050...@anu.edu.au>
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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------
Message: 2
Date: Tue, 15 Dec 2015 20:48:18 +0800
From: " ?? " <956066...@qq.com>
Subject: [Hol-info] [SPAM] Re: some questions about the proving
process in HOL4
To: " hol-info " <hol-info@lists.sourceforge.net>
Message-ID: <tencent_7de4e1d26609f7a50013c...@qq.com>
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 " <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
****************************************
-------------- 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 7
****************************************------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
