miz3/Samples/forster.ml

   1 (* ======== translation of "The shortest?" from Examples/forster.ml ======== *)
   2
   3 horizon := 0;;
   4
   5 let FORSTER_PUZZLE_1 = thm `;
   6   let f be num->num;
   7   thus (!n. f(n + 1) > f(f(n))) ==> !n. f(n) = n
   8   proof
   9     assume !n. f(n + 1) > f(f(n));
  10     !n. f(f(n)) < f(SUC n) [1] by -,GT,ADD1;
  11     !m n. m <= f(n + m) [2]
  12     proof
  13       !n. 0 <= f(n + 0) [3] by LE_0,ADD_CLAUSES,LE_SUC_LT;
  14       now let m be num;
  15         assume !n. m <= f(n + m);
  16         !n. m < f(SUC (n + m)) by -,1,LET_TRANS,SUB_ADD;
  17         thus !n. SUC m <= f(n + SUC m) by -,LE_0,ADD_CLAUSES,LE_SUC_LT;
  18       end;
  19     qed by INDUCT_TAC,-,3;
  20     !n. f(n) < f(SUC n) [4] by -,1,LET_TRANS,LE_TRANS,ADD_CLAUSES;
  21     !m n. f(m) < f(n) ==> m < n
  22     proof
  23       !n. f(0) < f(n) ==> 0 < n [5] by LT_LE,LE_0,LTE_TRANS,LE_SUC_LT;
  24       now let m be num;
  25         assume !n. f(m) < f(n) ==> m < n;
  26         thus !n. f(SUC m) < f(n) ==> SUC m < n
  27           by -,4,LT_LE,LE_0,LTE_TRANS,LE_SUC_LT;
  28       end;
  29     qed by INDUCT_TAC,-,5;
  30   qed by -,1,2,LE_ANTISYM,ADD_CLAUSES,LT_SUC_LE`;;
  31
  32 (* ======== long-winded informal proof ===================================== *)
  33
  34 (*
  35
  36 Suppose that f(f(n)) < f(n + 1) for all n.  We want to
  37 show that f has to be the identity.  We will do this by
  38 successively establishing two properties of f (both in a
  39 certain sense being "monotonicity of f"):
  40
  41         n <= f(n)
  42
  43         m < n ==> f(m) < f(n)
  44
  45 The first is the harder one to prove.  The second is easy,
  46 but the proof uses the first.  Once we know the second
  47 property we know so much about f that the result easily
  48 follows.
  49
  50 To prove the first, suppose by contradiction that there is a
  51 counterexample, so there is an n with f "going backwards",
  52 i.e., with f(n) < n.  Take such a counterexample with f(n)
  53 minimal.  (That this minimality is the right one to focus
  54 on is the key to the whole proof for me.  Of course one can
  55 present this proof the other way around -- as an induction --
  56 but the intuition of a descending chain of counterexamples
  57 I find much easier to remember.)  Now from the relation
  58
  59         f(f(n - 1)) < f(n)
  60
  61 it seems reasonable to look for an n' with f going backwards
  62 that has an image less than f(n).  So look at
  63
  64         n - 1  |->  f(n - 1)  |->  f(f(n - 1))
  65
  66 and distinguish how f(n - 1) compares to f(n).  If it's less,
  67 then the left mapping goes backward to an image < f(n).
  68 (To see that it goes backward, use that f(n) < n, so that
  69 f(n) <= n - 1.)  If it's not less, then the right mapping
  70 goes backward to an image < f(n).  In both cases we have
  71 a contradiction with the minimality of our choice of n.
  72
  73 The second kind of monoticity now follows using a trivial
  74 transitivity:
  75
  76         f(n) <= f(f(n)) < f(n + 1)
  77
  78 This shows that f(n) < f(n + 1) for all n, from with the
  79 monotonicity of the whole function directly follows.
  80
  81 Finally to show that f has to be the identity, notice that
  82 a strictly monotonic function always has the property that
  83
  84         n <= f(n)
  85
  86 (Of course we knew this already, but I like to just think
  87 about the strict monotonicity of f at this point.)
  88
  89 However we also can get an upper bound on f(n).  A strictly
  90 monototic function always has a strictly monotonic inverse,
  91 and so from the key property
  92
  93         f(f(n)) < f(n + 1)
  94
  95 it follows that
  96
  97         f(n) < n + 1
  98
  99 Together this means that we have to have that f(n) = n.
 100
 101 *)
 102
 103 (* ======== formal proof sketch of this proof ============================== *)
 104
 105 horizon := -1;;
 106 sketch_mode := true;;
 107
 108 let FORSTER_PUZZLE_SKETCH = ref None;;
 109
 110 FORSTER_PUZZLE_SKETCH := Some `;
 111   let f be num->num;
 112   assume !n. f(f(n)) < f(n + 1);
 113   thus !n. f(n) = n
 114   proof
 115     !n. n <= f(n)
 116     proof
 117       assume ~thesis;
 118       ?n. f(n) < n;
 119       consider n such that f(n) < n /\
 120         !m. f(m) < m ==> f(n) <= f(m);
 121       cases;
 122       suppose f(n - 1) < f(n);
 123         f(n - 1) < n - 1 /\ f(n - 1) < f(n)
 124         proof
 125           f(n) < n;
 126           f(n) <= n - 1;
 127         qed;
 128         thus F;
 129       end;
 130       suppose f(n) <= f(n - 1);
 131         f(f(n - 1)) < f(n - 1) /\ f(f(n - 1)) < f(n);
 132         thus F;
 133       end;
 134     end;
 135     !m n. m < n ==> f(m) < f(n)
 136     proof
 137       now
 138         let n be num;
 139         f(n) <= f(f(n)) /\ f(f(n)) < f(n + 1);
 140         thus f(n) < f(n + 1);
 141       end;
 142     qed;
 143     let n be num;
 144     n <= f(n);
 145     !m n. f(m) < f(n) ==> m < n;
 146     f(f(n)) < f(n + 1);
 147     f(n) < n + 1;
 148     thus f(n) = n;
 149   end`;;
 150
 151 sketch_mode := false;;
 152
 153 (* ======== formalization from this formal proof sketch ==================== *)
 154
 155 horizon := 1;;
 156
 157 let FORSTER_PUZZLE_2 = thm `;
 158   let f be num->num;
 159   assume !n. f(f(n)) < f(n + 1) [1];
 160   thus !n. f(n) = n
 161   proof
 162     !n. n <= f(n) [2]
 163     proof
 164       assume ~thesis;
 165       ?n. f(n) < n by NOT_LE;
 166       ?fn n. f(n) = fn /\ f(n) < n;
 167       consider fn such that (?n. f(n) = fn /\ f(n) < n) /\
 168         !fm. fm < fn ==> ~(?m. f(m) = fm /\ f(m) < m) [3]
 169           by REWRITE_TAC,GSYM num_WOP;
 170       consider n such that f(n) = fn /\ f(n) < n;
 171       f(n) < n /\ !m. f(m) < m ==> f(n) <= f(m) [4] by 3,NOT_LE;
 172       cases;
 173       suppose f(n - 1) < f(n) [5];
 174         f(n - 1) < n - 1 /\ f(n - 1) < f(n)
 175         proof
 176           f(n) < n by 4;
 177           f(n) <= n - 1 by ARITH_TAC;
 178         qed by 5,LTE_TRANS;
 179         thus F by 4,NOT_LE;
 180       end;
 181       suppose f(n) <= f(n - 1) [6];
 182         0 < n by ARITH_TAC,4;
 183         (n - 1) + 1 = n by ARITH_TAC;
 184         f(f(n - 1)) < f(n) by 1;
 185         f(f(n - 1)) < f(n - 1) /\ f(f(n - 1)) < f(n) by ARITH_TAC,6;
 186         thus F by 4,NOT_LE;
 187       end;
 188     end;
 189     !m n. m < n ==> f(m) < f(n) [7]
 190     proof
 191       now
 192         let n be num;
 193         f(n) <= f(f(n)) /\ f(f(n)) < f(n + 1) by 1,2;
 194         thus f(n) < f(SUC n) by ARITH_TAC;  // modified from f(n) < f(n + 1)
 195       end;
 196     qed by LT_TRANS,
 197       SPEC (parse_term "\\m n. (f:num->num)(m) < f(n)") TRANSITIVE_STEPWISE_LT;
 198     let n be num;
 199     n <= f(n) [8] by 2;  // really should be an induction proof from 7
 200     !m n. f(m) < f(n) ==> m < n [9] by 7,LE_LT,NOT_LE;
 201     f(f(n)) < f(n + 1) by 1;
 202     f(n) < n + 1 by 9;
 203     thus f(n) = n by ARITH_TAC,8;
 204   end`;;
 205
 206 (* ======== ... and a slightly compressed version ========================== *)
 207
 208 horizon := 1;;
 209
 210 let FORSTER_PUZZLE_3 = thm `;
 211   let f be num->num;
 212   assume !n. f(f(n)) < f(n + 1) [1];
 213   !n. n <= f(n) [2]
 214   proof
 215     assume ~thesis;
 216     ?fn n. f(n) = fn /\ f(n) < n by NOT_LE;
 217     consider fn such that (?n. f(n) = fn /\ f(n) < n) /\
 218       !fm. fm < fn ==> ~(?m. f(m) = fm /\ f(m) < m) [3]
 219         by REWRITE_TAC,GSYM num_WOP;
 220     consider n such that f(n) = fn /\ f(n) < n [4];
 221     cases;
 222     suppose f(n - 1) < f(n) [5];
 223       f(n - 1) < n - 1 by ARITH_TAC,4;
 224       thus F by 3,4,5;
 225     end;
 226     suppose f(n) <= f(n - 1) [6];
 227       (n - 1) + 1 = n by ARITH_TAC,4;
 228       thus F by 1,3,4,6,LTE_TRANS;
 229     end;
 230   end;
 231   !n. f(n) < f(SUC n) by 1,2,ADD1,LET_TRANS;
 232   !m n. m < n ==> f(m) < f(n) by LT_TRANS,
 233     SPEC (parse_term "\\m n. (f:num->num)(m) < f(n)") TRANSITIVE_STEPWISE_LT;
 234   !m n. f(m) < f(n) ==> m < n by LE_LT,NOT_LE;
 235   thus !n. f(n) = n by 1,2,ADD1,LE_ANTISYM,LT_SUC_LE`;;
 236
 237 (* ======== Mizar formalization from the formal proof sketch =============== *)
 238
 239 (*
 240
 241 environ
 242   vocabularies RELAT_1, FUNCT_1, ARYTM, ARYTM_1, ORDINAL2;
 243   notations ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
 244     VALUED_0;
 245   constructors XXREAL_0, INT_1, PARTFUN1, VALUED_0, MEMBERED, RELSET_1;
 246   registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0, XREAL_0,
 247     NAT_1, INT_1, VALUED_0, MEMBERED;
 248   requirements NUMERALS, REAL, SUBSET, ARITHM;
 249   theorems XXREAL_0, XREAL_1, INT_1, NAT_1, VALUED_0, VALUED_1, FUNCT_2,
 250     ORDINAL1;
 251   schemes NAT_1;
 252
 253 begin
 254   reserve n,m,fn,fm for natural number;
 255   reserve f for Function of NAT,NAT;
 256
 257 theorem
 258   (for n holds f.(f.n) < f.(n + 1)) implies for n holds f.n = n
 259 proof
 260   assume
 261 A1: for n holds f.(f.n) < f.(n + 1);
 262 A2: for n holds n <= f.n
 263   proof
 264     assume
 265 A3:   not thesis;
 266     defpred P[Nat] means ex n st f.n < n & f.n = $1;
 267 A4: ex fn st P[fn] by A3;
 268     consider fn being Nat such that
 269 A5:   P[fn] & for fm being Nat st P[fm] holds fn <= fm from NAT_1:sch 5(A4);
 270     consider n such that
 271 A6:   f.n < n & f.n = fn by A5;
 272     n >= 0 + 1 by A6,NAT_1:13;
 273     then n - 1 >= 0 by XREAL_1:21;
 274     then n - 1 in NAT by INT_1:16;
 275     then reconsider m = n - 1 as natural number;
 276     per cases;
 277     suppose
 278 A7:     f.m < f.n;
 279       f.n < m + 1 by A6;
 280       then f.n <= m by NAT_1:13;
 281       then f.m < m by A7,XXREAL_0:2;
 282       hence contradiction by A5,A6,A7;
 283     end;
 284     suppose
 285 A8:     f.n <= f.m;
 286 A9:   f.(f.m) < f.(m + 1) by A1;
 287       then f.(f.m) < f.m by A8,XXREAL_0:2;
 288       hence contradiction by A5,A6,A9;
 289     end;
 290   end;
 291   now
 292     let n;
 293     f.n <= f.(f.n) & f.(f.n) < f.(n + 1) by A1,A2;
 294     hence f.n < f.(n + 1) by XXREAL_0:2;
 295   end;
 296   then reconsider f as increasing Function of NAT,NAT by VALUED_1:def 13;
 297 A10: now
 298     let m,n;
 299     dom f = NAT & m in NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 13;
 300     hence f.m < f.n implies m < n by VALUED_0:def 15;
 301   end;
 302   let n;
 303   f.(f.n) < f.(n + 1) by A1;
 304   then f.n < n + 1 by A10;
 305   then n <= f.n & f.n <= n by A2,NAT_1:13;
 306   hence thesis by XXREAL_0:1;
 307 end;
 308
 309 *)
 310
 311 (* ======== miz3 formalization close to the Mizar formalization ============ *)
 312
 313 horizon := 0;;
 314
 315 let FORSTER_PUZZLE_4 = thm `;
 316   !f. (!n. f(f(n)) < f(n + 1)) ==> !n. f(n) = n
 317 proof
 318   let f be num->num;
 319   assume !n. f(f(n)) < f(n + 1) [1];
 320   !n. n <= f(n) [2]
 321   proof
 322     assume ~thesis [3];
 323     set P = \fn. ?n. f(n) < n /\ f(n) = fn [P];
 324     ?fn. P(fn) [4] by 3,P,NOT_LE;
 325     consider fn such that P(fn) /\ !fm. P(fm) ==> fn <= fm [5]
 326       by 4,num_WOP,NOT_LE;
 327     consider n such that f(n) < n /\ f(n) = fn [6] by P,5;
 328     set m = n - 1;
 329     n = m + 1 [m] by ARITH_TAC,6;       // replaces the reconsider
 330     cases;
 331     suppose f(m) < f(n) [7];
 332       f(n) < m + 1 by ARITH_TAC,6;
 333       f(n) <= m by ARITH_TAC,-;
 334       f(m) < m by ARITH_TAC,-,7;
 335       f(n) <= f(m) by -,P,5,6;          // extra step
 336       thus F by ARITH_TAC,-,7;
 337     end;
 338     suppose f(n) <= f(m) [8];
 339       f(f(m)) < f(m + 1) [9] by 1;
 340       f(f(m)) < f(m) by -,m,8,LTE_TRANS;
 341       f(n) <= f(f(m)) by -,P,5,6;       // extra step
 342       thus F by -,m,9,NOT_LE;
 343     end;
 344   end;
 345   now
 346     let n be num;
 347     f(n) <= f(f(n)) /\ f(f(n)) < f(n + 1) by 1,2;
 348     thus f(n) < f(n + 1) by ARITH_TAC,-;
 349   end;
 350   !n. f(n) < f(SUC n) by -,ADD1;        // extra step
 351   !m n. m < n ==> f(m) < f(n) by -,LT_TRANS,
 352     SPEC (parse_term "\\m n. (f:num->num)(m) < f(n)") TRANSITIVE_STEPWISE_LT;
 353                                         // replaces the reconsider
 354   now [10]
 355     let m n be num;
 356     thus f(m) < f(n) ==> m < n by -,LE_LT,NOT_LE;
 357   end;
 358   let n be num;
 359   f(f(n)) < f(n + 1) by 1;
 360   f(n) < n + 1 by -,10;
 361   n <= f(n) /\ f(n) <= n by -,2,ADD1,LT_SUC_LE;
 362   thus thesis by ARITH_TAC,-;
 363 end`;;
 364
 365 (* ======== formalization following Tobias & Sean's version ================ *)
 366
 367 horizon := 3;;
 368
 369 let num_MONO_LT_SUC = thm `;
 370   let f be num->num;
 371   assume !n. f(n) < f(SUC n);
 372   !n m. m < n ==> f(m) < f(n) by LT_TRANS,
 373     SPEC (parse_term "\\m n. (f:num->num)(m) < f(n)") TRANSITIVE_STEPWISE_LT;
 374   thus !n m. m < n <=> f(m) < f(n) by LE_LT,NOT_LE`;;
 375
 376 let FORSTER_PUZZLE_5 = thm `;
 377   let f be num->num;
 378   assume !n. f(f(n)) < f(SUC(n));
 379   !n m. n <= m ==> n <= f(m)
 380   proof
 381     now let n be num; assume !m. n <= m ==> n <= f(m);
 382       !m. SUC n <= m ==> ?k. m = SUC k by num_CASES,LT,LE_SUC_LT;
 383       thus !m. SUC n <= m ==> SUC n <= f(m) by LE_SUC,LET_TRANS,LE_SUC_LT;
 384     end;
 385     !m. 0 <= m ==> 0 <= f(m);
 386   qed by INDUCT_TAC;
 387   !n. f(n) < f(SUC n) by LE_REFL,LET_TRANS;
 388   thus !n. f(n) = n by num_MONO_LT_SUC,LT_SUC_LE,LE_ANTISYM`;;
 389