Does anyone know how to formalize an axiom schema in HOL Light? I'm interested
in formalizing the Tarski axiomatic geometry
Axiom schema of Continuity
http://en.wikipedia.org/wiki/Tarski%27s_axioms#The_axioms
and the part I don't know how to handle involves the universal quantification
Let
Ramana and Robert, matrix multiplication in HOL Light is defined in the
Multivariate directory. I'm not a real expert on this, but you can find
examples of Multivariate-powered matrix multiplication in
Thanks, Rob! I think we're in agreement on the substantive issues, after I
agree with your true correction:
If you replace “true” by “provable”, then this is how one would
state Andrews’ claim that the rules of N are admissible in FOL.
Yes, thanks for the correction. So we're just
Rob, I want to argue that Peter Andrews's book To Truth Through Proof supports
my idea of informal mathematics documentation for HOL Light. I don't
understand yet how the informal math compares to your HOL documentation
http://www.lemma-one.com/ProofPower/specs/spc001.pdf
Mostly I'm going
Thanks, Rob! You seem to be correct about Andrews's book To Truth Through
Proof. His Chapter 5 Type Theory is 56 pages long, and it's mostly about Q_0
which is based on equality, which he calls Q:A-A-bool, and I notice that he
prove the only truth table result I was able to prove:
|- T ∧ T =
Thanks, Rob! Then since I only technically have a model, I would say I'm
working in your class (c):
(c) Informal mathematical proofs that an assertion is provable in
some agreed deductive system.
I still don't understand what you're saying about class (d), or why this is
true:
Your
Thanks, Rob! You're right, I hadn't looked at Section 1.4 A Formulation Based
on Equality of Andrew's link
http://plato.stanford.edu/entries/type-theory-church/ and more to the point,
I didn't read the longer version Andrew's wrote in his book To Truth Through
Proof:
More details about
Mark, I tried to make your corrections, and here's my new draft, at just 500
lines:
I want to explain how to read the HOL Light basics from the source code in
several sections
0) informal math and HOL
1) the type bool and the constant =
2) sequents, new_basic_definition and the HOL Light
I want to explain how to read the HOL Light basics from the source code in
several sections
0) colloquial (informal) math and HOL
1) the definitions of type bool and the constant =
2) sequents, new_basic_definition and the HOL Light inference rules
3) The BETA_CONV proof of general
Thanks, Mark! I figured out the constant = myself, but it would have saved me a
lot of time if I checked my mail yesterday when you explained it :)
I should have said '@' instead of '?' here. The constant '?' is
actually defined in these axiomatisations (using '@').
This is true for
Thanks, Konrad! You seem to agree with me here, that the typed-LC-implies-FOL
isn't actually important:
My personal feelings on this foundational aspect are that the
actual set of axioms isn't that important provided the usual
introduction and elimination rules of predicate calculus
Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find Gordon
and Melham's book. Two points:
I don't believe that Church ever explained how typed LC implies FOL. Church
certainly does not explain this in his paper
A Formulation of the Simple Theory of Types
Thanks for correcting me, Mark! I'll look at your HOL Zero source code,
especially corethy.ml. I see my error now. From bool.ml:
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
The first = is an Ocaml =, but the 2nd =, the one we care about, is the
primitive HOL
Thanks, John and Rob! The main problem I'm having is actually embarrassingly
simple: I don't understand the typed Lambda Calculus angle in Church's work or
HOL. Now I definitely see the point of having functions as well as sets, and
that means that the HOL type theory (sets are either types
2. The argument formerly used a direct port of the original
Diaconescu proof as presented in Beeson's Foundations of
Constructive Mathematics. But in July 2009 I changed it to a
somewhat optimized variant shown to me by Mark Adams. This is
noted in the CHANGES file
Thanks, Konrad! I see that the HOL light BOOL_CASES_AX is proved in class.ml
using the result I mentioned, EXCLUDED_MIDDLE, which class.ml says is derived
from Beeson's book:
let BOOL_CASES_AX = prove
(`!t. (t = T) \/ (t = F)`,
GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE)
I'm trying to understand Tom Hales's compact description of HOL Light in his
AMS Notices article www.ams.org/notices/200811/tx081101370p.pdf
The first things I don't understand are the type bool and the beta-conversion
inference rule.
Isn't there an axiom that there are exactly two term type
Vince, this is very interesting:
I would say what is bad coding is not to rely on features you don't
understand but on features that are actually
undocumented/unintended. Here, the ordering chosen is indeed
ingenious to prevent some often-met looping situations. However,
as John
Back to my other question, there's something about USE_THEN and type
annotations I don't understand. I get the same problem with FIRST_ASSUM. In
Multivariate/topology.ml there's a theorem
let FRONTIER_CLOSURES = prove
(`!s:real^N-bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`,
Thanks, John! I'll read p 34 more carefully. Your example shows the behavior
I'd want from REWRITE_TAC. You theorem is
# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
This is a good exercise for my right associativity skill. and that's what it
I have a question about REWRITE_TAC. I was invited to speak at the conference
https://ihp2014.pps.univ-paris-diderot.fr/doku.php?id=workshop_1
where John, Freek, Tobias Nipkow and Tom Hales are 4 of the 14 plenary
speakers, and I hope folks here will help answer various HOL Light questions I
Here's a question about free variables and REWRITE_TAC (and other
thmlist-tactics). Almost every usage of USE_THEN in the HOL Light sources is
of the form
USE_THEN label MATCH_MP_TAC
Here's an example of a labeled assumption used in thmlist of MESON_TAC:
let NSQRT_2 = prove
(`!p q. p * p =
In my last post I should have said instead that HOL programmers have very good
concrete down-to-earth adjoint functors skills, which pure mathematicians tend
to have good theoretical adjoint functors skills, and maybe interfaces that
hides the adjoint functors calculations are good.
Today I'd
Rob, I think Michael's IMAGE idea may show that I was wrong about your semantic
embedding idea. I said that I was happy with the HOL Light parser's definition
of the set comprension
{f x | R x} = {a | ∃x. a = f x ∧ R x}
and I didn't think that it made sense to talk about the semantic value
I want to explain GEN_REWRITE_TAC, which I just understood (partly because of
Rob and Michael's advice here about is_comb etc), and to argue that
1) HOL programmers are very good at the pure math skill of adjoint functor, and
2) getting mathematicians to use HOL may require an interface that
Rob, thanks for correcting my variable capture mistake:
In this case, the two instances of x have different types and there
is no variable capture, since two variables with the same name but
different types are considered to be distinct in the logic.
Right, and you have to do the type
Rob, I learned a lot from your post! My conclusion is that in both HOL Light
and HOL4,
{f x | R x} = λa. ∃x. R x ∧ a = f x
for some variable a than is not free in R x or f x. I judge both HOL
approaches to have pluses minuses, and can't rate one above the other:
1) In HOL Light, the proof
Michael, that's very helpful! You taught me something about term.ml, and
reminded me of that every HOL term is either a constant, a variable, a function
(abstraction) or a function application (combination). So pasting your code
into HOL Light gives the right answers:
let PrintTermType tm =
Thanks, Rob! This is helpful info:
In all the HOLs, you will find that the parser uses various
constants like [the SETSPEC definition] to represent derived
syntactic constructs (like set comprehensions) in terms of
primitive constructs (like conjunction and equality) in such a way
Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC?
I would think that GSPEC would have to choose a fresh variable, and I've never
understood how that's to be done, because you have know that your new fresh
variable hasn't already been chosen. So I would think that
Rob, I think the answer to your interesting question involves more complicated
set abstractions like {y + 6 | y 0}. I think here we see the merit of the
HOL Light invisible variables, as this simple proof shows:
g `EMPTY = {y + 6 | y 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;
John, I'm sorry it took me so long to respond to your MP_TAC vs MESON_TAC post
of Jun 1:
| What's the difference between MESON_TAC[th1; th2; th3];; and
| MP_TAC th3;;
| MESON_TAC[th1; th2];;
The difference is that after MP_TAC any free variables or free type
variables
Mark, I now understand your HOLZero/print_exn idea, and it works pretty well:
exception Readable_fail of string;;
let PrintErrorFail s = raise(Readable_fail s);;
let print_exn e =
match e with
| Readable_fail s
- print_string s
| _ - print_string (Printexc.to_string e);;
Mark, your update_database.ml idea worked great! My code simplified to
(* From update_database.ml: Execute any OCaml expression given as a string. *)
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
(* exec and a
Mark, I think you can write some good Light documentation, and maybe improve
the HOL Light code. Let me try to explain. My only objection to my
PrintErrorFail is minor: it prints
Exception: Failure .
at the end, but arguably this is a good error message. Here's what I like
about my def:
1)
Thanks, Mark! I see your include Format;; in printer.ml. By grepping, I see
occurrences of Format.print_string and Format.print_newline commands in e.g.
make.ml, but isn't the Format prefix here unnecessary, because they're
pervasive? Isn't that explained in section
20.2 Module Pervasives :
Thanks, Vince! Your is_thm works fine, but I get a warning when I try to
extend your idea:
let is_thm s =
try ignore (exec_thm s); true
with _ - false;;
let is_tactic s =
try ignore (exec_tactic s); true
with _ - false;;
let is_thmtactic s =
try ignore (exec_thmtactic s); true
I hope folks can help me improve my code readable.ml, which in the new
subversion 166 is in
hol_light/RichterHilbertAxiomGeometry/
1) Can you pretty-print error messages in HOL Light? E.g. here:
with Not_found - failwith(missing initial \proof\ or final \qed;\ in ^ s)
It would be nice to at
I just noticed that Voevodsky's Homotopy Type Theory book deals on p 7 with
issues I've posted here:
http://hottheory.files.wordpress.com/2013/03/hott-online.pdf
One difficulty often encountered by the classical mathematician when
faced with learning about type theory is that [it is not
Thanks for the great response, John! I'm sorry it took me so long to respond,
and I still don't have a good response, but:
l think I see what you're saying about MP_TAC, MESON_TAC and FREEZE_THEN, and
I'll have to do more experiments.
I ought to learn how parse_preterm works, and I would if
Can someone explain the point of HOL Light parsers, as in the reference manual
entry for many:
This is one of a suite of combinators for manipulating
``parsers''. A parser is simply a function whose OCaml type is some
instance of :('a)list - 'b * ('a)list. The function should take a
Thanks, Ramana! I think it would be good to compare what I'm doing with how
things are in HOL4, because
1) John has always stressed the importance of readability in formal proofs, and
2) my code looks like it will be a lot simpler than John's mizar.ml or Freek's
miz.ml.
I know nothing of
Thanks, Ramana! I created my thmlist_tactics list in the same way that HOL
Light creates the theorems database in hol_light/database.ml:
needs help.ml;;
theorems :=
[
ABSORPTION,ABSORPTION;
ABS_SIMP,ABS_SIMP;
ADD,ADD;
[...]
vector,vector
];;
That doesn't strike me as a painful solution, but I
Thanks, Freek, Ramana and Vincent! I think (assoc thm !theorems) gives a nicer
solution:
RK In HOL Light I guess there's no database of theorems indexed by
RK names? That would be one way to avoid having to use Obj.magic.
Yes! The database is an association listtheorems, which is 2212 lines
Thanks for explaining the ((asl,w) as g) of tactics.ml, Vince! I now see your
explanation is also in ocaml-4.00-refman.pdf, sec 6.6 Patterns. I know you
told me about your HOL-Light-Q, but you told me not to read it, and you did not
tell me how to get the nonempty environment we need. But
Thanks, Vince! It look like your q.ml and the HOL4 version are both
counterexamples to what I've been posting, that the only place where
retypecheck is used with a nonempty environment is in John Freek's Mizar-like
code. I'm really happy to have been wrong! I can definitely see some
Thanks, Konrad and Mark! I sorta understood what you posted on my own, by
thinking about John Freek's Mizar-like code. And thanks to Vince, as I now
have the type annotation reduction I wanted, using retypecheck code from
Freek's function parse_context_term from Mizarlight/miz2a.ml, which is
Vince, I think you just explained to me that I've been misunderstanding HOL all
along! What I'd been asking about environment and scope of variable sounds now
like the simple fact that HOL allows free variables. I think that means that
FOL is actually quite different than the way
Thanks, Vince! I didn't know this:
Mathematically, a variable is the pair of a name and a type, so if
two variables have the same name and the same type then they're
just the same variable.
But I should have known this, because there are 4 different kinds of terms,
each having a type,
Vince, I solved your parser/preterm/retypecheck exercise to fix my cases, using
this below:
(term_of_preterm o (retypecheck [])) (end_itlist
(fun pt1 pt2 - (Combp (Combp (`;\/`, pt1), pt2))) pretermDisjlist)
But I think it's much simpler to get the parser to produce strings instead of
Thanks, Vince! I think you're saying that the HOL4 Q-module can do type
inference using the goal. I would guess that Petros's IsabelleLight techniques
(which I used for my consider) could also do this goal-powered type inference.
Freek's miz3.ml does much more type inference.
Thanks, Vince! Here's an example of a free variable occurrence in the scope of
a variable binding whose type is not inferred, from
hol_light/Examples/inverse_bug_puzzle_tac.ml. I picked a long proof so you can
clearly see. I apologize is my ML-like terminology isn't correct in HOL:
let
Thanks, Vince! It worked, once I substituted your quotexpander into system.ml
and restarted HOL Light with
ocaml
#use hol.ml;;
Now I can get to work on your exercise. A few questions:
Why didn't my attempt work? Why did I get the error message Exception:
Noparse. from
let parse_qproof
Vince, thanks for fixing my error! This works now:
let parse_qproof s = (fst o parse_preterm o lex o explode) (String.sub s 1
(String.length s - 1));;
Now I get the same output for both
`;1 + 1`;;
and, with your new quotexpander,
`'1 + 1`;;
val it : preterm =
Combp
(Combp (Varp (+,
Thanks, Petros! I hate to be an ingrate, but could you port one of my longer
proofs to IsabelleLight? It might help if you read section 10.1, The bug
puzzle, of the HOL Light tutorial, or
hol_light/Examples/inverse_bug_puzzle_tac.ml. Thanks for telling me about
cases: I'll change the name.
Vince, you recommended replacing the lines
let quotexpander s =
if String.sub s 0 1 = : then
parse_type \^
(String.escaped (String.sub s 1 (String.length s - 1)))^\
else parse_term \^(String.escaped s)^\;;
in system.ml by:
let quotexpander s =
if
Petros, I think this is a pretty good exercise for a novice (unless they use
MESON_TAC[], which solves it instantly):
g `P == (P==Q) == Q`;;
e (REPEAT DISCH_TAC);;
e (FIRST_ASSUM (fun x - FIRST_ASSUM (fun y - ACCEPT_TAC (MP x y;;
I'm still kind of a novice myself, so I tried to
Petros, your code worked great, and I now have consider working the way I
wanted, included below. I couldn't use it for cases, and that's a good place
to try Vincent's quotexpander idea. I put your code into BuildExist, and
borrowed some of Marco Maggesi's HYP ideas to turn a string into a
Thanks, Vincent! I definitely have to work your exercise now. Two dumb
questions:
1) how do I get quotexpander to turn off type inference by putting a period at
the end of the terms? Of all your possibilities, that's the one I like best.
2)Doesn't Ocaml use the applicative order application
Petros, your consider code is a huge step toward what I need. I'll try to
finish modifying your code tonight. Here's the string version I have now, and
below that is an earlier term version:
let consider vars_t prfs lab =
let len = String.length vars_t in
let rec findSuchThat = function
Vincent, you gave me a nice exercise which I'll try to work, but it dawned on
me that we can't use that unless we permanently change the parser. E.g. every
time I use miz3, I have to change the parser for that entire HOL Light session.
The same thing goes for your nice hack of quotexpander:
Freek, can you explain your code miz3.ml in really broad detail? I think
miz3.ml is an amazing accomplishment, but I don't understand it, and much of
what I don't understand involves parsing.
Petros, thanks for your new stuff, which I haven't understood yet. I ran your
code, which works:
Thanks, Vincent, but I really was wrong, I just made an error in describing my
mistake. You're right (and I knew it):
if you just type `1 + 1`, you still get the exception:
My error was thinking that the presence of preterm_of_term would keep `1 + 1`
from being evaluated, and that was
Vince, this is great! May I ask you to learn about miz3? With a little work,
I think miz3.ml can be turned into a general purpose interface for HOL Light,
with much improved readability, with fewer type annotations in particular. The
part of miz3.ml we don't need is what I think is the hard
Thanks, Vincent and Petros! I'll have to study your interesting posts
carefully. A few quick comments:
Petros, it looks like you're doing something that's a whole lot more
interesting than my project. I'm not sure I have the terminology straight:
Suppose we bind a variable x, say with
Thanks, Vincent! Let me be more precise. I want functions that act on terms
that are somewhat like the ocaml function ^ which concatenates strings. I
don't know how to define ^, but I know how to define similar functions on lists
in ocaml. There's a simple example in the official
Thanks, Ramana! You're the person I wanted to talk to. I already had a vague
understand of what you explained (thanks for explaning), but I have a different
question about HOL4:
I'm convinced that the solution to my problem involves camlp (I use
camlp5-6.05), as I can't find anything in the
John Harrison pointed out that my Mizar-like function `consider' and `cases' I
just posted won't work if a string contains /\ followed immediately by a
newline. We see the problem from
# move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y);;
I fixed my Mizar-like function `consider' (see below) using strings, Marco's
DESTRUCT_TAC ideas and Freek's parse_term ideas, and used it to port the HOL
Light tutorial (p 81) readable proof of the irrationality of sqrt 2. I
realized that John's function (p 78) `using' can be thought of
Freek Wiedijk answered a question: string_of_term and then parse_term take
terms to strings and strings to terms. Using parse_term, I made a start
toward Freek's miz3 interface which doesn't use backquotes and require the
extra type annotations. It also uses Marco Maggesi's new
Sounds like good work, Marko! You ought to post your OS, as I think the
Makefile does different things depending on what it detects your OS to be.
--
Best,
Bill
--
Master Visual Studio, SharePoint, SQL, ASP.NET, C#
Marko, Petros Ramana, I use Emacs miz3, with a minimal interface
hol_light/RichterHilbertAxiomGeometry/hol-light-fonts.el
which mostly allows writing HOL Light code with math characters. The Isabelle
folks are phasing out ProofGeneral in favor of jedit. I would like to have
automatic
I think I just learned something about MP_TAC, that these are different:
MP_TAC t THEN MESON_TAC[]
MESON_TAC[t]
This is important to me because of the HOL Light tutorial's Mizar-like
definitions
let by labs tac = MAP_EVERY (fun l - USE_THEN l MP_TAC) labs THEN tac;;
let using ths tac = MAP_EVERY
Marko, as Ramana said, you're having a ocaml/campl5 problem. You didn't say
which HOL Light version you're using. I reccommend the latest subversion.
That might fix the problem. If not, read John Harrison's post
http://sourceforge.net/mailarchive/message.php?msg_id=29268458
You didn't say
Thanks, Ramana! I think I wasn't clear. As Rob explained, there's a type
quantification problem: we can't define Fibration p E B. Any time you wish to
write Fibration p E B, you must write instead
!M:A-bool. HLP p E B M. With that in mind, I don't understand your objection
It's not
Just because you don't write the A doesn't mean it isn't there. And
if you'll still need to be careful if there's an A in context,
whether you write it explicitly or not, although hopefully type
inference will pick another type variable for you if there's
already an A around (e.g.
Ramana and Rob, thanks for telling me about dependent types, which I'd heard
Coq had. I think John Harrison believes that Coq dependent types are really
complicated, so I'm happy with HOL not allowing 3 to have type num in the
vector type real^3, , and instead requiring 3 to be a type. If
In HOL Light vectors, there's something like type quantification, and I thought
that wasn't possible in HOL.
First, I could not find an HOL4 analogue of HOL Light vectors. The basic idea
seems to be that to define the type operator ^ which yields the type real^3
which denotes vectors in R^3,
Thanks, Ramana! I'll try to find Larry's book ($66.30 on Amazon). But since
it's ML code, uh, can't we read the sources and get a pretty good idea? Is
there an Isabelle doc version of this? Thanks for the feedback on my MP_TAC o
SPEC code, which I forgot to say is John's code
Thanks, Ramana! That's very helpful, clarifying DISCH_TAC and explaining
To keep things really simple: thm_tactic is just an abbreviation
for (thm - tactic). That is, a thm_tactic is any function that
takes a theorem and returns a tactic.
Great, I didn't know how to parse the phrase
Thanks, Petros! It will take me a while to digest your post. BTW I was wrong
about the HOL Light reference manual treatment of STRIP_TAC, which is fine.
BTW how does HOL and Informatics fit together?
How do they not? :) They are connected in so many ways...
I think hol-info ought
I guess you've found a bug in the documentation.
Thanks, Michael! I think you're right, because the ref manual makes the same
apparent error:
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html
Given a goal (A,t), STRIP_TAC removes one outermost occurrence of one of the
connectives
Thanks, Petros Michael! I didn't completely understand what you wrote, but I
see how Michael simplified Petros's proof. This is really nice, and I can
probably just modify your code to finish the exercise in footnote 23, p 67 of
the HOL Light tutorial:
let addN = new_definition
`!p p' n.
Thank, Ramana and Petros! Your code looks very helpful, and I'll study it, but
first I want to explain something I did with miz3's `consider' but could not
port to HOL Light, even using the tutorial p 78 Mizar-like `consider'. Here's
a simpler version of the tutorial p 65 `reachable'
let
Petros, I really like your fix of my code, and it's even nicer than Ramana's,
although I need to understand why his CHOOSE_TAC(ASSUME t) works. Your fix
SUBGOAL_THEN `?m. p = 2 * m` CHOOSE_TAC
is especially appealing to me, because you're usage just substitutes CHOOSE_TAC
for ASSUME_TAC, as
I have a question about X_CHOOSE_TAC and another vote for miz3.
In miz3 you can easily define variables with `consider'. The HOL Light
tutorial only explains two ways to define variables, both in proofs (p 73--81)
of the irrationality of sqrt{2}. John's p 78 Mizar-like `consider' is close to
Mark, thanks for explaining my irregular syntax (how do I learn I can't mix
symbolic and alpha-numeric characters?), and that HOL Zero precedence is
similar to HOL Light's. I have a SWAP_FORALL_THM question an a vote for miz3.
I got this tactics proof to work, but I don't know why it does:
Thanks, Mark! This is very cool, and I did not know it:
Milner type inference tells us that type annotations are never needed!
And I don't need type annotations for FunctionSpace! These two results are
fine:
let FunctionSpace = new_definition
`! s t. s --- t = {f | (! x. x IN s == f
Thanks, Mark! Your precedence list explains my code. Why don't we try to
prove your precedence order is correct for HOL Light. Don't we just have to
understand parser.ml? I just realized I don't need type annotations if use
tactics:
let CartesianProduct = new_definition
`! X Y. X times
I'm trying to learn HOL Light by reading the tutorial, and I keep running into
things I don't understand. Maybe it's a good idea to have a thread for the
experts to straighten out beginners like me. Here's my latest problem, about
parenthesis and maybe precedence. I have an improved proof of
I'm sorry, it's the HOL Light tactic DISCH_TAC, not MATCH_MP_TAC, that's much
the same as the way the miz3 thesis changes from
α ⇒ β to β after writing
assume α;
And DISCH_TAC is part of STRIP_TAC, which also includes GEN_TAC, which is much
the same as the way the miz3 thesis changes from
∀
I have a dumb question about interactive HOL Light proofs vs tactics scripts.
I got the impression from p 48 of the tutorial that you can package an
interactive (g e) proof as a tactic script with THEN. But that didn't work
for me. Part of my question is how to debug a tactics script.
Continuing to study whether HOL Light tactics proofs can be ported to miz3, and
if miz3 can explain tactics proofs, I turn to John's inductive proof (p 52 ff)
of the sum of the first n natural numbers. John writes on p 53 The resulting
goal may look like a mess, but I think the problem is just
I ported the HOL Light tutorial's proof of the irrationality of sqrt{2}
(below). The tactics proof of NSQRT_2 (p 75) used the theorems
num_WF, RIGHT_IMP_FORALL_THM, EVEN_MULT, ARITH, EVEN_EXISTS, ARITH_RULE,
LE_MULT2, MULT_EQ_0; ARITH_RULE.
My miz3 port used all these theorems except
John, I'm now certain that your proof of TRIANGLE_ANGLE_SUM_LEMMA is pretty
much what I posted yesterday. I was confused about LAW_OF_COSINES, a vector
triviality which I actually used. Here's a better proof that my son I worked
out today. Which is to say, I gave it to him as a guided
John, I'm finally responding to your Aug 31 post. I lifted a bold, clever
proof of TRIANGLE_ANGLE_SUM in Multivariate/geom.ml, although your actual proof
may be simpler. I ran your code below, and saw the goalstacks, but they didn't
help much, because it's really TRIANGLE_ANGLE_SUM_LEMMA I
John Nicol, you may not need this anymore, but a miz3 tip that I learned from
your CARD exercise. Miz3 solves this immediately:
let notXinterYZ_THM = thm `;
! x y z: A. ~(x = y) /\ ~(x = z) /\ ~(y = z) == {x} INTER {y, z} = {}
by SET_RULE;
`;;
(* But let's try to get rid of the powerful
Thanks for the exercise, John! Konrad's tips were very helpful, and here's a
awkward-looking miz3 solution below (using the default timeout of 1). As
Konrad said, this is really an exercise in sets.ml, and CARD is a part of
sets.ml I didn't know anything about. Miz3Tips, which as you noted
Thanks, John! Here's a better version of my miz3 code and an exercise for you.
I think Konrad gave you excellent advice, especially considering that HOL4
does not yet have anything like miz3. I thought Konrad said that writing
declarative proofs in miz3 is a very good way to actually learn
Thanks for correcting my typed LC, Ramana: no Y combinator (that makes sense,
as Y sorta comes from Russell's paradox, which typing was designed to prevent),
and it's simply typed LC. My heavy was just slang, and generated is from
Hales's Notices article. Maybe I wasn't clear about syntax and
1 - 100 of 223 matches
Mail list logo
