Hi John,
No it's not that hard. A calculation-like goal such as
CARD {3;4} = 2
is a one-liner in HOL4 and I'd be surprised if that wasn't also
true in HOL-Light. In HOL4 the one-liner is an invocation of the
simplifier, using the implicit set of rewrites, so
RW_TAC (srw_ss()) []
solves it. (You could also invoke EVAL_TAC to prove it.)
BUT. Not all goals are so easy, and just firing off automated tools
blindly never gets very far. So you need to develop a deeper understanding
of what theorems, definitions, and tools are available. Browsing proofs
in set.ml (or whatever it is called in HOL-Light) is bound to be
illuminating.
Maybe re-do some of them in Miz3?
By the way, I can't get access to the HOL-Light documentation at the
moment,
but I'm wondering what {3,4} means in HOL Light. In HOL4 it's a singleton
list
holding a pair of numbers.
Konrad.
On Sat, Nov 3, 2012 at 10:48 PM, John Nicol <nicol.j...@gmail.com> wrote:
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
