Hi,
I was pretty excited and optimistic when I found that HOL Light had
developed a declarative mode, so I started working with the HOL Light
system a few weeks ago. (Without going into the whole philosophy, I prefer
declarative proofs because they're closer to my understanding of proofs,
they're hopefully portable, and hopefully don't involve all the tactics).
So in Freek's Miz3 mode, I wrote up several definitions, a bunch of
unproved theorems, and then:
1. Stumbled through a bunch of hidden type errors in my definitions like
"typechecking error (initial type assignment)". It was really a bear to
track down each of those. BTW, I've used Vincent's typecheck.ml since
then, and it's a huge help; I recommend something like that be added to the
system. Never figured out why real#real is a different type than real*real
(they're both just tuples, right?), but I digress.
2. I tried proving the most basic theorem I had declared. I got some
useful skeleton and syntax errors from Miz3 that helped a lot. But the I
got stuck on Inference or Timeout errors. They didn't tell me much, so
eventually I had to dive into HOL Light tactics and goalstacks directly to
see what was going on.
3. Turned out I couldn't prove *anything*. So I read through a lot of the
2.20 Tutorial, the Reference guide, the Quick Reference, the Very Quick
Reference, Freek's Miz3 paper, Richter's Miz3 notes, mailing list postings,
blogs, various ML proofs...
4. Eventually I was able to prove that the cardinality of {3} was 1, which
I thought should be trivial from something like SET_TAC, but apparently
not. It involved CONJ_TAC, REWRITE_TAC[FINITE_SING], and some other stuff
I've forgotten, but it worked.
5. I still can't prove that the cardinality of {3,4} is 2. Here's what I
have:
let blah_DEF = new_definition `blah={3,4}`;;
g `blah HAS_SIZE 2`;;
e(REWRITE_TAC[blah_DEF]);; (* now I have '{3,4} HAS_SIZE 2' *)
e(REWRITE_TAC[HAS_SIZE]);; (* now I have `FINITE {3, 4} /\ CARD {3,
4} = 2` *)
e(REWRITE_TAC[CONJ_TAC]);; (* two goals *)
e(REWRITE_TAC[FINITE_INSERT;FINITE_RULES];; (* I've proved that a
two-element set is finite now, yay. `CARD {3,4} =2` *)
(* Nothing seems to do anything here, except expanding the definition
more. e[REWRITE_TAC[CARD_CLAUSES] doesn't do anything here... *)
e(REWRITE_TAC[CARD]);; (* `ITSET (\x n. SUC n) {3, 4} 0 = 2` *)
e(REWRITE_TAC[ITSET]);; (* Huh? `(@g. g {} = 0 /\ (!x s. FINITE s
==> g (x INSERT s) = (if x IN s then g s else SUC (g s)))) {3, 4} = 2` *)
And then I'm completely stuck.
REWRITE_TAC[FINITE_INSERT;FINITE_RULES] no longer helps.
REWRITE_TAC[FINITE_INDUCT_STRONG] doesn't help. STRIP_TAC, MESON_TAC[]
barf.
I guess my questions are:
1. It can't really be this hard, can it? What am I missing?
2. Is there a way to rewind in the goal stack if I do something dumb, or
do I have to just redeclare my goal?
3. Is there some basic tactic that I could use for trivial problems to
say, "try everything possible and then tell me what tactics solved this".
I thought that's what things like MESON_TAC were for, but I'm not sure any
more. Would I need to wire in an automated theorem prover or something?
4. Are there any simpler examples than what's in the Examples/ directory?
Thanks,
John
------------------------------------------------------------------------------
LogMeIn Central: Instant, anywhere, Remote PC access and management.
Stay in control, update software, and manage PCs from one command center
Diagnose problems and improve visibility into emerging IT issues
Automate, monitor and manage. Do more in less time with Central
http://p.sf.net/sfu/logmein12331_d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
