Hi,guys
I am working with HOL4.
I am going to prove
g`!p q. (LENGTH p = LENGTH q)
==> !l m n .
TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `;
Where the definition of CX is
val CX_def = Define`
(CX [] p q = p) ??
(CX (x::xs) p q =
TAKE x (CX xs p q) ++
DROP x (CX xs q p))`;
Inorder to use TAKE_APPEND1, TAKE_APPEND2, DROP_APPEND1 and
DROP_APPEND2. I need to add the nesessary assumptions. After some steps, I got
> val it =
TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q))
------------------------------------
0. p IN d
1. q IN d
2. LENGTH p = LENGTH q
3. LENGTH (CX l p q) = LENGTH p
4. LENGTH (CX l q p) = LENGTH q
5. LENGTH (CX l p q) = LENGTH (CX l q p)
6. m <= LENGTH p
7. n <= LENGTH p
8. m <= n
9. m <= LENGTH (TAKE n (CX l p q))
It had been proved that (!p m n . (m<=n) ==> ((LENGTH (TAKE m p)) <= n)),
named "TAKE_LENGTH_NLESS1". So, I printed
e(`(LENGTH (TAKE m (CX l p q)) <= n)` by PROVE_TAC [TAKE_LENGTH_NLESS1]);
But it failed. The strange thing is that, "9. m <= LENGTH (TAKE n (CX l p
q))" was added through
e(`m <= (LENGTH (TAKE n (CX l p q)))` by PROVE_TAC [TAKE_LENGTH_LESS]);
Where TAKE_LENGTH_LESS is (!p m n . ((m<=LENGTH p) /\ (m<=n)) ==>
(m<=(LENGTH (TAKE n p)))).
Why can't it work in the same way?Does anyone know the reason?
Thanks!------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785231&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
