RichterHilbertAxiomGeometry/error-checking.ml

   1 (*                (c) Copyright, Bill Richter 2013                           *)
   2 (*          Distributed under the same license as HOL Light                  *)
   3 (*                                                                           *)
   4 (* Examples showing error messages displayed by readable.ml when raising the *)
   5 (* exception Readable_fail, with some working examples interspersed.         *)
   6
   7 needs "RichterHilbertAxiomGeometry/readable.ml";;
   8
   9 let s = "abc]edf" in Str.string_before s (FindMatch "\[" "\]" s);;
  10
  11 let s = "123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]xyz" in
  12   Str.string_before s (FindMatch "\[" "\]" s);;
  13
  14 (* val it : string = "abc]"
  15    val it : string = "123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]"                   *)
  16
  17 let s = "123456[abc]lmn[op[abc]pq]rs!!!!!!!!!![]xyz" in Str.string_before s
  18   (FindMatch "\[" "\]" s);;
  19
  20 (*     Exception:
  21 No matching right bracket operator \] to left bracket operator \[ in xyz.    *)
  22
  23 let s = "123456[abc]lmn[op[a; b; c]pq]rs[];xyz" in
  24   Str.string_before s (FindSemicolon s);;
  25
  26 let s = "123456[abc]lmn[op[a; b; c]pq]rs![]xyz" in
  27   Str.string_before s (FindSemicolon s);;
  28
  29 (* val it : string = "123456[abc]lmn[op[a; b; c]pq]rs[]"
  30
  31   Exception: No final semicolon in 123456[abc]lmn[op[a; b; c]pq]rs![]xyz. *)
  32
  33 let MOD_MOD_REFL = theorem `;
  34   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
  35
  36   proof
  37     intro_TAC !m n, H1;
  38     MP_TAC ISPECL [m; n; 1] MOD_MOD;
  39     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  40   qed;
  41 `;;
  42
  43 (*                   0..0..3..6..solved at 21
  44 0..0..3..6..31..114..731..5973..solved at 6087
  45 val MOD_MOD_REFL : thm = |- !m n. ~(n = 0) ==> m MOD n MOD n = m MOD n       *)
  46
  47 let MOD_MOD_REFL = theorem `;
  48   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
  49
  50   proof
  51     INTRO_TAC !m n, H1;
  52     MP_TAC ISPECL [m; n; 1] MOD_MOD;
  53     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  54   qed;
  55 `;;
  56
  57 (*                  Exception: Can't parse as a Proof:
  58
  59     INTRO_TAC !m n, H1.                                                      *)
  60
  61 let MOD_MOD_REFL = theorem `;
  62   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
  63
  64   proof
  65     intro_TAC !m n, H1;
  66     MP_TAC ISPECL [m; n; 1] mod_mod;
  67     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  68   qed;
  69 `;;
  70
  71 (*                Exception: Not a theorem:
  72  mod_mod.                                                                    *)
  73
  74
  75 let MOD_MOD_REFL = theorem `;
  76   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
  77
  78   proof
  79     intro_TAC !m n, H1;
  80     MP_TAC ISPECL  MOD_MOD;
  81     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  82   qed;
  83 `;;
  84
  85 (*                        Exception: termlist->thm->thm ISPECL
  86  not followed by term list in
  87   MOD_MOD.                                                                   *)
  88
  89 let MOD_MOD_REFL = theorem `;
  90   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
  91
  92   proof
  93     intro_TAC !m n, H1;
  94     MP_TAC ISPECL m n 1] MOD_MOD;
  95     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  96   qed;
  97 `;;
  98
  99 (*                        Exception:
 100 termlist->thm->thm ISPECL
 101  not followed by term list in
 102  m n 1] MOD_MOD.                                                             *)
 103
 104 interactive_goal `;∀p q. p * p = 2 * q * q  ⇒  q = 0
 105 `;;
 106 interactive_proof `;
 107     MATCH_MP_TAC     ;
 108     intro_TAC ∀p, A, ∀q, B;
 109     EVEN(p * p) ⇔ EVEN(2 * q * q)     [] proof  qed;
 110 `;;
 111
 112 (*         Exception: Empty theorem:
 113  .                                                                           *)
 114
 115
 116 interactive_goal `;∀p q. p * p = 2 * q * q  ⇒  q = 0
 117 `;;
 118 interactive_proof `;
 119     MATCH_MP_TAC num_WF num_WF ;
 120     intro_TAC ∀p, A, ∀q, B;
 121     EVEN(p * p) ⇔ EVEN(2 * q * q)     [] proof  qed;
 122 `;;
 123
 124 (*          Exception:
 125 thm_tactic MATCH_MP_TAC not followed by a theorem, but instead
 126  num_WF num_WF .                                                             *)
 127
 128 let EXP_2 = theorem `;
 129   ∀n:num. n EXP 2 = n * n
 130   by REWRITE BIT0_THM BIT1_THM EXP EXP_ADD MULT_CLAUSES ADD_CLAUSES`;;
 131
 132 (*      Exception:
 133 Not a proof:
 134  REWRITE BIT0_THM BIT1_THM EXP EXP_ADD MULT_CLAUSES ADD_CLAUSES.
 135
 136 The problem is that REWRITE should be rewrite.*)
 137
 138 let MOD_MOD_REFL = theorem `;
 139   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
 140
 141   prooof
 142     intro_TAC !m n, H1;
 143     MP_TAC ISPECL [m; n; 1] MOD_MOD;
 144     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
 145   qed;
 146 `;;
 147
 148 (*                            Exception:
 149 Missing initial "proof", "by", or final "qed;" in
 150
 151   !m n. ~(n = 0)  ==>  ((m MOD n) MOD n = m MOD n)
 152
 153   prooof
 154     intro_TAC !m n, H1;
 155     MP_TAC ISPECL [m; n; 1] MOD_MOD;
 156     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
 157   qed;
 158 .                                                                            *)
 159
 160 let MOD_MOD_REFL = theorem `;
 161   ∀m n. ¬(n = 0)  ⇒  ((m MOD n) MOD n = m MOD n)
 162
 163   proof
 164     intro_TAC !m n, H1;
 165     MP_TAC ISPECL [m; n; 1] MOD_MOD;
 166     fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
 167   qed;
 168 What me worry?
 169 `;;
 170
 171 (*                  Exception: Trailing garbage after the proof...qed:
 172 What me worry?
 173 .
 174
 175    Two examples from the ocaml reference manual sec 1.4 to show the
 176    handling of exceptions other than Readable_fail.                          *)
 177
 178 exception Empty_list;;
 179 let head l =
 180   match l with
 181      [] -> raise Empty_list
 182   | hd :: tl -> hd;;
 183 head [1;2];;
 184 head [];;
 185
 186 exception Unbound_variable of string;;
 187
 188 type expression =
 189      Const of float
 190    | Var of string
 191    | Sum of expression * expression
 192    | Diff of expression * expression
 193    | Prod of expression * expression
 194    | Quot of expression * expression;;
 195
 196 let rec eval env exp =
 197     match exp with
 198        Const c -> c
 199     | Var v ->
 200          (try List.assoc v env with Not_found -> raise(Unbound_variable v))
 201     | Sum(f, g) -> eval env f +. eval env g
 202     | Diff(f, g) -> eval env f -. eval env g
 203     | Prod(f, g) -> eval env f *. eval env g
 204     | Quot(f, g) -> eval env f /. eval env g;;
 205
 206 eval [("x", 1.0); ("y", 3.14)] (Prod(Sum(Var "x", Const 2.0), Var "y"));;
 207
 208 eval [("x", 1.0); ("y", 3.14)] (Prod(Sum(Var "z", Const 2.0), Var "y"));;
 209
 210
 211 (* The only difference caused by printReadExn is that
 212     Exception: Unbound_variable "z".
 213     is now
 214     Exception: Unbound_variable("z").                                        *)
 215
 216
 217 let binom = define
 218  `(!n. binom(n,0) = 1) /\
 219   (!k. binom(0,SUC(k)) = 0) /\
 220   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
 221
 222 let BINOM_LT = theorem `;
 223   ∀n k. n < k  ⇒  binom(n,k) = 0
 224
 225   proof
 226     INDUCT_TAC; INDUCT_TAC;
 227     rewrite binom ARITH LT_SUC LT;
 228     ASM_SIMP_TAC ARITH_RULE [n < k ==> n < SUC(k)] ARITH;
 229   qed;
 230 `;;
 231
 232 let BINOM_REFL = theorem `;
 233   ∀n. binom(n,n) = 1
 234
 235   proof
 236     INDUCT_TAC;
 237     ASM_SIMP_TAC binom BINOM_LT LT ARITH;
 238   qed;
 239 `;;
 240
 241 let BINOMIAL_THEOREM = theorem `;
 242   ∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
 243
 244   proof
 245     ∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))     [Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
 246     MATCH_MP_TAC num_INDUCTION;
 247     simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
 248     intro_TAC ∀n, nThm;
 249     rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC;
 250     rewriteR ADD_SYM;
 251     rewriteRLDepth SUB_SUC EXP;
 252     rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] [1 = binom(n, 0)] GSYM Nsum0SUC;
 253     simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n  ∧  0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
 254     simplify ARITH_RULE [k <= n  ⇒  SUC n - k = SUC(n - k)] EXP MULT_AC;
 255   qed;
 256 `;;
 257
 258 (* val binom : thm =
 259   |- (!n. binom (n,0) = 1) /\
 260      (!k. binom (0,SUC k) = 0) /\
 261      (!n k. binom (SUC n,SUC k) = binom (n,SUC k) + binom (n,k))
 262                 val BINOM_LT : thm = |- !n k. n < k ==> binom (n,k) = 0
 263                 val BINOM_REFL : thm = |- !n. binom (n,n) = 1
 264                               0..0..1..2..solved at 6
 265 val BINOMIAL_THEOREM : thm =
 266   |- !n. (x + y) EXP n =
 267          nsum (0..n) (\k. binom (n,k) * x EXP k * y EXP (n - k))             *)
 268
 269
 270 let BINOM_LT = theorem `;
 271   ∀n k. n < k  ⇒  binom(n,k) = 0
 272
 273   proof
 274     INDUCT_TAC; INDUCT_TAC;
 275     rewrite binom ARITH LT_SUC LT;
 276     ASM_SIMP_TAC ARITH_RULE n < k ==> n < SUC(k)] ARITH;
 277   qed;
 278 `;;
 279
 280 (*                   Exception:
 281 term->thm ARITH_RULE not followed by term list, but instead
 282 n < k ==> n < SUC(k)] ARITH.                                                 *)
 283
 284
 285 let BINOM_LT = theorem `;
 286   ∀n k. n < k  ⇒  binom(n,k) = 0
 287
 288   proof
 289     INDUCT_TAC; INDUCT_TAC;
 290     rewrite binom ARITH LT_SUC LT;
 291     ASM_SIMP_TAC ARITH_RULE [n < k; n < SUC(k)] ARITH;
 292   qed;
 293 `;;
 294
 295 (*                   Exception:
 296 term->thm ARITH_RULE not followed by length 1 term list, but instead the list
 297 [n < k; n < SUC(k)].                                                         *)
 298
 299
 300 let BINOM_LT = theorem `;
 301   ∀n k. n < k  ⇒  binom(n,k) = 0
 302
 303   proof
 304     INDUCT_TAC; INDUCT_TAC;
 305     rewrite binom ARITH LT_SUC LT;
 306     ASM_SIMP_TAC ARITH_RULE [ ] ARITH;
 307   qed;
 308 `;;
 309
 310 (*                   Exception:
 311 term->thm ARITH_RULE not followed by length 1 term list, but instead the list
 312  [].                                                                         *)
 313
 314
 315 let BINOMIAL_THEOREM = theorem `;
 316   ∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
 317
 318   proof
 319     ∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))     [Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
 320     MATCH_MP_TAC num_INDUCTION;
 321     simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
 322     intro_TAC ∀n, nThm;
 323     rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC;
 324     rewriteR ADD_SYM;
 325     rewriteRLDepth SUB_SUC EXP;
 326     rewrite MULT_AC EQ_ADD_LCANCEL MESON binom] [1 = binom(n, 0)] GSYM Nsum0SUC;
 327     simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n  ∧  0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
 328     simplify ARITH_RULE [k <= n  ⇒  SUC n - k = SUC(n - k)] EXP MULT_AC;
 329   qed;
 330 `;;
 331
 332 (*                                  Exception:
 333 thmlist->term->thm MESON not followed by thm list in
 334  binom] [1 = binom(n, 0)] GSYM Nsum0SUC.                                     *)
 335
 336
 337 let BINOMIAL_THEOREM = theorem `;
 338   ∀n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))
 339
 340   proof
 341     ∀f n. nsum (0.. SUC n) f = f(0) + nsum (0..n) (λi. f (SUC i))     [Nsum0SUC] by simplify LE_0 ADD1 NSUM_CLAUSES_LEFT NSUM_OFFSET;
 342     MATCH_MP_TAC num_INDUCTION;
 343     simplify EXP NSUM_SING_NUMSEG binom SUB_0 MULT_CLAUSES;
 344     intro_TAC ∀n, nThm;
 345     rewrite Nsum0SUC binom RIGHT_ADD_DISTRIB NSUM_ADD_NUMSEG GSYM NSUM_LMUL ADD_ASSOC;
 346     rewriteR ADD_SYM;
 347     rewriteRLDepth SUB_SUC EXP;
 348     rewrite MULT_AC EQ_ADD_LCANCEL MESON [binom] 1 = binom(n, 0)] GSYM Nsum0SUC;
 349     simplify NSUM_CLAUSES_RIGHT ARITH_RULE [0 < SUC n  ∧  0 <= SUC n] LT BINOM_LT MULT_CLAUSES ADD_CLAUSES SUC_SUB1;
 350     simplify ARITH_RULE [k <= n  ⇒  SUC n - k = SUC(n - k)] EXP MULT_AC;
 351   qed;
 352 `;;
 353
 354 (*                                Exception:
 355 thmlist->term->thm MESON followed by list of theorems [binom]
 356       not followed by term in
 357  1 = binom(n, 0)] GSYM Nsum0SUC.                                             *)
 358