Longueur
Les seuls concepts concepts primitifs utilisés par Tarski sont les points sur lesquelles il définit deux relations :
- Between : exprime le fait qu'un point se situe entre deux autres points (sur une même droite)
- Cong: permet d'affirmer que deux segments définis par deux couples de points ont même longueur
une longueur est ainsi définie :
longueur(l : Point -> Point -> Prop) :=
∃ A B : Point, ∀ X Y : Point, l X Y <=> Cong A B X Y
longueur nulle
lg_null ln := lg ln /\ ∃ A, ln A A
égalité de longueurs
eqL l1 l2 := lg l1 /\ lg l2 /\ ∀ A B, l1 A B <=> l2 A B
ou
eqL l1 l2 := lg l1 /\ lg l2 /\ ∃ A B, l1 A B <=> l2 A B
Angles
A la manière des longueurs, les angles sont définis grâce à la relation de congruence entre les angles : Conga
un angle est ainsi défini
ang (a : Tpoint -> Tpoint -> Tpoint -> Prop) :=
∃ A B C, A ≠ B /\ C ≠ B /\
∀ X Y Z, Conga A B C X Y Z <=> a X Y Z
égalité d'angles
eqA a1 a2 => ang a1 /\ ang a2 /\ ∀ A B C, a1 A B C <=> a2 A B C.
angle aigu
anga (a : Tpoint -> Tpoint -> Tpoint -> Prop) :=
∃ A B C, acute A B C /\
∀ X Y Z, Conga A B C X Y Z <=> a X Y Z
angle nul
is_null_ang a => ang a /\ ∀ A B C, a A B C => out B A C
ou
is_null_ang a => ang a /\ ∃ A B C, a A B C => out B A C
angle plat
is_flat_ang a => ang a /\ ∀ A B C, a A B C => Bet A B C
ou
is_null_ang a => ang a /\ ∃ A B C, a A B C => Bet A B C
longueur projetée
Tarski utilise une notation fonctionnelle pour la démonstration du théorème de Pappus-Pascal
En coq on utilise une notation sous forme de prédicats
la notation a l = lp s'écrit lcos lp l a
égalité des longueurs projetées
lcos_eq la a lb b := exists lp, lcos lp la a /\ lcos lp lb b
Ainsi lorsque Tarski note a la = b lp l'égalité des longueurs des projetées de
la selon l'angle a et de
lb selon l'angle b,
en Coq on écrit lcos_eq la a lb b
double projection
lcos2 lp l a b := exists la, lcos la l a /\ lcos lp la b
égalité de la double projection
lcos2_eq l1 a b l2 c d := exists lp, lcos2 lp l1 a b /\ lcos2 lp l2 c d
triple projection
lcos3 lp l a b c := exists la, exists lab, lcos la l a /\ lcos lab la b /\ lcos lp lab c
égalité de la triple projection
lcos3_eq := fun l1 a b c l2 d e f := exists lp, lcos3 lp l1 a b c /\ lcos3 lp l2 d e f
