Hi Freek,
I find GOAL_TAC already very useful! This may suffice for my purposes, for
now.
However, I discovered the following curious effect: The steps that
previously failed without REWRITE_TAC can also be solved using *only*
GOAL_TAC. For example, in the proof I posted a while ago, the following
step will work.
(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then &1
else &0)) [6] by GOAL_TAC,FUN_EQ_THM;
However, if I drop "GOAL_TAC" it will fail with an inference time-out. But
if I understood you correctly, then GOAL_TAC does nothing but "logging" of
the relevant subgoal, correct? So what is going on here?
My current guess would be: GOAL_TAC disables HOL_BY. Instead some different
procedure is used that applies FUN_EQ_THM in some trivial manner - which is
all that is really necessary here, and so this step is proven. And this
"trivial" prover tries something that HOL_BY does not.
I tried to go one step further and even ALL_TAC does something that HOL_BY
does not. So what does
(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then &1
else &0)) [6] by ALL_TAC,FUN_EQ_THM;
do, that
(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then &1
else &0)) [6] by FUN_EQ_THM;
does not?
BTW, thanks, again, for answering my many questions!
Felix
2012/5/7 Freek Wiedijk <[email protected]>
> Hi Felix,
>
> >From what I understand "by REWRITE_TAC[FUN_EQ_THM],2" and "by
> FUN_EQ_THM,2"
> >do very different things: "by FUN_EQ_THM,2" runs the HOL_BY tactic,
> whereas
> >"by REWRITE_TAC[FUN_EQ_THM],2" runs REWRITE_TAC, but not HOL_BY. Or does
> >the second option run first REWRITE_TAC and then HOL_BY?
>
> No, only "REWRITE_TAC[FUN_EQ_THM]" will be run.
>
> In fact, I would write it myself "REWRITE_TAC,FUN_EQ_THM,2".
> The "tactic" in the list after the "by" can have type "thm
> list -> tactic" (in fact, that's the basic ocaml type that
> I designed the thing for, a plain tactic is a derived thing.)
>
> >I'd find it helpful to have some more verbose error reporting for
> inference
> >errors. [...]
> >If I wanted to implement something like this, where would I start?
>
> Ouch! I wrote that code some years ago, and would have a
> hard time myself doing something like this. Basically you'd
> need to tinker with the whole chain of things:
>
> - think of some syntax for what you want
> - adapt the data structures for the proofs to know about
> that syntax
> - handle the extra possibilities in the data structures
> when processing the proofs
>
> So the syntax I was thinking about myself was something
> like
>
> ... by #SOME_TACTIC#,...;
>
> for when you don't want to "grow" the proof already by
> running SOME_TACTIC, but only want to get the subgoals that
> get produced by SOME_TACTIC as the current goals in your
> HOL session. To get the goal for a given justification
> for working on it then would be
>
> ... by ##,...;
>
> I guess. But I don't know whether I would like something
> like this if I tried it. Maybe I'd hate it :-)
>
> Slightly related: the tactic "GOAL_TAC" sets the current goal
> to the first subgoal produced at a certain point in a proof.
> So already you can say things like
>
> ... by #SOME_TACTIC THEN GOAL_TAC,...;
>
> or (as a separate proof step)
>
> exec GOAL_TAC;
>
> And then if you in the HOL session do
>
> p();;
>
> you'll see the goal there.
>
> You can even have "GOAL_TAC"s in the middle of a complicated
> traditional proof:
>
> ... THENL
> [...;
> ... THEN GOAL_TAC;
> ...] THEN
> ...
>
> Sometimes I find that convenient.
>
> Freek
>
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
