Re: [Hol-info] Viewing HOL proofs

Ramana: >For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is >perhaps even better for interactive proof-viewing, since it also keeps >track of where you are up to in the editor buffer, and shows all subgoals >of the proof in the viewing terminal. FWIW, this thing

Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Rob, >>[...] and Freek Wiedijk's vi mode for HOL Light. >Where do I find the above-mentioned vi mode? The current version has been on the web for a while at but there is no link yet. Everyone should feel free to do with it whatever they like.

Re: [Hol-info] proof structure in Coq

Hi Ramana, >Apparently Coq somewhat recently gained the ability to be explicit about >proof structure: >http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html >(Of course that comes naturally when using tacticals like THEN, THEN1, etc.) Not _very_ recently. It was introduced i

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Ramana, >Perhaps it would make more sense to ask people who are using rich type >systems what their motivations are :) >(On this list it's probably mostly people who are satisfied with simple >type theory.) One can do everything with anything. So dependent tpes certainly are not _needed_ for

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Jeremy, >My dominant recollection is the difficulty of getting the system to do the >right type inference, and getting terms to typecheck. I was forever working >out where I needed to put in type annotations. In Coq and Mizar I don't have this experience, in the sense that I hardly ever need

Re: [Hol-info] Tactic

Hi Dylan, What I would try in HOL Light: # g `a ==> b /\ c ==> d /\ e ==> k`;; Warning: Free variables in goal: a, b, c, d, e, k val it : goalstack = 1 subgoal (1 total) `a ==> b /\ c ==> d /\ e ==> k` # e (REPEAT DISCH_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`a`] 1 [`b /\ c`]

Re: [Hol-info] 0 / 0 = 0 ???

Hi Ramana, >I think this is exactly what is impossible to do in HOL: >it is a logic of total functions. I think that in PVS you _can_ do something like that, right? Using the predicate subtypes. Even though PVS _also_ only has total functions. And I _think_ there was a paper once about how to m

Re: [Hol-info] 0 / 0 = 0 ???

Dear all, For what it's worth, a definition of division with 0/0 = 0 won't be possible constructively, because in constructive mathematics all functions of type real->real are continuous, and with this definition division is _not_ continuous. Also, in IEEE 754 floating point of course division is

Re: [Hol-info] Installation Problem of HOL-Light

Dear all, Some time ago (in the times of Debian Stretch :-)) I made a Dockerfile for HOL Light, see the attachment. The commands I used for building the image and running it are: docker build -t hol-light . docker run -i -v /home/freek:/home/freek --name hol-light hol-light You need to run

Re: [Hol-info] Visualizing subgoals in a proof script

Dear Mario, >Hello. In HOL4 is there a way to generate something like the entries in >Metamath proof explorer for the subgoals generated within a proof and >the tactics used to solve them? Example: > For HOL Light there is Mark Adams's "tactician" which

[Hol-info] Calculemus 2008: First Call for Papers

Franche-Comte, France) Tomas Recio (Universidad de Cantabria, Spain) Renauld Rioboo (Universite Pierre et Marie Curie, France) Julio Rubio (Universidad de La Rioja, Spain), Chair Volker Sorge (University of Birmingham, UK) Makarius Wenzel (Technische Universitat Munchen, Germany) Freek Wiedijk (Radboud

[Hol-info] Calculemus 2008: Second Call for Papers.

Universitat Munchen, Germany) Freek Wiedijk (Radboud University Nijmegen, Netherlands), Chair Wolfgang Windsteiger (RISC-Linz, Austria) - This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008

[Hol-info] Calculemus 2008: extended deadline March 14

Universitat Munchen, Germany) Freek Wiedijk (Radboud University Nijmegen, Netherlands), Chair Wolfgang Windsteiger (RISC-Linz, Austria) - This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio

[Hol-info] Call for Presentations at AISC'08 and Calculemus 2008

-- [ We apologise if you receive multiple copies ] -- Call For Presentations == jointly for AISC'08 -- Artificial Intelligence and Symbolic

[Hol-info] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR)

ember 2008. * Notification: January 16th 2009. * Final versions: March 30th 2009. Editors of the special issue * Jacques Carette (McMaster University, Canada) * Makarius Wenzel (Technische Universitaet Muenchen, Germany) * Freek Wiedijk (Radboud University Nijmegen, N

[Hol-info] Second CFP - JAR special issue for PLMMS

ember 2008. * Notification: January 16th 2009. * Final versions: March 30th 2009. Editors of the special issue * Jacques Carette (McMaster University, Canada) * Makarius Wenzel (Technische Universitaet Muenchen, Germany) * Freek Wiedijk (Radboud University Nijmegen, N

[Hol-info] System Announcement: ProofWeb

ProofWeb home page. Cezary Kaliszyk Dan Synek Femke van Raamsdonk Freek Wiedijk Herman Geuvers James McKinna WHAT IS PROOFWEB? ProofWeb is both a system for teaching logic and for using proof assistants through the web. ProofWeb can be used in three ways. First, one can use the guest login, for

[Hol-info] "The QED Project"

ous whether there is anything interesting to say to this question.) Freek Message-ID: <4975cdb4.2010...@univie.ac.at> Date: Tue, 20 Jan 2009 14:12:20 +0100 From: Arnold Neumaier To: Freek Wiedijk Subject: The QED Projec

[Hol-info] 1 Postdoc and 1 PhD vacancy in the MathWiki project

1 POSTDOC and 1 PHD POSITION in the MathWiki project at Radboud University Nijmegen (NL) http://www.fnds.cs.ru.nl/fndswiki/Vacancies The Institute for Computing and Information Science of the Radboud University Nijmegen (NL) is looking for 2 researchers to work on the NWO

[Hol-info] ITP 2011 (Call for Papers)

search Mike Kishinevsky, Intel Conference co-chairs: Marko Van Eekelen, Radboud University Nijmegen/Open University of the Netherlands Herman Geuvers, Radboud University Nijmegen Julien Schmaltz, Open University of the Netherlands/Radboud University Nijmegen Freek Wiedijk, Radboud Universi

[Hol-info] ITP 2011 (Call for Workshop Proposals)

Eekelen, Radboud University Nijmegen/Open University of the Netherlands Herman Geuvers, Radboud University Nijmegen Julien Schmaltz, Open University of the Netherlands/Radboud University Nijmegen Freek Wiedijk, Radboud University Nijmegen

[Hol-info] Call for bids ITP 2012

the voting phase will take place. The people eligible to vote are those who are seriously thinking of attending ITP 2012. The voting system used will be Single Transferable Vote between all received bids. Marko van Eekelen Herman Geuvers Julien Schmaltz Freek Wiedijk

[Hol-info] Call for Papers ACL2 2011

A) David Russinoff (AMD, USA) Jun Sawada (IBM, USA) Julien Schmaltz (Open Universiteit, The Netherlands) Natarajan Shankar (SRI, USA) Sol Swords (Centaur, USA) Freek Wiedijk (Radboud Univ. Nijmegen, The Netherlands) -- WhatsUp

[Hol-info] ITP 2011 (Call for Participation)

CALL FOR PARTICIPATION ITP 2011: 2nd International Conference on Interactive Theorem Proving 22-25 August 2011, Nijmegen, The Netherlands http://itp2011.cs.ru.nl/ - Important dates:

[Hol-info] Mizar Light and miz3

Dear everyone, John Harrison pointed out to me that the following query was posted on the hol-info mailing list (I'm subscribed to that list but often just delete the messages without looking, sorry about that. So I missed this): >6) I am very curious about Mizar Light and would like to convert

Re: [Hol-info] Mizar Light and miz3

Hi Felix, >4) I start gvim and load a file with the following content: > >let ARITHMETIC_SUM = thm '; > !n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2 > proof > qed by #INDUCT_TAC; >';; The quotes should be backquotes. With this I think miz3 will try to execute this as ocaml source (it does not mat

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi John and Makarius, This is not very much about HOL as such, so if this reply is inappropriate for the HOL list, I apologise: >>mutating the names of constants. I always found this "mutable constants" complaint silly. Many people make it, but it never struck me as significant. Surely in every

Re: [Hol-info] Mizar Light and miz3

Hi Felix, >* The miz3 version is not only readable, but also not too far away from >what I might write in an informal proof. This is great! The miz3 language is just an almost exact copy of the Mizar proof language, so this praise should go to Poland :-) >- Working with definitions requires a tr

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi John, >Then every theorem would become |- TarskiModel((===),Between) ==> P >instead of just |- P. Couldn't you set up things in a way that all the theorems would have the form "TarskiModel((===),Between) |- P"? I think I would find that more attractive. Freek

Re: [Hol-info] Mizar Light and miz3

Hi Felix, >From what I understand "by REWRITE_TAC[FUN_EQ_THM],2" and "by FUN_EQ_THM,2" >do very different things: "by FUN_EQ_THM,2" runs the HOL_BY tactic, whereas >"by REWRITE_TAC[FUN_EQ_THM],2" runs REWRITE_TAC, but not HOL_BY. Or does >the second option run first REWRITE_TAC and then HOL_BY? N

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, I'm pondering the issue of miz3 not allowing free variables in contrast with how you want to work in an axiomatic framework. However, already: > !(===) (Between:point#point#point->bool) (cong). >TarskiModel((===),(Between:point#point#point->bool),(cong)) > let (===) be poi

Re: [Hol-info] Mizar Light and miz3

Hi Felix, >However, I discovered the following curious effect: The steps that >previously failed without REWRITE_TAC can also be solved using *only* >GOAL_TAC. For example, in the proof I posted a while ago, the following >step will work. > >(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n.

Re: [Hol-info] miz3 comments, statement labels, and `case ... by '

Hi Bill, First a reply to your other mail: >I can't understand what's wrong with this proof below. This is the >only thm I wrote where the conclusion is there-exists statement, and >I'm guessing that's the problem. Nah, there's nothing special about that. >The to-me incomprehensible Mizar_erro

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >Freek's miz3 code in the miz3 dox 1201.3601-1.pdf >solving the drinker's paradox on p 13--14 is perhaps designed to show >various features of miz3, but it is more than twice as long as needed: It's mainly intended to be as close as possible to the Jaśkowsky/Fitch-style natural deduction

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill & John, >| Better error messages would be great. The way the error messages work is that first the proof is split into "steps" based on the semicolons and keywords. (I think certain keywords always start a new step and semicolons always end one, with "now" and "proof" being the exception

Re: [Hol-info] Proof assistants and high school math

Hi Grant, >Are you familiar with Michael Beeson's MathXpert (formerly MathPert)? Yes, MathXpert-level mathematics is exactly what I had in mind when I was talking about "high school mathematics". The main difference between what MathXpert provides and what I was asking for, is that MathXpert is

Re: [Hol-info] Proof assistants for way more people

Hi Mark, >It's just that no-one's done it yet! There are just two things that make proof assistants difficult to use: 1. There is not sufficient automation of trivial stuff. I.e., you generally need to break down your reasoning into smaller steps than how you would experience things when

Re: [Hol-info] Proof assistants for way more people

Hi Cris, >I was speaking from a software engineering and usability >point of view. Okay, just to fix our minds: would you consider Knuth's/ Lamport's latex to be "usable" in this sense? Because I would strongly claim that it is. It's one of the most usable systems I know. That's why I think th

Re: [Hol-info] Proof assistants for way more people

Hi Ramana, >Later, after a long exploratory theory development, having settled on the >right structures, you can go back and fill in the cheats with real proofs, Yes, for example Peter Aczel was arguing for this once too, I think. It's a tempting approach. But my experience is that whenever I t

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >I think miz3 is much less powerful than HOL Light is generally. Sorry to disagree, but this seems wrong to me. This is only true if you don't put tactics in the justifications. I especially allow _arbitrary_ HOL Light tactics there for exactly this reason: so miz3 would be just as "pow

Re: [Hol-info] Proof assistants for way more people

I forgot who wrote this One way to ameliorate this problem is to compose proofs lazily. but anyway: Doesn't the Isabelle kernel now have a feature that you can "postpone" proving a thm and still already being allowed to use it? I think Makarius put that in the kernel especially to be able

Re: [Hol-info] Proof assistants for way more people

Hi Ramana, >In HOL4 that is called PROVE_HYP. In HOL Light too, thanks for answering my question! (Its arguments have the opposite order from the function I wrote though :-)) >In HOL4 you can control how much assumptions are printed >with a trace called "assumptions", HOL Light just prints them

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Michael, >miz3's "by" is just an invocation of MESON but with, >as I understand, a time limit imposed. FWIW, one can turn off the time limit by setting "timeout" to -1. This is useful for example if one wants to recheck a proof that is known to be correct on a slow computer. Of course, if a

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Ramana, >Isn't MESON (without limits) complete? I think it's complete for first order logic (although I'm not completely sure about whether it's complete for first order logic with equality). However, we're in a higher order logic here, right? So I guess it won't be complete for the HOL logi

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >MESON[] >`(!x y z. P x y /\ P y z ==> P x z) /\ >(!x y z. Q x y /\ Q y z ==> Q x z) /\ >(!x y. P x y ==> P y x) /\ >(!x y. P x y \/ Q x y) >==> (!x y. P x y) \/ (!x y. Q x y)`;; > >MESON solves this logic puzzle (which I still haven't yet >solved) quite quickly, and it writes >...solved

Re: [Hol-info] HOL and the axiom of choice

Hi Cris, To chime in on this: I don't have any problems with a system that doesn't allow you to disable the axiom of choice. In other words: hardwire choice all you like as far as I'm concerned. Without AC you get weirdnesses as that a union of countably many countable sets doesn't need to be pr

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >Why are miz3 and Mizar the only proof assistants where >one can easily write up human readable proofs? I'm surprised you're not including Isar in this list! And do you know about ForTheL (see )? Now _there's_ a readable formal language! :-) Al

Re: [Hol-info] HOL and the axiom of choice

Hi Rob, > (exists f. forall x. P(x, f(x))) <=> (forall x. exists y. P(x, y)) So _this_ is the kind of choice that I have no problems with, as it doesn't threaten my Platonism. (It is even provable in type theory! (But only if you use the right flavor of existential quantifier of course :-)))

Re: [Hol-info] HOL and the axiom of choice

Hi Cris, >At a philosophical level I'm surprised that Freek's >intervals of Platonism are during the week, with formalism >on weekends. It was a reference to a book related to the "philosophy" of mathematics that I liked a lot when I was much younger. See the quote on

Re: [Hol-info] HOL and the axiom of choice

Hi Michael, >[...] >Use standard principle that allows constants to be >"defined" once existence is proved to give yourself the >choice operator. > >Now, if you believe in the way HOL Light implements that >last definitional principle, you'll object that this uses >the choice operator. :-) Yes,

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >Can you jump into the discussion Michael and I were having >about whether miz3 is intentionally weakened? Michael seems >to think yes, I think no, but I wonder what effect the MESON >depth limit of 50 has, or the fact that MESON is just FOL >and not HOL. Ah no, there were no deep thoug

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Bill, >Thus, I conclude that the purpose of the default timeout >isn't to weaken miz3, but to better instruct beginners Ah no, the main point was that if an inference is _not_ correct, often MESON will run for the full timeout time. So checking proofs with errors (= all proofs when you're not

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

Hi Michael, Okay, final mail I'm sending about this: >1. miz3's "by" is designed (i.e., someone intentionally >chose to do this) with a time limit. Well, the time limit even is there if you put a tactic there yourself. So I would distinguish between the default "by" prover, and the time limit t

Re: [Hol-info] Fixing HOL Light

Phil: >When a theorem is proven and HOL Light announces "no >subgoals", there is no jingle. or musical fanfare. Please >fix. How about? let e tac = let gs = refine(by(VALID tac)) in match gs with | (_,gls,_)::_ -> if length gls = 0 then let _ = Unix.system ("mpg123 -q "^(!hol_dir)^

Re: [Hol-info] Learning HOL Light

Vincent: >Then each time you type something that starts with a semi-colon (e.g., >`;blabla`), you obtain the intermediate preterm instead of the term. Hey! miz3 already uses `;...` for proofs. So maybe it's less confusing if you use another symbol to get preterms? Freek -

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Chris, Thanks for bringing up this topic, which is very interesting question to me. It's question III in my talk . I'm replying here because there is an approach that I've been wanting to develop for a while now (but haven't really started work on).

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Mike, >Taking definedness to the level Freek is discussing would, >I think, not let you prove that > > x DIV 0 = x DIV 0 Exactly. I think that what I want is much closer to PVS and B than to IMPS. I also don't want any change to the logic. I _hate_ partial logics. I want to be able to use

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Rob, >Given a Z specification it could generate a set of proof >obligations called domain conditions. The idea was that >if the domain conditions were true, then the specification >was insensitive to the interpretation of undefined terms. This is exactly what I was trying to describe, and the

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Chris, My apologies for carrying on about this, but I care for this subject, sorry. >At some phases of the moon this sounds attractive to me too. For me too :-) The main problem is that you will get lots of extra proof obligations, so it's _not_ "efficient". You can _hope_ that the automatio