-
Notifications
You must be signed in to change notification settings - Fork 0
/
07_EuclideanGeometry.v
23320 lines (22668 loc) · 831 KB
/
07_EuclideanGeometry.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
ON CONSTRUCTIVE-DEDUCTIVE METHOD FOR PLANE EUCLIDEAN GEOMETRY
Evgeny V. Ivashkevich
January 29, 2019
Introduction
1. The logic of Euclid
Euclidean geometry [1] studies not only the properties of geometric figures,
but also the rules of their construction. Propositions, that we encounter
in Euclid's Elements, can be divided onto two types: problems and theorems.
To solve a problem one needs to find a sequence of elementary actions
(postulates) that leads to the construction of a figure with the required
properties. The set of allowed elementary actions is completely determined
by chosen geometric tools (a pencil, a straightedge and a collapsing compass)
and provides us with the instructions on how to handle these instruments.
Pencil helps us to draw some points on a plane. Ruler helps us to draw a
straight lines passing through two distinct points. Compass helps us to
draw a circle through a given point and center of the circle.
To prove a theorem one needs to find a sequence of elementary inferences
(axioms) that confirms the presence of a certain property in a given figure.
The set of allowed elementary inferences describes some basic properties of
figures (points, lines, circles and triangles) that were constructed using
the geometric tools that we have chosen.
A distinctive feature of Euclid's logic, is that it is not purely
deductive [2-3]. Postulates and problems represent an important constructive
part of Euclid's logic which cannot be completely separated from the
deductive one. Indeed, proofs of Euclid's theorems often require auxiliary
constructions, while problem solutions often require intermediate proofs
to ensure applicability of postulates or previously solved problems.
So, the inherent logic of Euclid's Elements can be considered as
constructive-deductive.
Later interpreters of Euclid, however, sought to reduce his theory to purely
predicate logic, reformulating all its problems into existential theorems.
In other words, they treated all objects of the theory as idealized and
pre-existing and considered every problem not as instruction on how to
construct the object with the required properties, but simply as propositional
proof of object's existence.
This forced reduction of constructive-deductive logic of Euclid to purely
propositional logic was not without its difficulties. Indeed, in the logic of
Euclid, every object under consideration must first be constructed. While in
purely propositional logic the mere existence of an object with the required
properties can be proved indirectly. One first assumes that such an object
does not exist, and then prove that this assumption leads to a contradiction.
Such an indirect proof by contradiction relies upon so-called "the law of
the excluded middle" first formulated by Aristotle. This law states that
either an assertion or its negation must be true.
Intuitionistic logic [4-6] was proposed to prohibit all indirect proofs of
existence. The main idea of the method was to reduce further not only the
constructive-deductive logic of Euclid, but also the classical propositional
logic. Namely, intuitionists suggested to exclude "the law of the excluded
middle" from the inference rules of propositional logic. As a results,
from the existential proofs of the intuitionistic logic one do can reproduce
original Euclid's constructions and vice versa.
Despite of the apparent success, this reduction of classical logic cannot
be considered satisfactory. Indeed, let us recall that Euclid builds his
theory using a limited set of geometric tools (a pencil, a straightedge and
a collapsing compass). This means, that translating postulates and problems
into existential axioms and theorems, and then limiting ourselves by the
rules of intuitionistic logic, we shall be able to prove existence of only
those geometric figures that can be constructed with this limited set of
geometric tools. However, it is well known that not all geometric figures
can be constructed by these simple tools. For example, it is impossible to
do an angle trisection. Obviously, this does not mean that the rays
that divide an angle onto three equal parts do not exist. To get around
this new difficulty, intuitionists would have to change the original
Euclidean postulates, thereby introducing some new idealized tools that
would give them the ability to construct more complex geometric figures.
2. Hilbert's system of axioms
The standards of mathematical rigor have changed dramatically since Euclid
wrote his Elements. Subsequently, many mathematicians added missing but
implicitly used statements to the original list of Euclid's postulates and
axioms. The culmination of this development was a small book by german
mathematician David Hilbert "Foundations of geometry" [6].
Although the overall approach of Hilbert is fairly close in spirit to
that of Euclid, yet in some respects it deviates substantially from it.
Let us discuss these differences.
a) First of all, we have to note that Hilbert does not adhere to the
constructive-deductive logic of Euclid. In fact, Hilbert was one of the main
proponents of the existential approach and hence reduced all the postulates
and problems of Euclid's Elements to purely existential statements within
classical logic.
b) Another striking feature of the Hilbert's axioms is the complete absence of
circles. Instead of circles, Hilbert focuses all his attention on the
properties of angles. Moreover, instead of Euclid's tools (a pencil,
a straightedge and a collapsing compass), Hilbert introduces more complicated
instruments to transfer both segments and angles. Surprisingly, those same
authors who criticized Euclid for his method of superposition (which is
nothing more than an auxiliary tool for existential triangle transfer) seem
to accept Hilbert's tool for angle transfer without any questions.
Since without compass it is not possible to reproduce many propositions from
Euclid's Elements, Hilbert followers [8,9] have to introduce some additional
"principles": such as line-circle intersection and circle-circle
intersection. These "principles" are nothing but additional postulates that
describe simple constructions by straightedge and compass. However, those
authors do not add these "principles" to the list of Hilbert's axioms.
Instead,they treat them as being derived from the Hilbert continuity axiom.
Needless to say, that if such a derivation is actually provided by those
authors, it goes far beyond Euclid's original approach.
c) As for the treatment of angles on which Hilbert seems to focus instead of
circles, it cannot be considered completely satisfactory either. The thing
is that, Hilbert defines only convex angles (greater than null angle and
less than straight angle). As a result of this truncated definition, it is
impossible to universally define the addition of two arbitrary convex
angles. Indeed, the sum of the two convex angles in Hilbert's theory is
defined only if the resulting angle is also convex.
d) In the last edition of his book, to define area of an arbitrary polygon
Hilbert introduces the idea of triangle orientation. However, Hilbert did
not provide the reader with any clear definition of the triangle orientation
and has not studied the properties of the concept within his system of axioms.
e) Hilbert introduces a number of separate congruence axioms for segments and
angles. In Euclid's approach, on the contrary, the lengths of segments,
angular measures and areas were all considered as "quantities" that obey the
same universal axioms: "two quantities equal to the third are equal to each
other", etc. In other words, for Euclid, "quantities" are more general
concepts than segments and angles themselves. As such, Euclid considers
"quantities" as classes o congruence.
3. Motivation and results
In this work, we return to Euclid's original constructive-deductive logic.
This means that we are going to use classical logic for propositions and
intuitionistic logic for constructions. In other words, we shall clearly
distinguish between existential statements and real constructions.
The same applies to disjunction. We shall consider both propositional
disjunctions which is a logical assertion that one of the two alternatives
is true without specifying which one, and constructive disjunction, which is
a practical algorithm that for every configuration of objects on the plane
decides which one of the two alternatives actually takes place.
We will show that the "Calculus of Constructions" (CoC), as it was
implemented in the Coq Proof Assistant, suits ideally for the
constructive-deductive logic of Euclid. In the CoC we have two sorts:
"Prop" and "Set". The first one is inhabited by propositions and their
proofs, while the second by constructed objects and their specifications
(required properties). Without contradiction we may accept classical
logic for proofs in the "Prop" sort, and at the same time limit ourselves
to intuitionistic logic for constructions in the "Set" sort. As a result,
our constructions will be limited to only those that can be performed with
our simple tools (a pencil, a straightedge and a collapsing compass),
while we shall be able to prove propositional existence of more complex
geometric figures.
We abandon Hilbert's postulates for segment and angle transfer and replace
them with simple versions of Euclid's postulates for collapsing compass
whose legs fold up when the compass is lifted off the paper. Moreover,
constructive-deductive logic of Euclid also gives us the opportunity to
formalize Euclid's "method of superposition". To prove triangle congruence
theorems, Euclid conjectured that every triangle could be moved and placed
over another triangle so that their respective sides and angles could be
compared. In this interpretation, the method of superposition seems to be
quite a strong postulate, which makes it possible to move, rotate and flip
triangles on the plane. That is why it is not very popular nowadays, and
it was questioned even in the times of Euclid. In our interpretation the
method of superposition turns into an axiom about the existence of an equal
triangle anywhere on the plane. The actual construction of equal triangle
can be done later by our standard tools (a pencil, a straightedge
and a collapsing compass).
We define angles as a pairs of rays originating from the same point and prove
that addition of angles can be defined uniformly for all angles (modulo the
full angle). Then we define the orientation of angles on the plane and use
this concept to define a subclass of convex angles, thus returning to
the Hilbert's definition of angle. As a results, all Hilbert axioms can
be derived form our formalization of Euclid's constructive-deductive method.
We also replaced congruence axioms for segments and angles by
their classes of congruences and consider the classes as definitions of
Euclid's "quantities". Such an approach simplifies our formalization
of Euclid's constructive-deductive method in the Coq Proof Assistant.
Finally, we demonstrate that from this set of constructive axioms it is
possible to reproduce all the Von Plato (for constructive incidence geometry)
and Hilbert axioms exactly in the form proposed by Gilles Kahn [10] and
Julien Narboux et al [11].
I would like to thank Andrei Rodin for interesting discussions about
Euclid's methods and phylosophy. I am also grateful to Julien Narboux and
Yves Bertot for drawing my attention to references [12-14] on recent
development in the field.
BIBLIOGRAPHY
[1] Euclid, "Elements",
Book I, Alexandria, (300 BC)
[2] Andrei Rodin, "On Constructive Axiomatic Method",
Logique et Analyse, Vol 61, No 242 (2018)
[3] Andrei Rodin, "Euclid's Mathematics in Context of Plato's and
Aristotle's Philosophy", Moscow, Nauka, (2003)
[4] Arend Heyting, "Axiomatic Projective Geometry",
Elsevier Science (2008)
[5] Jan Von Plato, "The Axioms of Constructive Geometry",
Annals of Pure and Applied Logic 76, 169-200 (1995)
[6] Michael Beeson, "A Constructive Version of Tarski's Geometry",
Annals of Pure and Applied Logic 166 (11) 1199-1273 (2015)
[7] David Hilbert, "Grundlagen der Geometrie",
7th ed., (1930)
[8] Marvin Jay Greenberg, "Euclidean and non-Euclidean geometries",
W. H. Freeman, New York, 2008.
[9] Robin Hartshorne, "Geometry: Euclid and beyond",
Springer, 2000
[10] Gilles Kahn, "Constructive Geometry following Jan von Plato",
https://github.com/coq-contribs/constructive-geometry
[11] Julien Narboux et al, "GeoCoq Project",
https://geocoq.github.io/GeoCoq/
see also references therein.
[12] Kellison, A., Bickford, M. & Constable, R. "Implementing Euclid's
straightedge and compass constructions in type theory",
Ann Math Artif Intell (2018).
http://www.nuprl.org/MathLibrary/geometry/
[13] Michael Beeson,"Constructive Geometry and the Parallel Postulate",
The Bulletin of Symbolic Logic, 22(1), 1-104 (2016).
Other publications by Michael Beeson
http://www.michaelbeeson.com/research/papers/pubs.html
[14] Michael Beeson, Julien Narboux, Freek Wiedijk, "Proof-checking Euclid",
Annals of Mathematics and Artificial Intelligence,
Springer Verlag, 2019, pp.53.
*)
Require Import Classical Setoid Morphisms.
(*****************************************************************************)
(** DEFINITIONS *)
(*****************************************************************************)
Record Duo { U : Set } : Set
:= BuildDuo { d1 : U; d2 : U }.
Notation " {{ A , B }} "
:= ({| d1 := A; d2 := B |})(at level 60).
Record Trio { U : Set } : Set
:= BuildTrio { t1 : U; t2 : U; t3 : U }.
Notation " {{ A , B , C }} "
:= ({| t1 := A; t2 := B; t3 := C |})(at level 60).
Record Duple { U : Set } { P : U -> U -> Prop } : Set
:= BuildDuple { da : U; db : U; dp : P da db }.
Notation " {{ A # B | AB }} "
:= ({| da := A; db := B; dp := AB |})(at level 60).
Record Triple { U : Set } { P : U -> U -> U -> Prop } : Set
:= BuildTriple { ta : U; tb : U; tc : U; tp : P ta tb tc }.
Notation " {{ A # B # C | ABC }} "
:= ({| ta := A; tb := B; tc := C; tp := ABC |})(at level 60).
Class Declarations :=
{
Point : Set;
Line : Set;
Incident : Point -> Line -> Prop;
Between : Point -> Point -> Point -> Prop;
}.
Notation " [ A @ x ] "
:= (Incident A x)
(at level 60).
Notation " [ A , B @ x ] "
:= ([ A @ x ] /\ [ B @ x ])
(at level 60).
Notation " [ A @ x , y ] "
:= ([ A @ x ] /\ [ A @ y ])
(at level 60).
Notation " [ A , B , C @ x ] "
:= ([ A @ x ] /\ [ B @ x ] /\ [ C @ x ])
(at level 60).
Notation " [ A , B @ x , y ] "
:= ([ A, B @ x ] /\ [ A, B @ y ])
(at level 60).
Notation " [ A @ x , y , z ] "
:= ([ A @ x ] /\ [ A @ y ] /\ [ A @ z ])
(at level 60).
Notation " [ A , B , C , D @ x ] "
:= ([ A @ x ] /\ [ B @ x ] /\ [ C @ x ] /\ [ D @ x ])
(at level 60).
Notation " [ A , B , C , D , E @ x ] "
:= ([ A @ x ] /\ [ B @ x ] /\ [ C @ x ] /\ [ D @ x ] /\ [ E @ x ])
(at level 60).
Notation " [ A , B , C , D , E , F @ x ] "
:= ([ A @ x ] /\ [ B @ x ] /\ [ C @ x ]
/\ [ D @ x ] /\ [ E @ x ] /\ [ F @ x ])
(at level 60).
Notation " [ A , B , C @ x , y ] "
:= ([ A , B , C @ x ] /\ [ A , B , C @ y ])
(at level 60).
Notation " [ A , B @ x , y , z ] "
:= ([ A @ x , y , z ] /\ [ B @ x , y , z ])
(at level 60).
Notation " [ A @ x , y , z , t ] "
:= ([ A @ x ] /\ [ A @ y ] /\ [ A @ z ] /\ [ A @ t ])
(at level 60).
Notation " [ A , B ] "
:= (exists x : Line, [ A , B @ x ])
(at level 60).
Notation " [ A , B , C ] "
:= (exists x : Line, [ A , B , C @ x ])
(at level 60).
Notation " [ A , B , C , D ] "
:= (exists x : Line, [ A , B , C , D @ x ])
(at level 60).
Notation " [ A , B , C , D , E ] "
:= (exists x : Line, [ A , B , C , D , E @ x ])
(at level 60).
Notation " [ A , B , C , D , E , F ] "
:= (exists x : Line, [ A , B , C , D , E , F @ x ])
(at level 60).
Notation " [ A # B # C ] " (* Hilbert's between relation *)
:= (Between A B C)
(at level 60).
Notation " [ A ; B # C ] "
:= ([ A # B # C ] \/ (A = B /\ B <> C))
(at level 60).
Notation " [ A # B ; C ] "
:= ([ A # B # C ] \/ (A <> B /\ B = C))
(at level 60).
Notation " [ A ; B ; C ] " (* Tarski's between relation *)
:= ([ A # B # C ] \/ A = B \/ B = C)
(at level 60).
Notation " [ A # B # C # D ] "
:= ([ A # B # C ] /\
[ A # B # D ] /\
[ A # C # D ] /\
[ B # C # D ])
(at level 60).
Notation " [ A # B # C # D # E ] "
:= ([ A # B # C # D ] /\
[ A # B # C # E ] /\
[ A # B # D # E ] /\
[ A # C # D # E ] /\
[ B # C # D # E ])
(at level 60).
Class Definitions `(dc : Declarations) :=
{
Convergent (x y : Line) : Prop
:= (x <> y) /\ (exists A : Point, [ A @ x, y ]);
Parallel (x y : Line) : Prop
:= (~ Convergent x y);
SameRay (O : Point)(A B : Point) : Prop
:= O <> A /\ O <> B /\ [ A, O, B ] /\ ~ [ A # O # B ];
OppositeSide (x : Line)(A B : Point) : Prop
:= ~ [ A @ x ] /\ ~ [ B @ x ] /\ (exists O, [ O @ x ] /\ [ A # O # B ]);
SameSide (x : Line)(A B : Point) : Prop
:= ~ [ A @ x ] /\ ~ [ B @ x ] /\ ~ (exists O, [ O @ x ] /\ [ A # O # B ]);
SameHalfplane (O A B C : Point) : Prop
:= O <> A /\ exists x : Line, [ O @ x ] /\ [ A @ x ] /\ SameSide x B C;
OppositeHalfplane (O A B C : Point) : Prop
:= O <> A /\ exists x : Line, [ O @ x ] /\ [ A @ x ] /\ OppositeSide x B C;
Segment
:= @Duo Point;
BuildSegment
:= @BuildDuo Point;
Triangle
:= @Triple Point (fun A B C => ~ [ A, B, C ]);
BuildTriangle
:= @BuildTriple Point (fun A B C => ~ [ A, B, C ]);
Ray
:= @Duple Point (fun A B => A <> B);
BuildRay
:= @BuildDuple Point (fun A B => A <> B);
EqRays (a b : Ray) : Prop
:= (da a = da b) /\ SameRay (da a)(db a)(db b);
OpRays (a b : Ray) : Prop
:= (da a = da b) /\ [ db a # da a # db b ];
Sector
:= @Duple Ray (fun a b => da a = da b);
BuildSector
:= @BuildDuple Ray (fun a b => da a = da b);
nColRs (a b : Ray) : Prop
:= da a = da b /\ ~ [ (db a), (da a), (db b) ];
Flag
:= @Duple Ray (fun a b => nColRs a b);
BuildFlag
:= @BuildDuple Ray (fun a b => nColRs a b);
}.
Notation " ![ a , b ] "
:= ([ da a, db a, da b, db b ])
(at level 60).
Notation " ![ a , b , c ] "
:= ([ da a, db a, da b, db b, da c, db c ])
(at level 60).
Notation " ![ a # b ] "
:= (nColRs a b)
(at level 60).
Notation " x >< y "
:= (Convergent x y)
(at level 60).
Notation " [ O # A , B ] "
:= (SameRay O A B)
(at level 60).
Notation " [ O ; A , B ] "
:= ([ O # A , B ] \/ O = A \/ O = B)
(at level 60).
Notation " [ A | x | B ] "
:= (OppositeSide x A B)
(at level 60).
Notation " [ x | A , B ] "
:= (SameSide x A B)
(at level 60).
Notation " [ O # A | B , C ] "
:= (SameHalfplane O A B C)
(at level 60).
Notation " [ B | O # A | C ] "
:= (OppositeHalfplane O A B C)
(at level 60).
Notation " [ O | A ; B ; C ] "
:= ([ O # A | B, C ] /\ [ O # C | B, A ])
(at level 60).
Notation " a == b "
:= (EqRays a b)
(at level 60).
Notation " a =/= b "
:= (~ EqRays a b)
(at level 60).
Notation " a <==> b "
:= (OpRays a b)
(at level 60).
Notation " a <=/=> b "
:= (~ OpRays a b)
(at level 60).
Notation " x || y "
:= (Parallel x y).
Class Quantities `(df : Definitions) :=
{(* This Class substitutes congruence axioms of Hilbert. We consider
Hilbert's "congruence classes" as "quanitites" in Euclud's Elements.
Thus, we consider this Class as the definition of those quantities.
Since in our subsequent geometric axioms we do not construct Length and
Angle 'per se', we do not assume that DrawSegment and DrawSector functions
do construct some new points and rays on the plane. Rather, they refer to
earlier constructed points and rays.
*)
Length : Set;
Ruler : Segment -> Length;
DrawSegment : forall d : Length, { s : Segment | Ruler s = d };
Angle : Set;
Protractor : Sector -> Angle;
DrawSector : forall a : Angle, { s : Sector | Protractor s = a };
}.
Notation " [| A , B |] "
:= (Ruler ({{ A, B }}))
(at level 60).
Notation " [| a , b | ab |] "
:= (Protractor ({{ a # b | ab }}))
(at level 60).
Notation " [| A , O , B | OA , OB |] "
:= ([| {{ O # A | OA }} , {{ O # B | OB }} | eq_refl O |])
(at level 60).
Notation " [ A -- O -- B ] "
:= ([ A # O # B ] /\ [| O, A |] = [| O, B |])
(at level 60).
Class Orientations `(qs : Quantities) :=
{(* This class does not contain any additional postulates or axioms.
It will be instantiated later based on the postulates and axioms of
points, lines and circles. This class is placed here for a
technical reasons. It helps us to define the convex angles right here,
at the very beginning of the file. Otherwise we woud have to postpone
the definition of the convex angles together with angle axioms
untill we study all the properties of triangle orientations on the plane.
*)
ConvexFlag : Flag -> bool;
ConvexAngleRs (a b : Ray)(diab : ![ a # b ]) : Angle
:= match ConvexFlag ({{ a # b | diab }}) with
| true => [| a, b | proj1 diab |]
| false => [| b, a | eq_sym (proj1 diab) |]
end;
nColPs_DiPs : forall (A O B : Point),
~ [ A, O, B ] -> O <> A /\ O <> B /\ A <> B;
ConvexAnglePs (A O B : Point)(nColAOB : ~ [A, O, B]) : Angle
:= match nColPs_DiPs A O B nColAOB with
| conj nOeqA (conj nOeqB _) =>
let a := {{ O # A | nOeqA }} in
let b := {{ O # B | nOeqB }} in
ConvexAngleRs a b (conj eq_refl nColAOB)
end;
nCol_a : forall (A B C : Point),
~ [ A, B, C ] -> ~ [ B, C, A ];
nCol_b : forall (A B C : Point),
~ [ A, B, C ] -> ~ [ C, A, B ];
EqTriangle (A B : Triangle)
:= [| ta A, tb A |] = [| ta B, tb B |]
/\ [| tb A, tc A |] = [| tb B, tc B |]
/\ [| tc A, ta A |] = [| tc B, ta B |]
/\ ConvexAnglePs (ta A)(tb A)(tc A)(tp A)
= ConvexAnglePs (ta B)(tb B)(tc B)(tp B)
/\ ConvexAnglePs (tb A)(tc A)(ta A)(nCol_a (ta A)(tb A)(tc A)(tp A))
= ConvexAnglePs (tb B)(tc B)(ta B)(nCol_a (ta B)(tb B)(tc B)(tp B))
/\ ConvexAnglePs (tc A)(ta A)(tb A)(nCol_b (ta A)(tb A)(tc A)(tp A))
= ConvexAnglePs (tc B)(ta B)(tb B)(nCol_b (ta B)(tb B)(tc B)(tp B));
}.
Notation " % F "
:= (ConvexFlag F)
(at level 70).
Notation " [| a # b | diab |] "
:= (ConvexAngleRs a b diab)
(at level 60).
Notation " [| A # O # B | nColAOB |] "
:= (ConvexAnglePs A O B nColAOB)
(at level 60).
Notation " A :=: B "
:= (EqTriangle A B)
(at level 60).
(*****************************************************************************)
(** AXIOMS AND POSTULATES *)
(*****************************************************************************)
Class Points `(df : Definitions) :=
{
(** P1 *)
DrawPoint :
{ A : Point | A = A };
(** P2 *)
DrawDistinctPoint : forall (A : Point),
{ B : Point | A <> B };
(** P3, Arend Heyting *)
DecidePointsDistinction : forall (A B C : Point),
A <> C
-> { A <> B } + { B <> C };
}.
Class Lines `(pt : Points) :=
{
(** P4 *)
DrawPointOnLine : forall (x : Line),
{ A : Point | [ A @ x ] };
(** P5 *)
DrawDistinctPointOnLine : forall (A : Point)(x : Line),
[ A @ x ]
-> { B : Point | A <> B /\ [ B @ x ] };
(** P6 *)
DrawPointApartLine : forall (x : Line),
{ A : Point | ~ [ A @ x ] };
(** P7, Point-Point Extension *)
DrawExtensionLinePP : forall (A B : Point),
A <> B
-> { x : Line | [ A, B @ x ] };
(** P8, Jan Von Plato *)
DecideLineApartTwoPoints : forall (A B : Point)(x y : Line),
A <> B
-> [ A, B @ x ]
-> x <> y
-> { ~ [ A @ y ] } + { ~ [ B @ y ] };
(** P9, Line-Line Intersection *)
DrawIntersectionPointLL : forall (x y : Line),
x >< y
-> { A : Point | [ A @ x, y ] };
}.
Class Circles `(ln : Lines)(qs : Quantities df) :=
{(* Note that we formalize here collapsing compas of Euclid.
So, the circle is defined by any two poins - circle's center and arbitrary
point on the circle. Circles with null radius are also permitted.
*)
(** A1a *)
BetPs_DiPs : forall (A B C : Point),
[ A # B # C ]
-> A <> C;
(** A1b *)
BetPs_ColPs : forall (A B C : Point),
[ A # B # C ]
-> [ A, B, C ];
(** A1c *)
BetPs_sym : forall (A B C : Point),
[ A # B # C ]
-> [ C # B # A ];
(** A1d *)
BetPs_nBetPerPs :
forall (A B C : Point),
[ A # B # C ]
-> ~ [ B # A # C ];
(** P10, Morits Pasch *)
DecideTwoSides : forall (A B C : Point)(x : Line),
~ [ B @ x ]
-> [ A | x | C ]
-> { [ A | x | B ] } + { [ B | x | C ] };
(** A2 *)
SegPs_sym : forall (A B : Point),
[| A, B |] = [| B, A |];
(** A3 : *)
EqSgs_EqPs : forall (A B C : Point),
[| A, B |] = [| C, C |]
<-> A = B;
(** P11, Line-Circle Intersection *)
DrawIntersectionPointLC : forall (O A B : Point),
O <> A
-> { C : Point | [ A # O ; C ] /\ [| O, C |] = [| O, B |] };
}.
Class Angles `(on : Orientations) :=
{(* Axiom 6 States that if two angles are equal, their explementary angles
will also be equal.
Since we defined angles as quantities (congruence classes), we need
the last Axiom 8, which ensures that the orientations we defined
earlier for pairs of rays originating from the same point, can also be
assigned to their respective angles. So, with this axiom we can lift
definition of orientation up from a particular geometric figures
(pairs of rays) to angles (congruence class).
*)
(** A4 *)
EqRs_EqRs_EqAs : forall (a b c d : Ray)
(orab : da a = da b)(orcd : da c = da d),
a == b
-> c == d
-> [| a, b | orab |] = [| c, d | orcd |];
(** A5 *)
OpRs_OpRs_EqAs : forall (a b c d : Ray)
(orab : da a = da b)(orcd : da c = da d),
a <==> b
-> c <==> d
-> [| a, b | orab |] = [| c, d | orcd |];
(** A6 *)
EqAs_EqExpAs : forall (a b c d : Ray)
(orab : da a = da b)(orcd : da c = da d),
[| a, b | orab |] = [| c, d | orcd |]
-> [| b, a | eq_sym orab |] = [| d, c | eq_sym orcd |];
(** A7 *)
EqAs_EqRs :
forall (a b c : Ray)(roab : da a = da b)(roac : da a = da c),
[| a, b | roab |] = [| a, c | roac |]
<-> b == c;
(** A8 *)
EqAs_EqTs : forall (a b c d : Ray)
(orab : da a = da b)(orcd : da c = da d)
(diab : ![ a # b ])(dicd : ![ c # d]),
[| a, b | orab |] = [| c, d | orcd |]
-> % {{ a # b | diab }} = % {{ c # d | dicd }};
}.
Class Concentricals `(cr : Circles) :=
{
(** A9 *)
ConcentricCircles : forall (O A B A' B' : Point),
[ O # A # B ]
-> [ O # A', B' ]
-> [| O, A |] = [| O, A' |]
-> [| O, B |] = [| O, B' |]
-> [ O # A' # B' ] /\ [| A, B |] = [| A', B' |];
(** P12, Circle-Circle Intersection *)
DrawIntersectionPointCC : forall (A O B A' O' B' P: Point),
~ [ O, O', P ]
-> [ A -- O -- B ]
-> [ A' -- O' -- B' ]
-> [ A # A' # B # B' ]
-> { Q : Point | [ O # O' | P, Q ] /\ [| O, Q |] = [| O, A |]
/\ [| O', Q |] = [| O', A' |] };
}.
(* We shall prove that the next two statements are actually equivalent to
each other. So, it suffices to accept only one of them as a new axiom.
The first statement formalizes the so-called Euclid's method of
superposition, while the second is actually a combination of
Euclid's SAS and SSS triangle congruence theorems.
*)
Class Superpositions `(on : Orientations) :=
{
(** A10 *)
SuperpositionPrinciple : forall (A B C D E F : Point)
(nABC : ~ [ A, B, C ])(nDEF : ~ [ D, E, F ]),
[| A, B |] = [| D, E |]
-> exists (F' : Point)(nDEF' : ~ [ D, E, F' ]), [ D # E | F, F' ] /\
{{ A # B # C | nABC }} :=: {{ D # E # F' | nDEF' }};
}.
Class Congruences `(on : Orientations) :=
{
(** A10' *)
TriangleCongruence : forall (A B C D E F : Point)
(nColABC : ~ [ A, B, C ])(nColDEF : ~ [ D, E, F ]),
[| A, B |] = [| D, E |]
-> [| B, C |] = [| E, F |]
-> [| C, A |] = [| F, D |]
<-> [| A # B # C | nColABC |] = [| D # E # F | nColDEF |];
}.
Class Parallels (dc : Declarations)(df : Definitions dc) :=
{
(** A11, John Playfair *)
(* No more than one line parallel to the given passes through
an arbitrary point on the plane. *)
ParallelAxiom :
forall (A : Point)(x y z : Line),
x || z
-> y || z
-> [ A @ x, y ]
-> x = y;
}.
(*****************************************************************************)
(* 1 *) Section INCIDENCE.
Context `{ ls : Lines }.
(*****************************************************************************)
Lemma nIncPt_DiPs :
forall (A B : Point)(x : Line),
[ A @ x ]
-> ~ [ B @ x ]
-> A <> B.
Proof with eauto.
intros * Aox nBox AeqB; subst; auto.
Qed.
Lemma nIncPt_DiLs :
forall (A : Point)(x y : Line),
[ A @ x ]
-> ~ [ A @ y ]
-> x <> y.
Proof with eauto.
intros * Aox nAoy xeqy; subst...
Qed.
(** Theorem #1. *)
(* a) For any two distinct points, there is at most one line containing
both these points. *)
Theorem DiPs_EqLs :
forall (A B : Point)(x y : Line),
A <> B
-> [ A, B @ x, y ]
-> x = y.
Proof with eauto.
intros * nAeqB [[ Aox Box ][ Aoy Boy ]].
apply NNPP; intros nxeqy.
destruct (DecideLineApartTwoPoints A B x y)...
Qed.
(* b) For any two distinct lines, there is at most one point on
both these lines. *)
Theorem DiLs_EqPs :
forall (A B : Point)(x y : Line),
x <> y
-> [ A, B @ x, y ]
-> A = B.
Proof with eauto.
intros * nxeqy [[ Aox Box ][ Aoy Boy ]].
apply NNPP; contradict nxeqy.
apply (DiPs_EqLs A B x y)...
Qed.
(** Problem #1 *)
(* Given an arbitrary point. Draw a line that pass through it. *)
Definition DrawLineThroughPoint :
forall (A : Point),
{ x : Line | [ A @ x ] }.
Proof with eauto.
intros.
destruct (DrawDistinctPoint A) as [ B nAeqB ];
destruct (DrawExtensionLinePP A B nAeqB) as [ x [ Aox Box ]];
exists x...
Defined.
(** Problem #2 *)
(* Draw an arbitrary line on plane. *)
Definition DrawLine :
{ x : Line | x = x }.
Proof with eauto.
destruct DrawPoint as [ A _ ].
destruct (DrawLineThroughPoint A) as [ x Aox ].
exists x...
Defined.
(** Problem #3 *)
(* Given an arbitrary point. Draw a line that does not pass through it. *)
Definition DrawLineApartPoint :
forall (A : Point),
{ x : Line | ~ [ A @ x ] }.
Proof with eauto.
intros.
destruct (DrawDistinctPoint A) as [ B nBeqA ].
destruct (DrawExtensionLinePP B A) as [ t [ Bot Aot ]]...
destruct (DrawPointApartLine t) as [ C nCot ].
assert (nBeqC : B <> C). { contradict nCot; subst... }
destruct (DrawExtensionLinePP B C ) as [ x [ Box Cox ]]...
exists x. intros Aox.
assert (xeqt : x = t). { eapply (DiPs_EqLs A B)... }
subst...
Defined.
(** Problem #4 *)
(* Given two distinct points. Draw a line that passes through one of these
points and does not pass through another. *)
Definition DrawLineSeparatingTwoPoints :
forall (A B : Point),
A <> B
-> { x : Line | [ A @ x ] /\ ~ [ B @ x ] }.
Proof with eauto.
intros * nAeqB.
destruct (DrawExtensionLinePP A B) as [ t [ Bot Aot ]]...
destruct (DrawPointApartLine t) as [ C nCot ].
assert (nAeqC : A <> C). { contradict nCot; subst... }
destruct (DrawExtensionLinePP A C ) as [ x [ Aox Cox ]]...
exists x; split...
intros Box.
assert (xeqt : x = t). { eapply (DiPs_EqLs A B)... }
subst...
Defined.
(** Problem #5 *)
(* Given two distinct lines. Draw a point that lies on one of these lines
and does not lie on the other. *)
Definition DrawPointSeparatingTwoLines :
forall (x y : Line),
x <> y
-> { A : Point | [ A @ x ] /\ ~ [ A @ y ] }.
Proof with eauto.
intros x y nxeqy.
destruct (DrawPointOnLine x) as [ A Aox ].
destruct (DrawDistinctPointOnLine A x Aox) as [ B [ nAeqB Box ]]...
destruct (DecideLineApartTwoPoints A B x y)...
Defined.
(** Problem #6 *)
(* Given two distinct points, through one of which pass two distinct lines.
Decide which of these two lines does not pass through another point. *)
Definition DecidePointApartTwoLines :
forall (O A : Point)(x y : Line),
A <> O
-> [ O @ x, y ]
-> x <> y
-> { ~ [ A @ x ] } + { ~ [ A @ y ] }.
Proof with eauto.
intros * nAeqO [ Oox Ooy ] nxeqy.
destruct (DrawDistinctPointOnLine O x Oox) as [ B [ nBeqO Box ]].
destruct (DrawDistinctPointOnLine O y Ooy) as [ C [ nCeqO Coy ]].
assert (nBeqC : B <> C).
{ contradict nxeqy; subst. eapply (DiPs_EqLs O C)... }
destruct (DrawExtensionLinePP B C nBeqC) as [ z [ Boz Coz ]].
destruct (DrawExtensionLinePP A O nAeqO) as [ t [ Aot Oot ]].
assert (nteqz : t <> z).
{ contradict nxeqy; subst...
assert (y = z). { eapply (DiPs_EqLs O C)... }
subst...
eapply (DiPs_EqLs O B)...
}
destruct (DecideLineApartTwoPoints B C z t nBeqC)
as [ H1 | H2 ]; try split...
{ left. contradict H1.
assert (x = t). { eapply (DiPs_EqLs A O)... }
subst...
}
{ right. contradict H2.
assert (y = t). { eapply (DiPs_EqLs A O)... }
subst...
}
Defined.
Example DrawThirdDistinctPoint :
forall (A B : Point),
{ C : Point | C <> A /\ C <> B }.
Proof with eauto.
intros.
destruct (DrawDistinctPoint A) as [ P nPeqA ].
destruct (DecidePointsDistinction A B P nPeqA) as [ nAeqB | nBeqP ].
{ destruct (DrawExtensionLinePP A B nAeqB) as [ x [ Aox Box ]].
destruct (DrawPointApartLine x) as [ C nCox ].
exists C; split; contradict nCox; subst...
}
{ exists P; split... }
Defined.
Lemma ConvLs_irrefl :
forall (x : Line),
~ x >< x.
Proof.
intros x [ H _ ].
contradict H; auto.
Qed.
Lemma ConvLs_sym :
forall (x y : Line),
x >< y
-> y >< x.
Proof.
unfold Convergent.
intros x y [ nyeqx [ A [ Aoy Aox ]]].
split; eauto.
Qed.
Lemma nIncPt_ConvLs_1 :
forall (A B : Point)(x y : Line),
A <> B
-> [ A @ x ]
-> [ A @ y ]
-> [ B @ x ]
-> ~ [ B @ y ]
-> x >< y.
Proof with eauto.
intros * nAeqB Aox Aoy Box nBoy.
split.
{ contradict nBoy; subst... }
{ exists A; split... }
Qed.
Lemma nIncPt_ConvLs_2 :
forall (A B : Point)(x y : Line),
A <> B
-> [ A @ x ]
-> [ A @ y ]
-> [ B @ y ]
-> ~ [ B @ x ]
-> x >< y.
Proof with eauto.
intros * nAeqB Aox Aoy Boy nBox.
split.
{ contradict nBox; subst... }
{ exists A; split... }
Qed.
Lemma ParLs_InsPs_EqLs :
forall (A : Point)(x y : Line),
x || y
-> [ A @ x, y ]
-> x = y.
Proof.
intros * xpary [ Aox Aoy ].
unfold Parallel, Convergent in *.
apply NNPP; intros nxeqy.
contradict xpary; split; try exists A; auto.
Qed.
End INCIDENCE.
Hint Resolve
not_eq_sym nIncPt_DiPs
: DiPs.
Hint Resolve
DiLs_EqPs
: EqPs.
Hint Resolve
not_eq_sym nIncPt_DiLs
: DiLs.
Hint Resolve
DiPs_EqLs
ParLs_InsPs_EqLs
: EqLs.
Tactic Notation "dips"
:= try solve
[ congruence
| eauto with DiPs
| intuition eauto with DiPs ].
Tactic Notation "dips" integer(n)
:= try solve
[ congruence
| eauto n with DiPs
| intuition (auto n with DiPs) ].
Tactic Notation "eqps"
:= try solve
[ congruence
| eauto with EqPs
| intuition eauto with EqPs ].
Tactic Notation "eqps" integer(n)
:= try solve
[ congruence
| eauto n with EqPs
| intuition (auto n with EqPs) ].
Tactic Notation "dils"
:= try solve
[ congruence
| eauto with DiLs
| intuition eauto with DiLs].
Tactic Notation "dils" integer(n)
:= try solve
[ congruence
| eauto n with DiLs
| intuition (auto n with DiLs) ].
Tactic Notation "eqls"
:= try solve
[ congruence
| eauto with EqLs
| intuition eauto with EqLs].
Tactic Notation "eqls" integer(n)
:= try solve
[ congruence
| eauto n with EqLs
| intuition (auto n with EqLs) ].
(*****************************************************************************)
(* 2 *) Section COLLINEARITY.
Context `{ lns : Lines }.
(*****************************************************************************)
Lemma ColPs_IncPt :
forall (A B C : Point)(x : Line),
A <> B
-> [ A, B @ x ]
-> [ A, B, C ] \/
[ A, C, B ] \/
[ B, A, C ] \/
[ B, C, A ] \/
[ C, A, B ] \/
[ C, B, A ]
-> [ C @ x ].
Proof.
intros * nAeqB [ Aox Box ] H;
repeat destruct H as [ H | H ];