I was able to prove it as follows, but I needed to prove another lemma
about TAKE which really should be in listTheory.
open HolKernel boolLib bossLib Parse
listTheory rich_listTheory arithmeticTheory
val _ = new_theory"ada"
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))`;
val CX_length = Q.store_thm("CX_length",
`!l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) = LENGTH p)`,
Induct \\ rw[CX_def,LENGTH_TAKE_EQ]);
(* TODO: this should be moved to listTheory *)
val TAKE_TAKE_EQ = Q.store_thm("TAKE_TAKE_EQ",
`TAKE n (TAKE m l) = TAKE (MIN n m) l`,
Cases_on`m < LENGTH l`
\\ rw[TAKE_LENGTH_TOO_LONG,MIN_DEF,TAKE_TAKE]);
(* -- *)
val ada_thm = Q.store_thm("ada_thm",
`!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)) `,
rw[TAKE_APPEND,DROP_APPEND,LENGTH_TAKE_EQ,CX_length,TAKE_TAKE_EQ]
\\ simp[MIN_COMM,DROP_DROP_T]
\\ Cases_on`n ≤ m` \\ fs[]
\\ rw[]
\\
rw[LIST_EQ_REWRITE,LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
\\ TRY (`m - n = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
\\ TRY (`n - m = 0` by DECIDE_TAC \\ pop_assum SUBST_ALL_TAC)
\\ fs[]
\\ Cases_on`x < n - m`
\\
rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
\\ Cases_on`x < m - n`
\\
rw[LENGTH_TAKE_EQ,CX_length,EL_DROP,EL_TAKE,EL_APPEND1,EL_APPEND2,LENGTH_DROP,EL_LENGTH_APPEND_rwt]
\\ qmatch_abbrev_tac`EL n1 ls = EL n2 ls`
\\ `n1 = n2` by (unabbrev_all_tac \\ decide_tac) \\ rw[]);
val _ = export_theory();
On 14 March 2016 at 19:06, Ada <ada.k...@qq.com> wrote:
> 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))`;
>
> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) =
> LENGTH p)", named "CX_length".
>
> I had tried several times. But the proof failed. How to prove it? Does
> anyone have any good idea?
>
> 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
>
>
------------------------------------------------------------------------------
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
