Hi everyone,
I have to prove a goal in HOL4:
g`!(A:('a , 'b) matrix) (B:('c , 'a) matrix) (C:('d , 'c) matrix). A ** (B **
C) = (A ** B) ** C`;
After having applied SRW_TAC as following, I could not find the solution to
prove the subgoal:
e(SRW_TAC [fcpLib.FCP_ss] [matrix_prod]);
1 subgoal:
> val it =
sum (0,dimindex (:'a))
(\k.
A ' i ' k *
(FCP i j. sum (0,dimindex (:'c)) (\k. B ' i ' k * C ' k ' j)) ' k '
i') =
sum (0,dimindex (:'c))
(\k.
(FCP j. sum (0,dimindex (:'a)) (\k. A ' i ' k * B ' k ' j)) ' k *
C ' k ' i')
------------------------------------
0. i < dimindex (:'b)
1. i' < dimindex (:'d)
: proof
And I have failed to use “e(MATCH_MP_TAC SUM_EQ)”, because the “dimindex(:’a)”
was not equal to “dimindex(:’c)”.
Could anybody give me some hints?
I really appreciate your help!
The loaded libraries are listed here:
app
load["HolKernel","bossLib","fcpTheory","listTheory","wordsLib","realTheory","realLib","simpLib","boolTheory","boolLib","mesonLib","Parse","fcpLib"];
open bossLib fcpTheory listTheory wordsLib realTheory realLib simpLib
boolTheory boolLib mesonLib Parse fcpLib;
val _ = type_abbrev ("matrix", ``:(real ** 'a) ** 'b``);
val matrix_prod = Define`matrix_prod (A:('p , 'm) matrix) (B:('n, 'p) matrix) =
(FCP i j. (sum(0,dimindex(:'p)) (\k. (A %% i %% k) * (B %% k %% j)))):('n , 'm)
matrix`;
val _ = overload_on ("**",``matrix_prod:('p , 'm) matrix -> ('n , 'p) matrix ->
('n , 'm) matrix``);
Amy------------------------------------------------------------------------------
This SF.net email is sponsored by Sprint
What will you do first with EVO, the first 4G phone?
Visit sprint.com/first -- http://p.sf.net/sfu/sprint-com-first
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
