Thanks Bill and Petros for the comments and the code!
Petros, now the need for the real#real type makes perfect sense to me. (I
originally wrote my definitions with OCaml type syntax, and it took me a
long time to figure out why it was failing.) So it's not just me that's
had difficulties with set tactics, and this doesn't seem to be a
one-liner. (If I continue to have problems with sets, perhaps I'll change
to lists also.) And thanks for the code and the goalstack trick! I can
definitely use those if I need to drop back into HOL Light mode.
Bill, your miz3 code is exactly what I needed to continue. Very clear, and
it doesn't require knowledge of the system tactics, which is great! (The
3-element case is especially useful, as I'll need to write something up for
many more elements... it will be an ugly hack, but I can deal with that.)
John
On Sun, Nov 4, 2012 at 11:34 AM, Petros Papapanagiotou <
[email protected]> wrote:
> 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<http://www.cl.cam.ac.uk/%7Ejrh13/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<http://www.proof-technologies.com/tactician/index.html>
>
>
> Hope this helps.
>
> Regards,
>
> Petros
>
>
> --
> Petros Papapanagiotou
> CISA, School of Informatics
> The University of Edinburgh
>
> Email: [email protected]
>
> ---
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
