[FOM] Formal verification

[Harvey Friedman]

Dear Freek,

This is, of course, a totally unacceptable ugly piece of disgusting
garbage (smile), according to any current standards of mathematical
practice. But I remember reading that there has been some reasonably
successful work on producing nice output. (I was involved in some
early stage in that). Perhaps FOM readers need to be reminded of some
references for creating nice output?

Incidentally, this is a kind of beautiful example, I think just meaty
enough to be interesting.

CHALLENGE: Use this example to create a new field of *micro proof
theory*, whereby new kinds of subtle quantitative and possibly
qualitative features of actual mathematical proofs are investigated,
those which correspond to important features of actual mathematical
proofs that are immediately recognized as interesting and significant
by those reflecting on actual mathematical practice.

Harvey Friedman

On Wed, Oct 22, 2014 at 2:37 PM, Freek Wiedijk <freek at cs.ru.nl> wrote:
> Dear Lasse,
>
> As a followup, here is this same thing
>
>>***
>>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.
>>***
>
> formalized using my declarative miz3 language for HOL Light
> (to be run with "horizon := -1;;").
>
>   let LASSE = thm `;
>     let f be real->real;
>     assume !x. f contl x;
>     assume !x. f x > x;
>     let x be num->real;
>     assume !n. x (n + 1) = f (x n);
>     thus !y. ?n. x n > y
>     proof
>       mono x by MONO_SUC,ADD1,REAL_LE_LT,real_ge,real_gt;
>       cases;
>       suppose convergent x;
>         consider l such that x tends_num_real l by convergent;
>         (\n. x n) tends_num_real f l
>         proof
>           (\n. x (SUC n)) = (\n. f (x n)) by ADD1,REWRITE_TAC;
>           (\n. (\n. x n) (SUC n)) tends_num_real f l by CONTL_SEQ;
>         qed by ONCE_REWRITE_TAC[SEQ_SUC] from -;
>         x = (\n. x n) by ETA_AX;
>       qed by SEQ_UNIQ,REAL_LT_REFL,real_gt;
>       suppose ~convergent x;
>         !n. x 0 <= x n
>         proof
>           x 0 <= x 0 [1];
>           now [2] let n be num;
>             assume x 0 <= x n;
>             thus x 0 <= x (SUC n)
>               by ADD1,REAL_LET_TRANS,REAL_LE_LT,real_gt;
>           end;
>         qed by INDUCT_TAC from 1,2;
>       qed by SEQ_BCONV,SEQ_BOUNDED_2,real_le,real_gt;
>     end`;;
>
> So this uses 13 lemmas from the library (ADD1, CONTL_SEQ,
> ETA_AX, MONO_SUC, real_ge, real_gt, REAL_LE_LT,
> REAL_LET_TRANS, REAL_LT_REFL, SEQ_BCONV, SEQ_BOUNDED_2,
> SEQ_SUC and SEQ_UNIQ), of which about half are just for
> moving between SUC n and n + 1, and between <, >, <=, etc.
> Statements of some of the more meaningful lemmas are:
>
>   MONO_SUC;;
>     !f. mono f <=> (!n. f (SUC n) >= f n) \/ (!n. f (SUC n) <= f n)
>   CONTL_SEQ
>     !f x l.
>         f contl l /\ x tends_num_real l ==> (\n. f (x n)) tends_num_real f l
>   SEQ_BCONV
>     !f. bounded (mr1,(>=)) f /\ mono f ==> convergent f
>   SEQ_BOUNDED_2;;
>     !f k K. (!n. k <= f n /\ f n <= K) ==> bounded (mr1,(>=)) f
>   SEQ_SUC
>     !f l. f tends_num_real l <=> (\n. f (SUC n)) tends_num_real l