[FOM] Formal verification

[Freek Wiedijk]

Dear Lasse,

>Here is a very simple statement which I often give to
>students as a first exercise in iteration, and to practice
>formal mathematics.
>
>***
>Let f be a real-valued function on the real line,
>such that f(x)>x for all x.  Let x_0 be a real number,
>and define the sequence (x_n) recursively by
>x_{n+1} := f(x_n).  Then x_n diverges to infinity.
>***

You missed the condition that f has to be continuous.
So formalizing it uncovered an error... :-)

>A standard proof might go along the following steps:
>1) By assumption, the sequence is strictly increasing;
>2) hence the sequence either diverges to infinity or has a
>finite limit; 3) by continuity, any finite limit would have
>to be a fixed point of f, hence the latter cannot occur.
>
>What effort would be required to formalize this kind of
>statement using current technology?

It's not hard.  I'm very much not proficient at HOL Light,
but with some struggling and studying the HOL Light libraries
whipped together the following proof script:

let LASSE = prove
 (`(!x. f contl x) /\ (!x. f x > x) /\ (!n. x (n + 1) = f (x n)) ==>
   !y. ?n. x n > y`,
  REWRITE_TAC[real_gt] THEN STRIP_TAC THEN
  SUBGOAL_THEN `mono x` ASSUME_TAC THENL
  [ASM_REWRITE_TAC[MONO_SUC; ADD1; real_ge; REAL_LE_LT]; ALL_TAC] THEN
  ASM_CASES_TAC `convergent x` THENL
  [POP_ASSUM MP_TAC THEN REWRITE_TAC[convergent] THEN STRIP_TAC THEN
   SUBGOAL_THEN `(\n. x n) tends_num_real (f:real->real) l`
     (ASSUME_TAC o REWRITE_RULE[ETA_AX]) THENL
   [ONCE_REWRITE_TAC[SEQ_SUC] THEN ASM_SIMP_TAC[ADD1; CONTL_SEQ]
   ;ALL_TAC] THEN
   ASM_MESON_TAC[SEQ_UNIQ; REAL_LT_REFL]
  ;SUBGOAL_THEN `~bounded (mr1,(>=)) (x:num->real)` ASSUME_TAC THENL
   [ASM_MESON_TAC[SEQ_BCONV]; ALL_TAC] THEN
   SUBGOAL_THEN `!y y'. ?n. ~(y <= (x:num->real) n) \/ ~(x n <= y')`
     (ASSUME_TAC o REWRITE_RULE[REAL_NOT_LE]) THENL
   [ASM_MESON_TAC[SEQ_BOUNDED_2]; ALL_TAC] THEN
   REWRITE_TAC[FORALL_NOT_THM; EXISTS_NOT_THM] THEN
   SUBGOAL_THEN `~ ?y. !n. ~(y < (x:num->real) n)`
     (fun th -> MESON_TAC[th]) THEN
   DISCH_THEN (CHOOSE_THEN ASSUME_TAC) THEN
   SUBGOAL_THEN `!n. x 0 <= x n` ASSUME_TAC THENL
   [INDUCT_TAC THENL [ARITH_TAC
    ;ASM_REWRITE_TAC[ADD1] THEN REWRITE_TAC[REAL_LE_LT] THEN
     DISJ1_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
     EXISTS_TAC `x (n:num):real` THEN ASM_REWRITE_TAC[]]
    ;FIRST_ASSUM (fun th -> STRIP_ASSUME_TAC
       (SPECL [`x 0:real`; `y:real`] th)) THENL
     [ASM_MESON_TAC[real_le] ;ASM_MESON_TAC[]]]]);;

(If John Harrison would prove this, it probably would be
twice as short :-))  Note that I have two different usages
of x in here: as reals and as sequences (I could have used
"x_" for the sequence, but that would look weird too).
Also note that I couldn't find a notation for "diverges
to infinity" (maybe it's there and I just missed it).
Finally note that this version doesn't make the point that
the sequence x is defined from f by recursion.

My main obstacle when doing this was that the libraries only
give the relation between being bounded and being convergent
for _two sided_ boundedness.  For that reason it was not
hard to derive that the sequence x couldn't stay bounded.
But to get from that the fact that it diverged to _plus
infinity_ took a bit more effort (I needed to show by
induction that f x > f 0 for all x).

Yes, I know, HOL Light proof scripts look like unreadable
gibberish.  Maybe I'll write a declarative version too,
as a comparison.

Freek