Hello John,
On 04/11/2012 03:48, John Nicol wrote:
> Never figured out why
> real#real is a different type than real*real (they're both just tuples,
> right?), but I digress.
Unless I'm missing something, real*real is the OCaml notation for a pair
of reals, whereas real#real is the HOL Light notation.
There is no 'real*real' type in HOL Light as * is parsed as the times
operator.
> 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.
>
> [...]
>
> I guess my questions are:
> 1. It can't really be this hard, can it? What am I missing?
I have also experienced some pain trying to achieve simple calculations
for sets in HOL Light (to the point where I chose to change my
formalisation to using lists).
Unfortunately, to my knowledge, HOL Light only provides SET_TAC as an
automated tactic for sets, which is often insufficient for such
calculations.
I tried this particular example and came up with a proof based on
CARD_CLAUSES, assuming you have already proven the cardinality of a
singleton set, ie. CARD {4} = 1:
g `CARD {4} = 1 ==> (CARD {3,4} = 2)`;;
e (SUBGOAL_TAC "" `FINITE {4}`
[REWRITE_TAC[FINITE_RULES;FINITE_INSERT]]);; (* You need finiteness to
reason about cardinality. *)
e (FIRST_ASSUM (SUBST1_TAC o (MATCH_MP (ISPEC `3` (CONJUNCT2
CARD_CLAUSES)))));;
e (DISCH_THEN SUBST1_TAC);;
e (REWRITE_TAC[IN_SING]);;
e (NUM_REDUCE_TAC);;
I'm sure there are others that can suggest better proofs.
More generally it might be easier to build small lemmas to help reason
about such computations more easily, such as:
let CARD_SING = prove ( `!a:A . CARD {a} = 1`, REWRITE_TAC[ONE;MATCH_MP
(ISPECL [`a:A`;`{}:A->bool`] (CONJUNCT2 CARD_CLAUSES)) FINITE_EMPTY;
CARD_CLAUSES;NOT_IN_EMPTY]);;
At least for me it has been standard practice to build my own little
libraries of lemmas to make reasoning about a particular theory easier
and more tailored to my needs.
> 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?
You can use:
b();;
which stands for "back".
> 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?
There are some automated tactics for particular sets of problems such as
MESON_TAC, NUM_REDUCE_TAC, REAL_ARITH_TAC, ITAUT, etc, but nothing more
general than MESON_TAC.
More generally, it takes some experience and going through the existing
lemmas and tactics (eg. through
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference_220.html) to become
accustomed to what you can use in each case.
> 4. Are there any simpler examples than what's in the Examples/ directory?
You may find it useful to inspect individual files containing the
theories you are interested in, such as sets.ml.
They usually include general lemmas and you can understand a lot about
how theories can be developed in HOL Light.
You can expand packaged proofs to step-by-step tactics using Tactician:
http://www.proof-technologies.com/tactician/index.html
Hope this helps.
Regards,
Petros
--
Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: p.papapanagio...@sms.ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
