1 (* ========================================================================= *)
2 (* Mizar Light proof of duality in projective geometry. *)
3 (* ========================================================================= *)
5 current_prover := standard_prover;;
7 (* ------------------------------------------------------------------------- *)
8 (* Axioms for projective geometry. *)
9 (* ------------------------------------------------------------------------- *)
11 parse_as_infix("ON",(11,"right"));;
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)`;;
22 (* ------------------------------------------------------------------------- *)
23 (* To get round extreme slowness of MESON for one situation. *)
24 (* ------------------------------------------------------------------------- *)
26 let USE_PROJ_TAC [prth; proj_def] =
27 REWRITE_TAC[REWRITE_RULE[proj_def] prth];;
29 (* ------------------------------------------------------------------------- *)
30 (* The main result, via two lemmas. *)
31 (* ------------------------------------------------------------------------- *)
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;
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];
50 "!(ON):Point->Line->bool. projective(ON)
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]];;
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;
86 have "!l1 l2. ~(l1 = l2) ==> ?!p. p ON l1 /\\ p ON l2" at 5
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)"
94 assume "p' ON l1 /\\ p' ON l2" at 8;
96 so have "l1 = l2" from [1;7;8];
97 hence contradiction from [6]];
100 have "!p1 p2. ?l. p1 ON l /\\ p2 ON l" at 9
102 [fix ["p1:Point"; "p2:Point"];
105 qed from [0] by [LEMMA_1]];
106 [suppose "~(p1 = p2)";
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
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"
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
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)";
148 have "~(p0 ON l1)" at 22
151 so have "l1 = l0" from [1;16;17;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]];;
163 current_prover := sketch_prover;;
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)"
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"
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"
188 [fix ["p1:Point"; "p2:Point"];
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)"
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"
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)"
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"];
232 [otherwise have "OP = OQ";
233 hence contradiction];
236 thus "O ON OP /\\ O ON OQ /\\ O ON OR"];
238 have "!(ON):Point->Line->bool. projective (\l p. p ON l) ==> projective(ON)";