Hi John,
in non-declarative mode,
proving `CARD {3} = 1` can be done by
"SIMP_TAC[CARD_CLAUSES;FINITE_RULES;NOT_IN_EMPTY;ARITH]"
proving `CARD{3,4} = 2` can be done by
"SIMP_TAC[CARD_CLAUSES;FINITE_RULES;NOT_IN_EMPTY;IN_INSERT;ARITH]"
(Note: HOL4 also makes use of these theorems in Konrad's tactic, because
they are implicitly contained in srw_ss)
I don't know Miz3, but I guess it should be possible to take the above
theorems and use them with Miz3 so that it would work. (?)
Cheers,
V.
Le 03/11/12 23:48, John Nicol a écrit :
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 <http://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
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
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
