As Thomas said, the key is rewriting (or simplification). I suggested to
use fs, not STRIP_ASSUME_TAC.
On 16 December 2015 at 01:14, 康漫 <956066...@qq.com> wrote:
> Thank everyone!
> This problem has been resolved. I added following steps:
>
> e (ASM_REWRITE_TAC [*TAKE_0*]) ;
> e
Hi Ada,
there are many ways to do it. But essentially what you want is rewriting.
Bird's eye view:
You want to prove
``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``
STEP 1 : You show that "p" is "[]" with theorem LENGTH_NIL.
STEP 2 : You use the theorem TAKE_0 to simplify "TAKE 0 p" to "[]"
STEP 3
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
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:
