Mizarlight/duality.ml

   1 (* ========================================================================= *)
   2 (* Mizar Light proof of duality in projective geometry.                      *)
   3 (* ========================================================================= *)
   4
   5 current_prover := standard_prover;;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Axioms for projective geometry.                                           *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 parse_as_infix("ON",(11,"right"));;
  12
  13 let projective = new_definition
  14  `projective((ON):Point->Line->bool) <=>
  15         (!p p'. ~(p = p') ==> ?!l. p ON l /\ p' ON l) /\
  16         (!l l'. ?p. p ON l /\ p ON l') /\
  17         (?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  18                     ~(?l. p ON l /\ p' ON l /\ p'' ON l)) /\
  19         (!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  20                         p ON l /\ p' ON l /\ p'' ON l)`;;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* To get round extreme slowness of MESON for one situation.                 *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 let USE_PROJ_TAC [prth; proj_def] =
  27   REWRITE_TAC[REWRITE_RULE[proj_def] prth];;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* The main result, via two lemmas.                                          *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let LEMMA_1 = theorem
  34  "!(ON):Point->Line->bool. projective(ON) ==> !p. ?l. p ON l"
  35  [fix ["(ON):Point->Line->bool"];
  36   assume "projective(ON)" at 0;
  37   have "!p p'. ~(p = p') ==> ?!l. p ON l /\\ p' ON l"
  38     at 1 from [0] by [projective] using USE_PROJ_TAC;
  39   have "?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
  40                     ~(?l. p ON l /\\ p' ON l /\\ p'' ON l)"
  41     at 3 from [0] by [projective] using USE_PROJ_TAC;
  42   fix ["p:Point"];
  43   consider ["q:Point"; "q':Point"] st "~(q = q')" from [3];
  44   so have "~(p = q) \/ ~(p = q')";
  45   so consider ["l:Line"] st "p ON l" from [1];
  46   take ["l"];
  47   qed];;
  48
  49 let LEMMA_2 = theorem
  50  "!(ON):Point->Line->bool. projective(ON)
  51    ==> !p1 p2 q l l1 l2.
  52      p1 ON l /\\ p2 ON l /\\ p1 ON l1 /\\ p2 ON l2 /\\ q ON l2 /\\
  53      ~(q ON l) /\\ ~(p1 = p2) ==> ~(l1 = l2)"
  54  [fix ["(ON):Point->Line->bool"];
  55   assume "projective(ON)" at 0;
  56   have "!p p'. ~(p = p') ==> ?!l. p ON l /\\ p' ON l"
  57     at 1 from [0] by [projective] using USE_PROJ_TAC;
  58   fix ["p1:Point"; "p2:Point"; "q:Point"; "l:Line"; "l1:Line"; "l2:Line"];
  59   assume "p1 ON l" at 5;
  60   assume "p2 ON l" at 6;
  61   assume "p1 ON l1" at 7;
  62   assume "p2 ON l2" at 9;
  63   assume "q ON l2" at 10;
  64   assume "~(q ON l)" at 11;
  65   assume "~(p1 = p2)" at 12;
  66   assume "l1 = l2" at 13;
  67   so have "p1 ON l2" from [7];
  68   so have "l = l2" from [1;5;6;9;12];
  69   hence contradiction from [10;11]];;
  70
  71 let PROJECTIVE_DUALITY = theorem
  72  "!(ON):Point->Line->bool. projective(ON) ==> projective (\l p. p ON l)"
  73  [fix ["(ON):Point->Line->bool"];
  74   assume "projective(ON)" at 0;
  75   have "!p p'. ~(p = p') ==> ?!l. p ON l /\\ p' ON l"
  76     at 1 from [0] by [projective] using USE_PROJ_TAC;
  77   have "!l l'. ?p. p ON l /\\ p ON l'"
  78     at 2 from [0] by [projective] using USE_PROJ_TAC;
  79   have "?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
  80                     ~(?l. p ON l /\\ p' ON l /\\ p'' ON l)"
  81     at 3 from [0] by [projective] using USE_PROJ_TAC;
  82   have "!l. ?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
  83                         p ON l /\\ p' ON l /\\ p'' ON l"
  84     at 4 from [0] by [projective] using USE_PROJ_TAC;
  85 (* dual of axiom 1 *)
  86   have "!l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\\ p ON l2" at 5
  87   proof
  88    [fix ["l1:Line"; "l2:Line"];
  89     assume "~(l1 = l2)" at 6;
  90     consider ["p:Point"] st "p ON l1 /\\ p ON l2" at 7 from [2];
  91     have "!p'. p' ON l1 /\\ p' ON l2 ==> (p' = p)"
  92     proof
  93      [fix ["p':Point"];
  94       assume "p' ON l1 /\\ p' ON l2" at 8;
  95       assume "~(p' = p)";
  96       so have "l1 = l2" from [1;7;8];
  97       hence contradiction from [6]];
  98     qed from [7]];
  99 (* dual of axiom 2 *)
 100   have "!p1 p2. ?l. p1 ON l /\\ p2 ON l" at 9
 101   proof
 102    [fix ["p1:Point"; "p2:Point"];
 103     per cases
 104      [[suppose "p1 = p2";
 105        qed from [0] by [LEMMA_1]];
 106       [suppose "~(p1 = p2)";
 107        qed from [1]]]];
 108 (* dual of axiom 3 *)
 109   have "?l1 l2 l3. ~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3) /\\
 110                     ~(?p. p ON l1 /\\ p ON l2 /\\ p ON l3)" at 10
 111   proof
 112    [consider ["p1:Point"; "p2:Point"; "p3:Point"] st
 113       "~(p1 = p2) /\\ ~(p2 = p3) /\\ ~(p1 = p3) /\\
 114                     ~(?l. p1 ON l /\\ p2 ON l /\\ p3 ON l)" from [3] at 11;
 115     have "~(p1 = p3)" from [11];
 116     so consider ["l1:Line"] st "p1 ON l1 /\\ p3 ON l1 /\\
 117         !l'. p1 ON l' /\\ p3 ON l' ==> (l1 = l')" from [1] at 12;
 118     have "~(p2 = p3)" from [11];
 119     so consider ["l2:Line"] st "p2 ON l2 /\\ p3 ON l2 /\\
 120         !l'. p2 ON l' /\\ p3 ON l' ==> (l2 = l')" from [1] at 13;
 121     have "~(p1 = p2)" from [11];
 122     so consider ["l3:Line"] st "p1 ON l3 /\\ p2 ON l3 /\\
 123         !l'. p1 ON l' /\\ p2 ON l' ==> (l3 = l')" from [1] at 14;
 124     take ["l1"; "l2"; "l3"];
 125     thus "~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3)" from [11;12;13;14] at 15;
 126     assume "?q. q ON l1 /\\ q ON l2 /\\ q ON l3";
 127     so consider ["q:Point"] st "q ON l1 /\\ q ON l2 /\\ q ON l3";
 128     so have "(p1 = q) /\\ (p2 = q) /\\ (p3 = q)" from [5;12;13;14;15];
 129     hence contradiction from [11]];
 130 (* dual of axiom 4 *)
 131   have "!p0. ?l0 L1 L2. ~(l0 = L1) /\\ ~(L1 = L2) /\\ ~(l0 = L2) /\\
 132                         p0 ON l0 /\\ p0 ON L1 /\\ p0 ON L2"
 133   proof
 134    [fix ["p0:Point"];
 135     consider ["l0:Line"] st "p0 ON l0" from [0] by [LEMMA_1] at 16;
 136     consider ["p:Point"] st "~(p = p0) /\\ p ON l0" from [4] at 17;
 137     consider ["q:Point"] st "~(q ON l0)" from [3] at 18;
 138     so consider ["l1:Line"] st "p ON l1 /\\ q ON l1" from [1;16] at 19;
 139     consider ["r:Point"] st "r ON l1 /\\ ~(r = p) /\\ ~(r = q)" at 20
 140     proof
 141      [consider ["r1:Point"; "r2:Point"; "r3:Point"] st
 142        "~(r1 = r2) /\\ ~(r2 = r3) /\\ ~(r1 = r3) /\\
 143                         r1 ON l1 /\\ r2 ON l1 /\\ r3 ON l1" from [4] at 21;
 144       so have "~(r1 = p) /\\ ~(r1 = q) \/
 145         ~(r2 = p) /\\ ~(r2 = q) \/
 146         ~(r3 = p) /\\ ~(r3 = q)";
 147       qed from [21]];
 148     have "~(p0 ON l1)" at 22
 149     proof
 150      [assume "p0 ON l1";
 151       so have "l1 = l0" from [1;16;17;19];
 152       qed from [18;19]];
 153     so have "~(p0 = r)" from [20];
 154     so consider ["L1:Line"] st "r ON L1 /\\ p0 ON L1" from [1] at 23;
 155     consider ["L2:Line"] st "q ON L2 /\\ p0 ON L2" from [1;16;18] at 24;
 156     take ["l0"; "L1"; "L2"];
 157     thus "~(l0 = L1)" from [0;17;19;20;22;23] by [LEMMA_2];
 158     thus "~(L1 = L2)" from [0;19;20;22;23;24] by [LEMMA_2];
 159     thus "~(l0 = L2)" from [18;24];
 160     thus "p0 ON l0 /\\ p0 ON L2 /\\ p0 ON L1" from [16;24;23]];
 161   qed from [5;9;10] by [projective]];;
 162
 163 current_prover := sketch_prover;;
 164
 165 let PROJECTIVE_DUALITY = theorem
 166  "!(ON):Point->Line->bool. projective(ON) = projective (\l p. p ON l)"
 167  [have "!(ON):Point->Line->bool. projective(ON) ==> projective (\l p. p ON l)"
 168   proof
 169    [fix ["(ON):Point->Line->bool"];
 170     assume "projective(ON)";
 171     have "!p p'. ~(p = p') ==> ?!l. p ON l /\\ p' ON l" at 1;
 172     have "!l l'. ?p. p ON l /\\ p ON l'" at 2;
 173     have "?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
 174                      ~(?l. p ON l /\\ p' ON l /\\ p'' ON l)" at 3;
 175     have "!l. ?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
 176                          p ON l /\\ p' ON l /\\ p'' ON l" at 4;
 177   (* dual of axiom 1 *)
 178     have "!l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\\ p ON l2"
 179     proof
 180      [fix ["l1:Line"; "l2:Line"];
 181       otherwise have "?p p'. ~(l1 = l2) /\\ ~(p = p') /\\
 182         p ON l1 /\\ p' ON l1 /\\ p ON l2 /\\ p' ON l2";
 183       so have "l1 = l2" from [1];
 184       hence contradiction];
 185   (* dual of axiom 2 *)
 186     have "!p1 p2. ?l. p1 ON l /\\ p2 ON l"
 187     proof
 188      [fix ["p1:Point"; "p2:Point"];
 189       qed from [1]];
 190   (* dual of axiom 3 *)
 191     have "?l1 l2 l3. ~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3) /\\
 192                      ~(?p. p ON l1 /\\ p ON l2 /\\ p ON l3)"
 193     proof
 194      [consider ["p1:Point"; "p2:Point"; "p3:Point"] st
 195         "~(p1 = p2) /\\ ~(p2 = p3) /\\ ~(p1 = p3) /\\
 196          ~(?l. p1 ON l /\\ p2 ON l /\\ p3 ON l)" from [3];
 197       consider ["l1:Line"] st "p1 ON l1 /\\ p3 ON l1 /\\
 198          !l'. p1 ON l' /\\ p3 ON l' ==> (l1 = l')" from [1];
 199       consider ["l2:Line"] st "p2 ON l2 /\\ p3 ON l2 /\\
 200          !l'. p2 ON l' /\\ p3 ON l' ==> (l2 = l')" from [1];
 201       consider ["l3:Line"] st "p1 ON l3 /\\ p2 ON l3 /\\
 202          !l'. p1 ON l' /\\ p2 ON l' ==> (l3 = l')" from [1];
 203       take ["l1"; "l2"; "l3"];
 204       thus "~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3)";
 205       assume "?q. q ON l1 /\\ q ON l2 /\\ q ON l3";
 206       so consider ["q:Point"] st "q ON l1 /\\ q ON l2 /\\ q ON l3";
 207       have "(q = p1) \/ (q = p2) \/ (q = p3)";
 208       so have "p1 ON l2 \/ p2 ON l1 \/ p3 ON l3";
 209       hence contradiction];
 210   (* dual of axiom 4 *)
 211     have "!O. ?OP OQ OR. ~(OP = OQ) /\\ ~(OQ = OR) /\\ ~(OP = OR) /\\
 212                          O ON OP /\\ O ON OQ /\\ O ON OR"
 213     proof
 214      [fix ["O:Point"];
 215       consider ["OP:Line"] st "O ON OP";
 216       consider ["P:Point"] st "~(P = O) /\\ P ON OP";
 217       have "?Q:Point. ~(Q ON OP)"
 218       proof
 219        [otherwise have "!Q:Point. Q ON OP";
 220         so have "~(?p p' p''. ~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\
 221                     ~(?l. p ON l /\\ p' ON l /\\ p'' ON l))";
 222         hence contradiction from [3]];
 223       so consider ["Q:Point"] st "~(Q ON OP)";
 224       consider ["l:Line"] st "P ON l /\\ Q ON l" from [1];
 225       consider ["R:Point"] st "R ON l /\\ ~(R = P) /\\ ~(R = Q)" from [4];
 226       have "~(P = Q) /\\ ~(R = P) /\\ ~(R = Q)";
 227       consider ["OQ:Line"] st "O ON OQ /\\ Q ON OQ";
 228       consider ["OR:Line"] st "O ON OR /\\ R ON OR";
 229       take ["OP"; "OQ"; "OR"];
 230       thus "~(OP = OQ)"
 231       proof
 232        [otherwise have "OP = OQ";
 233         hence contradiction];
 234       thus "~(OQ = OR)";
 235       thus "~(OP = OR)";
 236       thus "O ON OP /\\ O ON OQ /\\ O ON OR"];
 237     qed];
 238   have "!(ON):Point->Line->bool. projective (\l p. p ON l) ==> projective(ON)";
 239   qed];;
 240