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
