Also, since the proof appears not to mention CX_def anywhere, it should be
possible to generalise the theorem to be about any two lists with the same
length (and not mention CX); that might be an easier statement to deal with.
On 15 March 2016 at 09:25, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> 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
