|
|
HolLightDemo1
#John Harrison on using HOL Light
Video Presentation
John Harrison gives a video demonstration of how to use HOL Light. The presentation lasts about 30 minutes, followed by questions and answers.
The theorem that he proves is a problem on an old international math olympiad (IMO).
IMO problem and solution
The IMO problem and solution discussed by Harrison is the following.
Problem [B2 from IMO 1972] f and g are real-valued functions defined on the real line. For all x and y, f(x + y) + f(x - y) = 2 f(x) g(y). f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x. Solution Let k be the least upper bound for |f(x)|. Suppose |g(y)| > 1. Then 2k ≥ |f(x + y)| + |f(x - y)| ≥ |f(x + y) + f(x - y)| = 2 |g(y)||f(x)|, so |f(x)| ≤ k/|g(y)|. In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. Contradiction.
Here is the pdf solution, and a second pdf solution.
HOL Light solution
The video demo shows the steps he used to create the following proof, written by Harrison. The first part is what he did during the video demo. The second version is another proof of the same theorem he did later. It is not part of the demo. After the code, I give a line-by-line commentary on the code.
As the video and the commentary show, it is hard to read the code just by looking at it. To understand it, you "replay" it on the computer step by step.
(* ------------------------------------------------------------------------- *)
(* Cleaned-up proof from session. *)
(* ------------------------------------------------------------------------- *)
needs "Multivariate/misc.ml";;
let IMO = prove
(`!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
~(!x. f(x) = &0) /\
(!x. abs(f(x)) <= &1)
==> !x. abs(g(x)) <= &1`,
let LL = REAL_ARITH `&1 < k ==> &0 < k` in
REPEAT STRIP_TAC THEN SPEC_TAC(`x:real`,`y:real`) THEN
ABBREV_TAC `k = sup (IMAGE (\x. abs(f(x))) (:real))` THEN
MP_TAC(SPEC `IMAGE (\x. abs(f(x))) (:real)` SUP) THEN
ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV] THEN
ANTS_TAC THENL [ASM SET_TAC[]; STRIP_TAC] THEN
SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `k / abs(g(y:real))`) THEN
SIMP_TAC[NOT_IMP; NOT_FORALL_THM] THEN CONJ_TAC THENL
[ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL;
REAL_ARITH `u + v = &2 * z /\ abs u <= k /\ abs v <= k ==> abs z <= k`];
ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL; REAL_MUL_RID; LL;
REAL_ARITH `~(z = &0) /\ abs z <= k ==> &0 < k`]]);;
(* ------------------------------------------------------------------------- *)
(* second proof. *)
(* ------------------------------------------------------------------------- *)
let LEMMA1 = prove
(`(!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\ (!x. abs(f x) <= &1)
==> !l x. abs(f x * (g y) pow l) <= &1`,
DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN INDUCT_TAC THEN
ASM_SIMP_TAC[real_pow; REAL_MUL_RID] THEN GEN_TAC THEN MATCH_MP_TAC
(REAL_ARITH `abs((&2 * a * b) * c) <= &2 ==> abs(a * b * c) <= &1`) THEN
ASM_SIMP_TAC[] THEN FIRST_ASSUM(MP_TAC o SPEC `x + y`) THEN
FIRST_ASSUM(MP_TAC o SPEC `x - y`) THEN REAL_ARITH_TAC);;
let LEMMA2 = prove
(`~(x = &0) /\ &1 < abs(y) ==> ?n. &1 < abs(y pow n * x)`,
SIMP_TAC[REAL_ABS_MUL; REAL_ABS_POW; GSYM REAL_LT_LDIV_EQ;
GSYM REAL_ABS_NZ; REAL_ARCH_POW]);;
let IMO = prove
(`!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
~(!x. f(x) = &0) /\
(!x. abs(f(x)) <= &1)
==> !x. abs(g(x)) <= &1`,
MESON_TAC[LEMMA1; LEMMA2; REAL_NOT_LE; REAL_MUL_SYM]);;
Commentary
This gives a step by step commentary on Harrison's proof. After seeing the details, you will see how much has been packed into a few lines of computer code. It is really remarkable that Harrison was able to work out the details of this formal proof in about 30 minutes.
To get started, install CAML and HOL Light on your machine, following the instructions on page 5 of the tutorial. It runs on most computers.
Start a session of CAML. Load HOL Light.
Step 0. Understand the conventional Proof
Every formal proof starts with a conventional proof (that is, non-formal proof). We should study the conventional math proof of the IMO problem (given above) and understand it thoroughly. With a thorough understanding of the conventional proof, we are ready to move on.
Step 1. Load theorems
needs ---- prioritize_real
The first step of the proof is
needs "Multivariate/misc.ml";;
In his proof of the IMO problem, Harrison uses some theorems that have already been proved in the file "Multivariate/misc.ml". This line tells the theorem prover to load those theorems.
Harrison doesn't include the following step, but I add it, to tell the theorem prover that I am working with the real numbers in this problem, rather than the natural numbers. Otherwise, HOL Light might think x and y are natural numbers.
prioritize_real();;
Step 2. State the theorem to be proved.
The statement of the problem
f and g are real-valued functions defined on the real line. For all x and y, f(x + y) + f(x - y) = 2 f(x) g(y). f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x.
appears in HOL Light as follows:
let IMO = prove
(`!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
~(!x. f(x) = &0) /\
(!x. abs(f(x)) <= &1)
==> !x. abs(g(x)) <= &1`, (* TACTIC HERE *) );;The notation is explained in the HOL Light tutorial. Real numbers need to be marked with &. For instance, &0 is the real number zero (as opposed to the natural number zero 0). The logical symbol "and" is typed as /\, "less than or equal" appears as <=, "the absolute value" as abs. It is necessary to learn the names of different functions from the tutorial.
The function prove takes two arguments, a backquoted string giving the result that is to be proved, and a tactic that gives the proof. The prove function is used after the proof is complete to package the proof into something that can be used by other people. When the proof is being worked out, the desired theorem is stated as a goal. For this, type g for goal and then the backquoted string.
g `!f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
~(!x. f(x) = &0) /\
(!x. abs(f(x)) <= &1)
==> !x. abs(g(x)) <= &1`;;Step 3. Work out proof tactics
The style of proving in HOL Light is generally "backwards". This means that you start out with a goal of what you want to prove (in this case the IMO problem), and work backwards until you have reduced the goal to easier statements that are easy to prove. Each backwards step of the proof is called a tactic. If you look at the HOL Light proof of the IMO problem, it has the general form
let IMO = prove ( (* backquoted goal *) , (* tactic *) );;
The tactic, if you look carefully, is a long sequence of separate commands joined together with THEN. The THEN function makes a single tactic out of many tactics. For example, if we have three backwards proof steps called tactic1, tactic2, and tactic3, we can create a single tactic by writing
let combined_tactic = tactic1 THEN tactic2 THEN tactic3;;
You join the tactics together into a single tactic after you have finished the proof and want to package the proof into something that other people can use. When you are writing down the HOL Light proof for the first time, you don't need to use THEN to join the tactics together. Wait until you have finished working out the formal proof.
So for now, we ignore the THEN s and go through the separate tactics of the proof.
First Line
let LL = REAL_ARITH `&1 < k ==> &0 < k`
HOL Light has some powerful automated theorem proving functions built into it. One of them is called REAL_ARITH. It takes simple (backquoted) statements about the real numbers and automatically turns them into theorems. In this proof, we will later need the simple fact that "if 1 < k then 0 < k". Harrison starts the IMO proof with an automated proof of this result and gives this theorem the name LL for future reference.
REAL_ARITH is something that you learn in Harrison's HOL Light tutorial.
First Tactic
REPEAT STRIP_TAC
REPEAT ---- STRIP_TAC ---- GEN_TAC ---- e
The first thing we want to do in the proof is to get rid of the the "for all f and g" (written as !f g.) at the beginning of the goal. STRIP_TAC or GEN_TAC gets rid of the "for all". GEN_TAC only gets rid of the quantifier !f, but STRIP_TAC goes farther in breaking down ==>, ~, and /\. Since we have two foralls, we want to repeat this command. If you write REPEAT before a tactic, that tactic gets repeated as many times as possible.
You can learn about the different tactics such as STRIP_TAC from the following sources.
- tactics one line summary of each tactic.
- Type help "STRIP_TAC" in HOL Light to get the documentation on that tactic.
- web index gives full documentation of each tactic.
What we actually type into the system is this: e (REPEAT STRIP_TAC);; The result is that the goal has been simplified into the following form:
val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] `abs (g x) <= &1`
Not only did STRIP_TAC get rid of the quantifiers, but it moved the different assumptions into the assumption list, each on a separate line. Many proofs start with REPEAT STRIP_TAC as the first tactic. It is a convenient way to begin.
Next Tactic
SPEC_TAC(`x:real`,`y:real`)
SPEC_TAC works in the opposite direction as GEN_TAC. The last step, which we repeated as many times as possible, took away one quantifier too many. We put it back, renaming the variable x as y. Look at how the tactic changes the goal:
# e (SPEC_TAC(`x:real`,`y:real`));; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] `!y. abs (g y) <= &1`
Next Tactic
ABBREV_TAC `k = sup (IMAGE (\x. abs(f(x))) (:real))`
Until now, we have just been moving things around, without really working on the proof. The text proof starts with the statement: "Let k be the least upper bound for |f(x)|." This tactic implements this line of text by defining k to be an abbreviation for the sup of |f(x)|. We need to state this more precisely than it is done in the text. In HOL Light the function that takes x to abs(f(x)) is written in lambda notation as \x. abs(f(x)). (The backslash \ is HOL Light notation for the Greek letter lambda.) We then take the image of that function, which is a subset of the real numbers, and then the supremum of that set. The functions sup, IMAGE, and abs are all part of the standard HOL Light library. When we run this line of code, we see that it adds a new assumption, giving the definition of k:
# e ( ABBREV_TAC `k = sup (IMAGE (\x. abs(f(x))) (:real))` );; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] `!y. abs (g y) <= &1`
Next Tactic
MP_TAC(SPEC `IMAGE (\x. abs(f(x))) (:real)` SUP)
We have defined k to be the sup of a set, but we need to quote a theorem that tells us about the properties of sup. The theorem SUP says that if we have a nonempty set of real numbers bounded from above, then every element in that set is at most the sup, and it is the smallest number with that property. Here is the formal statement. (The symbol ? means "there exists", and IN is for set membership.)
# SUP;;
val it : thm =
|- !s. ~(s = {}) /\ (?b. !x. x IN s ==> x <= b)
==> (!x. x IN s ==> x <= sup s) /\
(!b. (!x. x IN s ==> x <= b) ==> sup s <= b)We want to apply this theorem for a specific value of s. We want to let s be the set IMAGE (\x. abs(f(x))) used in the definition of k. The command SPEC specializes a theorem. This is what we get. It looks much more complicated, but it is exactly the same theorem with IMAGE (...) substituted for each s.
# SPEC `IMAGE (\x. abs(f(x))) (:real)` SUP;;
val it : thm =
|- ~(IMAGE (\x. abs (f x)) (:real) = {}) /\
(?b. !x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
==> (!x. x IN IMAGE (\x. abs (f x)) (:real)
==> x <= sup (IMAGE (\x. abs (f x)) (:real))) /\
(!b. (!x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
==> sup (IMAGE (\x. abs (f x)) (:real)) <= b)The MP_TAC changes the goal from something of the form Q to something of the form P ==> Q, where P is a known theorem. We want to insert this big messy theorem for P.
When we run this tactic, the goal looks much more complicated. But actually, it has changed in a simple way. Note that the new goal has the form P ==> Q where P is the messy theorem we created out of SUP and Q is the old goal. The hypotheses have not changed.
# e ( MP_TAC(SPEC `IMAGE (\x. abs(f(x))) (:real)` SUP) );;
val it : goalstack = 1 subgoal (1 total)
0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`]
1 [`~(!x. f x = &0)`]
2 [`!x. abs (f x) <= &1`]
3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`]
`(~(IMAGE (\x. abs (f x)) (:real) = {}) /\
(?b. !x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
==> (!x. x IN IMAGE (\x. abs (f x)) (:real)
==> x <= sup (IMAGE (\x. abs (f x)) (:real))) /\
(!b. (!x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
==> sup (IMAGE (\x. abs (f x)) (:real)) <= b))
==> (!y. abs (g y) <= &1)`The next tactic will simplify things again.
Next Tactic
ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV] )
The tactic ASM_SIMP_TAC is a simplification tactic, using the assumption list and whatever other theorems you give it. In this case, we use three other theorems. This is what those theorems say.
# FORALL_IN_IMAGE;; val it : thm = |- !f s. (!y. y IN IMAGE f s ==> P y) <=> (!x. x IN s ==> P (f x)) # EXISTS_IN_IMAGE;; val it : thm = |- !f s. (?y. y IN IMAGE f s /\ P y) <=> (?x. x IN s /\ P (f x)) # IN_UNIV;; val it : thm = |- !x. x IN (:A)
Let's look at how this tactic changes the goal:
# e ( ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV] );;
val it : goalstack = 1 subgoal (1 total)
0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`]
1 [`~(!x. f x = &0)`]
2 [`!x. abs (f x) <= &1`]
3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`]
`(~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b)
==> (!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b))
==> (!y. abs (g y) <= &1)`This has simplified the goal considerably. We see that the definition of k in the assumption list has been substituted into the goal for the messy sup (...). From FORALL_IN_IMAGE, EXISTS_IN_IMAGE, every term in the goal of the form x IN IMAGE has been replaced with with a simpler expression. The theorem IN_UNIV doesn't do much; it says that every real number is IN the set of real numbers.
Next Tactic
ANTS_TAC
We can only use the properties of the sup of a set X when we know that X is nonempty and bounded. The current goal lists those two things as hypotheses. We need to prove a separate goal that shows that X is nonempty and bounded. The tactic ANTS_TAC breaks things down into two subgoals:
# e ( ANTS_TAC );;
val it : goalstack = 2 subgoals (2 total)
0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`]
1 [`~(!x. f x = &0)`]
2 [`!x. abs (f x) <= &1`]
3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`]
`(!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b)
==> (!y. abs (g y) <= &1)`
0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`]
1 [`~(!x. f x = &0)`]
2 [`!x. abs (f x) <= &1`]
3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`]
`~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b)`New Tactic
[ [ASM SET_TAC[]; STRIP_TAC]
ASM ---- SET_TAC ---- STRIP_TAC ---- THENL
In this step, Harrison connects the tactics with THENL rather than THEN and gives a list of tactics after THENL. He does this because we have two goals. When we use THENL instead of THEN, the tactics that follow get applied to all the different subgoals at once. I consider this an advanced technique. It means that when we use it, we are proving two different results at once, using a single command. Harrison uses this technique very effectively. In this commentary, I will work on a single subgoal at a time.
SET_TAC is a powerful tactic that proves many simple results about sets (unions and intersections and so forth). We use it here to prove that our set X is nonempty. (The image of the real numbers under any function is nonempty.) We also, have assumption list number 2, which says that abs(f x) <= &1 for all x. This is exactly what we need to show that it is bounded. The tactic ASM SET_TAC[] uses the set tactic and the assumption list to prove that X is nonempty and bounded. It solves the subgoal. We are now back to a single goal.
# e(ASM SET_TAC[]);; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] `(!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b) ==> (!y. abs (g y) <= &1)`
We have already discussed what STRIP_TAC does. It moves the antecedent in the goal down to the assumption list. We are up to five assumptions. We now have a long list of assumptions (which is good) and a rather easy goal (which is also good).
# e(STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`!b. (!x. abs (f x) <= b) ==> k <= b`] `!y. abs (g y) <= &1`
New Tactic
SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM]
STRIP_TAC
We are ready to move to the next statement "Suppose |g(y)| > 1" of the text proof. This step sets up the proof by contradiction. Our goal is to prove !y. abs (g y) <= &1 and we say, suppose for a contradiction that there is a real number that does not satisfy this inequality.
GSYM takes a theorem a = b and replaces it with b=a. The reason that we need to change the order is that the simplification tactic looks in the goal for something that looks like the left-hand side, and replaces it with the right-hand side. This is how GSYM transforms the theorem REAL_NOT_LT. See how the left and right hand sides have been swapped:
# REAL_NOT_LT;; val it : thm = |- !x y. ~(x < y) <=> y <= x # GSYM REAL_NOT_LT;; val it : thm = |- !x y. y <= x <=> ~(x < y)
Another example:
# NOT_EXISTS_THM;; val it : thm = |- !P. ~(?x. P x) <=> (!x. ~P x) # GSYM NOT_EXISTS_THM;; val it : thm = |- !P. (!x. ~P x) <=> ~(?x. P x)
The tactic SIMP_TAC is similar to ASM_SIMP_TAC, which we have used already. The difference is that SIMP_TAC is not going to use anything from the assumption list. It will only use the theorems we give it. In this case, we use two theorems. Since we currently have abs(g y) <= &1 in the goal, we can transform it with GSYM REAL_NOT_LT (but REAL_NOT_LT would have no effect).
# e ( SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM] );; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`!b. (!x. abs (f x) <= b) ==> k <= b`] `~(?y. &1 < abs (g y))`
We have already discussed STRIP_TAC. It moves the negated down to the hypothesis list and finishes setting up the proof by contradiction. We are up to six assumptions. Notice that STRIP_TAC also gets rid of the existential quantifier on y.
# e(STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`!b. (!x. abs (f x) <= b) ==> k <= b`] 6 [`&1 < abs (g y)`] `F`
New Tactic
FIRST_X_ASSUM(MP_TAC o SPEC `k / abs(g(y:real))`)
FIRST_X_ASSUM ---- MP_TAC ---- SPEC ---- o
We are going to work backwards in the proof. The last statement of the text reads "In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. Contradiction." In this step we say it is enough to show that the assumption that k/|g(y)| is an upper bound leads to a contradiction." To do that, we specialize Assumption 5 (which states the least upper bound property for k) with k/|g(y)| as the upper bound. Then we move this assumption up to the main goal.
We have already seen that SPEC is used to specialize an assumption. We have also see that MP_TAC takes a theorem P and a goal Q and create a new goal P ==> Q. However, in this case, we want P to be Assumption 5, rather than a theorem. If we were working with a theorem th rather than the assumption list, the correct tactic would be MP_TAC (SPEC `k/abs(g(y:real))` th).
What we want to do is transform this tactic into another tactic that looks through the assumption list one by one (starting with the highest numbered one first) for a theorem that can be used. The command that transforms a tactic that uses a theorem into a tactic that uses the assumption list is FIRST_X_ASSUM. First it tries to use Assumption 6, but that assumption cannot be specialized (it does not have a universal quantifier). Then it tries Assumption 5, and it works. So it specializes that assumption and uses MP_TAC to bring it out of the assumption list into the goal:
# e ( FIRST_X_ASSUM(MP_TAC o SPEC `k / abs(g(y:real))`) );; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`&1 < abs (g y)`] `((!x. abs (f x) <= k / abs (g y)) ==> k <= k / abs (g y)) ==> F`
New Tactic
SIMP_TAC[NOT_IMP; NOT_FORALL_THM]
This step is a rather basic simplification of the goal using the following two theorems.
# NOT_IMP;; val it : thm = |- !t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2 # NOT_FORALL_THM;; val it : thm = |- !P. ~(!x. P x) <=> (?x. ~P x)
We simply express the goal in a logically equivalent way that no longer involves proving a contradiction:
# e ( SIMP_TAC[NOT_IMP; NOT_FORALL_THM] );; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`&1 < abs (g y)`] `(!x. abs (f x) <= k / abs (g y)) /\ ~(k <= k / abs (g y))`
New Tactic
CONJ_TAC
The goal has the form a /\ b. We use the conjunction tactic to break it into two subgoals a and b:
# e ( CONJ_TAC );; val it : goalstack = 2 subgoals (2 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`&1 < abs (g y)`] `~(k <= k / abs (g y))` 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`&1 < abs (g y)`] `!x. abs (f x) <= k / abs (g y)`
New Tactic
ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL; REAL_ARITH `u + v = &2 * z /\ abs u <= k /\ abs v <= k ==> abs z <= k`];
ASM_MESON_TAC ---- REAL_ARITH
We can quickly treat the third sentence of the text proof: "Then 2k ≥ |f(x + y)| + |f(x - y)| ≥ |f(x + y) + f(x - y)| = 2 |g(y)||f(x)|, so |f(x)| ≤ k/|g(y)|."
In fact, the rest of the proof just follows from basic real arithmetic. We will treat the two remaining goals one at a time. We have already discussed REAL_ARITH, which proves basic statements about real arithmetic. Harrison has it prove u + v = &2 * z /\ abs u <= k /\ abs v <= k ==> abs z <= k. Notice that the conclusion of this statement is exactly in the form of the goal (after we multiply through by abs(g y) and the hypotheses of this statement are in the form of the Assumptions 1, 4 (used twice). Thus, all it takes is a bit of logic and a few simple theorems about real numbers to solve the goal from the assumption list. The tactic ASM_MESON_TAC uses logic, the assumption list, and the list of theorems that follows it to solve a goal completely. It is one of the most powerful tactics in HOL Light.
Here are the theorems we use. (The theorem LL was the first line of the proof.)
# REAL_LE_RDIV_EQ;; val it : thm = |- !x y z. &0 < z ==> (x <= y / z <=> x * z <= y) # REAL_ABS_MUL;; val it : thm = |- !x y. abs (x * y) = abs x * abs y
We are now down to a single goal again:
# e(ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL; REAL_ARITH `u + v = &2 * z /\ abs u <= k /\ abs v <= k ==> abs z <= k`]);; val it : goalstack = 1 subgoal (1 total) 0 [`!x y. f (x + y) + f (x - y) = &2 * f x * g y`] 1 [`~(!x. f x = &0)`] 2 [`!x. abs (f x) <= &1`] 3 [`sup (IMAGE (\x. abs (f x)) (:real)) = k`] 4 [`!x. abs (f x) <= k`] 5 [`&1 < abs (g y)`] `~(k <= k / abs (g y))`
Final Tactic
ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL; REAL_MUL_RID; LL; REAL_ARITH `~(z = &0) /\ abs z <= k ==> &0 < k`]
ASM_MESON_TAC ---- REAL_ARITH
This step is similar to the previous step. We use REAL_ARITH to prove a simple statement in real arithmetic that connects the facts of the assumption list to the goal. Then we use the powerful ASM_MESON_TAC to apply logic, the assumption list, and a few theorems about real numbers to finish off the goal.
Here are the basic facts about real numbers that get used:
# REAL_LE_RDIV_EQ;; val it : thm = |- !x y z. &0 < z ==> (x <= y / z <=> x * z <= y) # REAL_ABS_MUL;; val it : thm = |- !x y. abs (x * y) = abs x * abs y # REAL_NOT_LE;; val it : thm = |- !x y. ~(x <= y) <=> y < x # REAL_LT_LDIV_EQ;; val it : thm = |- !x y z. &0 < z ==> (x / z < y <=> x < y * z) # REAL_LT_LMUL;; val it : thm = |- !x y z. &0 < x /\ y < z ==> x * y < x * z # REAL_MUL_RID;; val it : thm = |- !x. x * &1 = x
This step completes the proof of the IMO problem:
# e(ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL; REAL_MUL_RID; LL; REAL_ARITH `~(z = &0) /\ abs z <= k ==> &0 < k`]);; val it : goalstack = No subgoals
We are done!
Exercise
Work through Harrison's second solution of the IMO problem in the same way. Replay each step inside HOL Light to see how it changes the goal and assumption list. Look up each tactic that you do not understand in the master index.
After you have gone through a few formal proofs in this way, many of the tactics will become familiar, and you will be ready to formalize your own theorems.
Further reading
More details about this demo here.
Sign in to add a comment