Hi Freek,
2012/5/4 Freek Wiedijk <[email protected]>
> >- Working with definitions requires a trick: If you want to make a couple
> >of definitions, you need to make sure that there are no blank lines
> between
> >your definitions and the theorem you are working on
>
>
> Huh? No, that's not how I intended things.
>
> The "Ctrl-C RET" really does two completely different things,
> depending on what the "block" that you're in looks like.
> If it starts with "let LEMMANAME = thm `;" it will get the
> miz3 treatment, have errors messages put in if necessary,
> etc. But if it does _not_ look like that, it's just
> copy-pasted as ocaml to the HOL session. This second
> behavior was a late addition to the interface, just as
> a convenience. Apparently for you that has caused confusion.
>
> What you should do is to have blank lines around the
> defintion from the start. So process it with "Ctrl-C RET"
> (then it will be sent as ocaml and processed that way,
> because it doesn't look like a lemma) _or_ copy-paste
> it to the HOL session as you would have done without the
> miz3 thing. And then further leave it alone and go on with
> the lemmas after it.
>
Thanks for the explanation! I had actually tried copy-and-pasting the
lemmas into the HOL session. But apparently I made a mistake so that it did
not work, and was then convinced that copy-and-paste does not work in
general. Anyway, now I got it!
> >- Of course you cannot use backticks inside a block of miz3 syntax. So if
> >you want to do something like (SPEC `(\k. f k * recip f (x - k))`
> >SUM_CLAUSES_LEFT) within miz3 you need to write it as (SPEC (parse_term
> >"(\\k. f k * recip f (x - k))") SUM_CLAUSES_LEFT). I.e.: use the
> parse_term
> >function, use double-quotes and escape your backslashes.
>
> Exactly. I also regret this.
>
> Originally I wanted to use the syntax ``...`` for proofs
> and then allow "nested" quotes like ``... `...` ...``.
>
> However, to have accomplished that, I would have needed
> to tinker with the "pa_j.ml" file, which I consider "holy"
> and untouchable. Or, stated differently: I wanted to keep
> the whole thing contained to the single file "miz3.ml".
> So in the end I went for the `;...` syntax for proofs, as
> the second best option. And then there couldn't be nested
> quotes anymore.
>
I can completely understand that you did not want to touch pa_j.ml :) And I
can live with the current syntax. It just confused me when I ran into this
issue for the first time.
> >I can drop REWRITE_TAC almost everywhere (and
> >list only the theorems I would pass to REWRITE_TAC) but for some reason
> >this does not work in these last two lines.
>
> The current miz3 system has two main weaknesses:
>
> - The "by" justifier is not what it should be. If you can
> prove something trivially by REWRITE_TAC, then "by" should
> be able to do that too. As you found out, currently it's
> not that way. This "wrong by" is of course orthogonal
> to the basic design of the system. But from a user's
> point of view it is very bad, yes.
>
What I find puzzling is that REWRITE_TAC can be omitted in most cases but
not in all. I'd like to find out what is going wrong in the cases where
REWRITE_TAC has to be stated explicitly.
>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?
I tried reproducing this inference step in a standard HOL session. In this
case REWRITE_TAC[FUN_EQ_THM,LEMMA], where LEMMA is the theorem referred to
by 2, does actually not suffice to solve the goal. Rather I had to do
REWRITE_TAC[FUN_EQ_THM], then FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP LEMMA))
and then ASM_REWRITE_TAC[].
>
> - There is not a good interface to "develop" the
> justification tactic in a "by" without already firing
> it into the proof. I have some ideas on an extension to
> the interface for this, but currently I'm not working on
> this either.
>
I'd find it helpful to have some more verbose error reporting for inference
errors. Maybe something like this:
* If no tactics are given, print the goal stack that the defaultprover has
to solve in that instance.
* If some tactics are given, print the goal stack before and after all
those tactics have been applied.
If I wanted to implement something like this, where would I start?
>
> The other shortcomings are _to me_ minor inconveniences.
> But these two are big ones, yes.
>
On the whole, I am very happy with miz3! :)
Felix
--
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
