Update from HH
[hl193./.git] / 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