Hi Konrad,
Thanks! I hope it turns out to be that easy in HOL Light :-)
Yes, I browsed sets.ml, which is how I found the various FINITE_* tactics
and theorems. I also did greps on the sources to look for uses of CARD and
HAS_SIZE and see how they were used. No dice.
{3,4} in HOL Light is set enumeration syntax (page 92 of the Tutorial), so
is, AFAIK, a set containing two elements.
Blindly firing off automated tools is not necessarily a bad thing! If
doing so gives you an answer you can learn from (regardless of success or
failure), then it's useful.
John
On Sun, Nov 4, 2012 at 8:39 AM, Konrad Slind <[email protected]> wrote:
> 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 <[email protected]> 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
>> [email protected]
>> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
