Mizarlight/duality_holby.ml

   1 (* ========================================================================= *)
   2 (* Mizar Light proof of duality in projective geometry.                      *)
   3 (* ========================================================================= *)
   4
   5 let holby_prover =
   6   fun ths (asl,w as gl) -> ACCEPT_TAC(HOL_BY ths w) gl;;
   7
   8 current_prover := holby_prover;;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* To avoid adding any axioms, pick a simple model: the Fano plane.          *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let Line_INDUCT,Line_RECURSION = define_type
  15  "Line = Line_1 | Line_2 | Line_3 | Line_4 |
  16          Line_5 | Line_6 | Line_7";;
  17
  18 let Point_INDUCT,Point_RECURSION = define_type
  19  "Point = Point_1 | Point_2 | Point_3 | Point_4 |
  20           Point_5 | Point_6 | Point_7";;
  21
  22 let Point_DISTINCT = distinctness "Point";;
  23
  24 let Line_DISTINCT = distinctness "Line";;
  25
  26 let fano_incidence =
  27   [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4;
  28    4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];;
  29
  30 let fano_point i = mk_const("Point_"^string_of_int i,[])
  31 and fano_line i = mk_const("Line_"^string_of_int i,[]);;
  32
  33 let p = `p:Point` and l = `l:Line` ;;
  34
  35 let fano_clause (i,j) =
  36   mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
  37
  38 (* ------------------------------------------------------------------------- *)
  39 (* Define the incidence relation "ON" from "fano_incidence"                  *)
  40 (* ------------------------------------------------------------------------- *)
  41
  42 parse_as_infix("ON",(11,"right"));;
  43
  44 let ON = new_definition
  45  `(p:Point) ON (l:Line) <=>
  46         (p = Point_1 /\ l = Line_1) \/
  47         (p = Point_1 /\ l = Line_2) \/
  48         (p = Point_1 /\ l = Line_3) \/
  49         (p = Point_2 /\ l = Line_1) \/
  50         (p = Point_2 /\ l = Line_4) \/
  51         (p = Point_2 /\ l = Line_5) \/
  52         (p = Point_3 /\ l = Line_1) \/
  53         (p = Point_3 /\ l = Line_6) \/
  54         (p = Point_3 /\ l = Line_7) \/
  55         (p = Point_4 /\ l = Line_2) \/
  56         (p = Point_4 /\ l = Line_4) \/
  57         (p = Point_4 /\ l = Line_6) \/
  58         (p = Point_5 /\ l = Line_2) \/
  59         (p = Point_5 /\ l = Line_5) \/
  60         (p = Point_5 /\ l = Line_7) \/
  61         (p = Point_6 /\ l = Line_3) \/
  62         (p = Point_6 /\ l = Line_4) \/
  63         (p = Point_6 /\ l = Line_7) \/
  64         (p = Point_7 /\ l = Line_3) \/
  65         (p = Point_7 /\ l = Line_5) \/
  66         (p = Point_7 /\ l = Line_6)`;;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Also produce a more convenient case-by-case rewrite.                      *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 let ON_CLAUSES = prove
  73  (`(Point_1 ON Line_1 <=> T) /\
  74    (Point_1 ON Line_2 <=> T) /\
  75    (Point_1 ON Line_3 <=> T) /\
  76    (Point_1 ON Line_4 <=> F) /\
  77    (Point_1 ON Line_5 <=> F) /\
  78    (Point_1 ON Line_6 <=> F) /\
  79    (Point_1 ON Line_7 <=> F) /\
  80    (Point_2 ON Line_1 <=> T) /\
  81    (Point_2 ON Line_2 <=> F) /\
  82    (Point_2 ON Line_3 <=> F) /\
  83    (Point_2 ON Line_4 <=> T) /\
  84    (Point_2 ON Line_5 <=> T) /\
  85    (Point_2 ON Line_6 <=> F) /\
  86    (Point_2 ON Line_7 <=> F) /\
  87    (Point_3 ON Line_1 <=> T) /\
  88    (Point_3 ON Line_2 <=> F) /\
  89    (Point_3 ON Line_3 <=> F) /\
  90    (Point_3 ON Line_4 <=> F) /\
  91    (Point_3 ON Line_5 <=> F) /\
  92    (Point_3 ON Line_6 <=> T) /\
  93    (Point_3 ON Line_7 <=> T) /\
  94    (Point_4 ON Line_1 <=> F) /\
  95    (Point_4 ON Line_2 <=> T) /\
  96    (Point_4 ON Line_3 <=> F) /\
  97    (Point_4 ON Line_4 <=> T) /\
  98    (Point_4 ON Line_5 <=> F) /\
  99    (Point_4 ON Line_6 <=> T) /\
 100    (Point_4 ON Line_7 <=> F) /\
 101    (Point_5 ON Line_1 <=> F) /\
 102    (Point_5 ON Line_2 <=> T) /\
 103    (Point_5 ON Line_3 <=> F) /\
 104    (Point_5 ON Line_4 <=> F) /\
 105    (Point_5 ON Line_5 <=> T) /\
 106    (Point_5 ON Line_6 <=> F) /\
 107    (Point_5 ON Line_7 <=> T) /\
 108    (Point_6 ON Line_1 <=> F) /\
 109    (Point_6 ON Line_2 <=> F) /\
 110    (Point_6 ON Line_3 <=> T) /\
 111    (Point_6 ON Line_4 <=> T) /\
 112    (Point_6 ON Line_5 <=> F) /\
 113    (Point_6 ON Line_6 <=> F) /\
 114    (Point_6 ON Line_7 <=> T) /\
 115    (Point_7 ON Line_1 <=> F) /\
 116    (Point_7 ON Line_2 <=> F) /\
 117    (Point_7 ON Line_3 <=> T) /\
 118    (Point_7 ON Line_4 <=> F) /\
 119    (Point_7 ON Line_5 <=> T) /\
 120    (Point_7 ON Line_6 <=> T) /\
 121    (Point_7 ON Line_7 <=> F)`,
 122   REWRITE_TAC[ON; Line_DISTINCT; Point_DISTINCT]);;
 123
 124 (* ------------------------------------------------------------------------- *)
 125 (* Case analysis theorems.                                                   *)
 126 (* ------------------------------------------------------------------------- *)
 127
 128 let FORALL_POINT = prove
 129  (`(!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\
 130                  P Point_5 /\ P Point_6 /\ P Point_7`,
 131   EQ_TAC THEN REWRITE_TAC[Point_INDUCT] THEN SIMP_TAC[]);;
 132
 133 let EXISTS_POINT = prove
 134  (`(?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/
 135                  P Point_5 \/ P Point_6 \/ P Point_7`,
 136   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
 137   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_POINT]);;
 138
 139 let FORALL_LINE = prove
 140  (`(!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\
 141                  P Line_5 /\ P Line_6 /\ P Line_7`,
 142   EQ_TAC THEN REWRITE_TAC[Line_INDUCT] THEN SIMP_TAC[]);;
 143
 144 let EXISTS_LINE = prove
 145  (`(?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/
 146                  P Line_5 \/ P Line_6 \/ P Line_7`,
 147   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
 148   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_LINE]);;
 149
 150 (* ------------------------------------------------------------------------- *)
 151 (* Hence prove the axioms by a naive case split (a bit slow but easy).       *)
 152 (* ------------------------------------------------------------------------- *)
 153
 154 let FANO_TAC =
 155   GEN_REWRITE_TAC DEPTH_CONV
 156    [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN
 157   GEN_REWRITE_TAC DEPTH_CONV
 158    (basic_rewrites() @ [ON_CLAUSES; Point_DISTINCT; Line_DISTINCT]);;
 159
 160 let AXIOM_1 = time prove
 161  (`!p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\
 162      !l'. p ON l' /\ p' ON l' ==> (l' = l)`,
 163   FANO_TAC);;
 164
 165 let AXIOM_2 = time prove
 166  (`!l l'. ?p. p ON l /\ p ON l'`,
 167   FANO_TAC);;
 168
 169 let AXIOM_3 = time prove
 170  (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 171     ~(?l. p ON l /\ p' ON l /\ p'' ON l)`,
 172   FANO_TAC);;
 173
 174 let AXIOM_4 = time prove
 175  (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 176     p ON l /\ p' ON l /\ p'' ON l`,
 177   FANO_TAC);;
 178
 179 (* ------------------------------------------------------------------------- *)
 180 (* Now the interesting bit.                                                  *)
 181 (* ------------------------------------------------------------------------- *)
 182
 183 let AXIOM_1' = theorem
 184  "!p p' l l'. ~(p = p') /\\ p ON l /\\ p' ON l /\\ p ON l' /\\ p' ON l'
 185     ==> (l' = l)"
 186  [fix ["p:Point"; "p':Point"; "l:Line"; "l':Line"];
 187   assume "~(p = p') /\\ p ON l /\\ p' ON l /\\ p ON l' /\\ p' ON l'" at 1;
 188   consider ["l1:Line"] st "p ON l1 /\\ p' ON l1 /\\
 189     !l'. p ON l' /\\ p' ON l' ==> (l' = l1)" from [1] by [AXIOM_1] at 2;
 190   have "l = l1" from [1;2];
 191   so have "... = l'" from [1;2];
 192   qed];;
 193
 194 let LEMMA_1 = theorem
 195  "!O. ?l. O ON l"
 196  [consider ["p:Point"; "p':Point"; "p'':Point"] st
 197    "~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
 198      ~(?l. p ON l /\\ p' ON l /\\ p'' ON l)" by [AXIOM_3] at 1;
 199   fix ["O:Point"];
 200   have "~(p = O) \/ ~(p' = O)" from [1];
 201   so consider ["P:Point"] st "~(P = O)" at 2;
 202   consider ["l:Line"] st "O ON l /\\ P ON l /\\
 203     !l'. O ON l' /\\ P ON l' ==> (l' = l)" from [2] by [AXIOM_1] at 3;
 204   thus "?l. O ON l" from [3]];;
 205
 206 let DUAL_1 = theorem
 207  "!l l'. ~(l = l') ==> ?p. p ON l /\\ p ON l' /\\
 208     !p'. p' ON l /\\ p' ON l' ==> (p' = p)"
 209  [otherwise consider ["l:Line"; "l':Line"] st
 210    "~(l = l') /\\ !p. p ON l /\\ p ON l'
 211      ==> ?p'. p' ON l /\\ p' ON l' /\\ ~(p' = p)" at 1;
 212   consider ["p:Point"] st "p ON l /\\ p ON l'" by [AXIOM_2] at 2;
 213   consider ["p':Point"] st "p' ON l /\\ p' ON l' /\\ ~(p' = p)" from [1;2] at 3;
 214   hence contradiction from [1;2] by [AXIOM_1']];;
 215
 216 let DUAL_2 = theorem
 217  "!p p'. ?l. p ON l /\\ p' ON l"
 218  [fix ["p:Point"; "p':Point"];
 219   have "?l. p ON l" by [LEMMA_1] at 1;
 220   have "(p = p') \/
 221     ?l. p ON l /\\ p' ON l /\\
 222       !l'. p ON l' /\\ p' ON l' ==> (l' = l)" by [AXIOM_1];
 223   hence thesis from [1]];;
 224
 225 let DUAL_3 = theorem
 226  "?l1 l2 l3. ~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3) /\\
 227     ~(?p. p ON l1 /\\ p ON l2 /\\ p ON l3)"
 228  [consider ["p1:Point"; "p2:Point"; "p3:Point"] st
 229    "~(p1 = p2) /\\ ~(p2 = p3) /\\ ~(p1 = p3) /\\
 230       ~(?l. p1 ON l /\\ p2 ON l /\\ p3 ON l)" by [AXIOM_3] at 1;
 231   consider ["l1:Line"] st "p1 ON l1 /\\ p3 ON l1" by [DUAL_2] at 2;
 232   consider ["l2:Line"] st "p2 ON l2 /\\ p3 ON l2" by [DUAL_2] at 3;
 233   consider ["l3:Line"] st "p1 ON l3 /\\ p2 ON l3" by [DUAL_2] at 4;
 234   take ["l1"; "l2"; "l3"];
 235   thus "~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3)" from [1;2;3;4] at 5;
 236   otherwise consider ["q:Point"] st "q ON l1 /\\ q ON l2 /\\ q ON l3" at 6;
 237   consider ["q':Point"] st "q' ON l1 /\\ q' ON l3 /\\
 238     !p'. p' ON l1 /\\ p' ON l3 ==> (p' = q')" from [5] by [DUAL_1] at 7;
 239   have "q = q'" from [6;7];
 240   so have "... = p1" from [2;4;7];
 241   hence contradiction from [1;3;6]];;
 242
 243 let DUAL_4 = theorem
 244  "!O. ?OP OQ OR. ~(OP = OQ) /\\ ~(OQ = OR) /\\ ~(OP = OR) /\\
 245     O ON OP /\\ O ON OQ /\\ O ON OR"
 246  [fix ["O:Point"];
 247   consider ["OP:Line"] st "O ON OP" by [LEMMA_1] at 1;
 248   consider ["p:Point"; "p':Point"; "p'':Point"] st
 249    "~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
 250       p ON OP /\\ p' ON OP /\\ p'' ON OP" by [AXIOM_4] at 2;
 251   have "~(p = O) \/ ~(p' = O)" from [2];
 252   so consider ["P:Point"] st "~(P = O) /\\ P ON OP" from [2] at 3;
 253   consider ["q:Point"; "q':Point"; "q'':Point"] st
 254    "~(q = q') /\\ ~(q' = q'') /\\ ~(q = q'') /\\
 255       ~(?l. q ON l /\\ q' ON l /\\ q'' ON l)" by [AXIOM_3] at 4;
 256   have "~(q ON OP) \/ ~(q' ON OP) \/ ~(q'' ON OP)" from [4];
 257   so consider ["Q:Point"] st "~(Q ON OP)" at 5;
 258   consider ["l:Line"] st "P ON l /\\ Q ON l" by [DUAL_2] at 6;
 259   consider ["r:Point"; "r':Point"; "r'':Point"] st
 260    "~(r = r') /\\ ~(r' = r'') /\\ ~(r = r'') /\\
 261       r ON l /\\ r' ON l /\\ r'' ON l" by [AXIOM_4] at 7;
 262   have "((r = P) \/ (r = Q) \/ ~(r = P) /\\ ~(r = Q)) /\\
 263     ((r' = P) \/ (r' = Q) \/ ~(r' = P) /\\ ~(r' = Q))";
 264   so consider ["R:Point"] st "R ON l /\\ ~(R = P) /\\ ~(R = Q)" from [7] at 8;
 265   consider ["OQ:Line"] st "O ON OQ /\\ Q ON OQ" by [DUAL_2] at 9;
 266   consider ["OR:Line"] st "O ON OR /\\ R ON OR" by [DUAL_2] at 10;
 267   take ["OP"; "OQ"; "OR"];
 268   have "~(O ON l)" from [1;3;5;6] by [AXIOM_1'];
 269   hence "~(OP = OQ) /\\ ~(OQ = OR) /\\ ~(OP = OR) /\\
 270     O ON OP /\\ O ON OQ /\\ O ON OR" from [1;3;5;6;8;9;10] by [AXIOM_1']];;