fs[LENGTH_NIL,TAKE_def] On 15 December 2015 at 14:27, Ada <[email protected]> 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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
