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
