Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

2015-12-14 Thread Jeremy Dawson 
Hi Ada,

You need to search for suitable theorems.

In this case

 > apropos ``TAKE 0`` ;
<>
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
>

--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

2015-12-14 Thread Ramana Kumar 
fs[LENGTH_NIL,TAKE_def]

On 15 December 2015 at 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
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info