Here is a fragment of working code (but depending on some previous stuff
not shown, so you can't just run this code). Since the code works, you
don't
need to run it--I'm just asking if it really needs to be this complicated.
Details below.
let tapermutation = MATCH_MP ta3 ta2;; # tarea(c,a,b) = tarea(a,b,c)
let tadditive = prove
( `L(b,d,c) ==> tarea(d,a,b) + tarea(c,a,d) = tarea(c,a,b)`,
CONV_TAC (PAT_CONV `\x. L(b,d,c) ==> cc + cc = x`
(REWRITE_CONV[tapermutation])) THEN
MESON_TAC[tadditive1]
);;
Observe the main goal in tadditive, namely
`L(b,d,c) ==> tarea(d,a,b) + tarea(c,a,d) = tarea(c,a,b)`.
At this point I already have a theorem tadditive1, which differs
from that goal only in having area(c,a,d) in the last place instead of
tarea(c,a,b).
So all we have to do is use tapermutation to rewrite that last tarea(c,a,b).
But, we have to rewrite ONLY that term, and not the other tarea terms.
We can do that kind of thing with PAT_CONV, but it only works on
conversions, and SIMP isn't a conversion, hence the convoluted code
above that makes REWRITE into a conversion, then uses PAT_CONV, and
that makes that back into a tactic. Sheesh, does it really have to be
like this?
In particular, in a FORWARDS proof is there any way to direct SIMP or
REWRITE to work only on certain subterms?
Then the final line with MESON_TAC; that works, but why
didn't the following work?
# e (CONV_TAC (PAT_CONV `\x. L(b,d,c) ==> cc + cc = x`
(REWRITE_CONV[tapermutation])));;
Warning: inventing type variables
val it : goalstack = 1 subgoal (1 total)
`L (b,d,c) ==> tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)`
# tadditive1;;
val it : thm =
|- !a b c d. L (b,d,c) ==> tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
# e (ACCEPT_TAC (SPEC_ALL tadditive1));;
Exception: Failure "ACCEPT_TAC".
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
