Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Assignment 9
Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 9
For what natural number k is the predicate least(k) provable? Don't produce a machine-checked proof of this, or even a formal handwritten proof, but just give an informal explanation of why I should believe your value of k. You should explain how each clause of the prop predicate is relevant to answer. On this assignment you can work in pairs, if you find it helpful to have someone to discuss ideas with. 
inverse = exists [inv] forall [x] neq x zero imp eq (times X (inv @ X)) one.
supremum = 
 forall [s]
  (exists [x] s @ x) imp
  (exists [m] forall [x] s @ x imp leq x m) imp
  (exists [m] (forall [x] s @ x imp leq x m) and
              (forall [m'] (forall [x] S @ x imp leq x m') imp leq m m')).
it's_the_real_numbers = inverse and supremum.      

sqr: tm (num arrow num) = lam [X] times X X.

limit: tm ((num arrow num) arrow num arrow form) =
 lam2 [s][v]
   forall [epsilon] gt epsilon zero imp 
      exists [n] isNat n and
         forall [i] isNat i imp 
          gt i n imp lt (sqr @ (minus v (s @ i))) epsilon.

continuous: tm ((num arrow num) arrow form) =
  lam [f] forall2 [s][v] limit @ s @ v imp 
                          limit @ (lam [i] f @ (s @ i)) @ (f @ v).

bounded = lam [f] exists [n] isNat n and forall [x] lt (sqr @ (f @ x)) n.

inrange: tm (num arrow num arrow form) =
  lam2 [n][i] isInt i and geq i zero and lt i n.

prop: tm (num arrow form) =
 lam [k]  isNat k  and  it's_the_real_numbers and
 forall3 [n][f][g] exists [c]
 (isNat n and 
  (forall [i] continuous @ (f @ i) and bounded @ (f @ i) and 
              continuous @ (g @ i) and bounded @ (g @ i))  and
  (forall4 [i][j][t1][t2] 
   inrange @ n @ i and inrange @ n @ j and
   not (eq i j) and 
   lt zero t1 and lt t1 one and
   leq zero t2 and leq t2 one  and
   not(eq (f @ i @ zero) (f @ i @ one) and eq (g @ i @ zero) (g @ i @ one)) and
   not(eq (f @ i @ t1) (f @ j @ t2) and eq (g @ i @ t1) (g @ j @ t2))))  imp
  ((forall2 [x][y] inrange @ k @ (c @ x @ y)) and
   (forall [i] inrange @ n @ i imp 
		 not (eq (c @ (f @ i @ zero) @ (g @ i @ zero))
			 (c @ (f @ i @ one) @ (g @ i @ one))))).
  
least: tm (num arrow form) =
  lam [k] prop @ k and forall [j] prop @ j imp geq j k.

Hints:

In all cases, names of predicates used in this assignment are not meant to mislead. That is, predicates such as continuous, bounded, etc. are intended to do what the names imply.

The coreTCB object logic that we have been using contains an incomplete axiomatization of arithmetic. Models of num include the integers, the rationals, and the reals: that is, our axioms don't rule out any of these models. But for this puzzle I want the real numbers. The predicates inverse and supremum are part of a standard axiomatization of the reals (see Section 2.1 of Theorem Proving with the Real Numbers, by John Harrison, Springer 1998). By asserting it's_the_real_numbers in prop, we state that this property (only) holds in models where num is the reals. If you are willing to accept this claim, then you can ignore the details of the supremum formula, and just use your intuitive understanding of the real numbers.

Similarly, the predicate limit is used only to define the predicate continuous, which is a definition of what it is to be a continuous function. If you think you understand what a continuous function is, then you can ignore the details of the limit predicate.

What to turn in

You should turn in one hand-written page, containing:
  1. The number k
  2. A 5-to-10 word short explanation why this number
  3. Some diagrams, illustrating what the different subformulas in the "prop" predicate actually do. The diagrams might, for example, be 2-dimensional geometric figures of some sort. That's a hint.

Extra credit

Turn in a machine-checked proof, 
the_answer: tm num = const (...).
theorem: pf (least @ the_answer) = ...