-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCh01_tarski_axioms.v
124 lines (83 loc) · 3.56 KB
/
Ch01_tarski_axioms.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
(* Julien Narboux *)
(* Formalization of *)
(* Tarski's axiomatic *)
Require Export general_tactics.
(** We use the axioms used in the book of Schwabäuser, Szmielew and Tarski. *)
(** We assume that we have a set of points. This axiomatic is based only on points, lines are implicit. *)
Parameter Point : Set.
(* Here we use classical logic, for a intuitionnist approach
use von Plato axiomatic for instance.
In this development, the classic axiom is mainly applied to formulas of the form :
- Col A B C,
- A=B
*)
Require Export Classical.
(** Tarski's axiomatic is based on two predicates over points,
one ternary and one quaternary. *)
(** Cong A B C D informally means that the distance AB
is equal to the distance CD. *)
Parameter Cong : Point -> Point -> Point -> Point -> Prop.
(** Bet A B C, informally means that :
A, B and C are on the same line
B is between A and C.
Note that they are not necessarily distinct.
This is the difference between
the Between predicate of Tarski and the BetweenH prdicate of Hilbert
*)
Parameter Bet : Point -> Point -> Point -> Prop.
Definition Col (A B C : Point) : Prop :=
Bet A B C \/ Bet B C A \/ Bet C A B.
Ltac cases_col A B C := elim (classic (Col A B C));intros.
(** %\textbf{% Identity axiom for betweenness. %}% *)
Axiom between_identity : forall A B, Bet A B A -> A=B.
(** %\textbf{% Reflexivity axiom for equidistance.%}% *)
Axiom cong_pseudo_reflexivity : forall A B : Point, Cong A B B A.
(** %\textbf{% Identity axiom for equidistance.%}% *)
Axiom cong_identity : forall A B C : Point, Cong A B C C -> A = B.
(** %\textbf{% Transitivity axiom for equidistance.%}% *)
Axiom cong_inner_transitivity : forall A B C D E F : Point,
Cong A B C D -> Cong A B E F -> Cong C D E F.
(** %\textbf{% Pasch Axiom (Inner form).%}% *)
Axiom inner_pasch : forall A B C P Q : Point,
Bet A P C -> Bet B Q C ->
exists x, Bet P x B /\ Bet Q x A.
(** %\textbf{% Euclid Axiom.%}% *)
Axiom euclid : forall A B C D T : Point,
Bet A D T -> Bet B D C -> A<>D ->
exists x, exists y,
Bet A B x /\ Bet A C y /\ Bet x T y.
(** %\textbf{% Five segments axiom.%}% *)
Axiom five_segments : forall A A' B B' C C' D D' : Point,
Cong A B A' B' ->
Cong B C B' C' ->
Cong A D A' D' ->
Cong B D B' D' ->
Bet A B C -> Bet A' B' C' -> A <> B -> Cong C D C' D'.
(** %\textbf{% Axiom of segment construction.%}% *)
Axiom segment_construction : forall A B C D : Point,
exists E : Point, Bet A B E /\ Cong B E C D.
(** %\textbf{% Lower dimension axiom (2).%}% *)
Axiom lower_dim :
exists A, exists B, exists C, ~ Col A B C.
(** %\textbf{% Upper dimension axiom (2).%}% *)
Axiom upper_dim : forall A B C P Q : Point,
P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q ->
Col A B C.
(** %\textbf{% Continuity axioms.%}% *)
Axiom continuity :
forall X Y : Point -> Prop,
(exists A : Point, (forall x y : Point, X x -> Y y -> Bet A x y)) ->
exists B : Point, (forall x y : Point, X x -> Y y -> Bet x B y).
Hint Resolve segment_construction five_segments inner_pasch euclid : Tarski.
Hint Resolve cong_pseudo_reflexivity cong_identity between_identity : Tarski.
Hint Resolve cong_inner_transitivity : Tarski.
Ltac eTarski := eauto with Tarski.
Ltac Tarski := auto with Tarski.
(** We use classical logic, to emphasize the fact that it is mainly for the decidability of point equality we use the
following lemma *)
Lemma eq_dec_points : forall A B:Point, A=B \/ ~ A=B.
Proof.
intros.
apply classic.
Qed.
Ltac cases_equality A B := elim (eq_dec_points A B);intros.