Comment: Beeson's Constructive Tarski Geometry
Tarski and his students (Szemeilew, Gupta) gave a
first order axiomatic theory for Euclidean plane geometry
that had only Points as elements and two relations.
a ternary "betweeness" relation and a quaternary "congruence" relation
(which defines a binary "same length" relation on segments).
They made the system minimal, so that the axioms were all independent
and none of them could be derived from the others (using classical logic).
Beeson has given a constructive, intuitionistic logic, version of Tarski's
system -- which we formalize here in Nuprl. We use constructive
logic and do not assume that equality of Points is decidable.
Therefore, a theorem stating that for
all points A and B satisfying some constraints P(A,B)
there exists a point C satisfying constraints Q(A,B,C)
may not be proved by cases where if A=B then C is constructed one way
and if not(A=B) then C is constructed another way.
Because of this, Beeson must add a few axioms that
were derivable (using classical logic) in Tarski's system.
Also, to make all of the constructions continuous functions of their input
points, two of the axioms (the "extend" axiom and the "inner Pasch" axiom)
that construct new points are restricted to non-degenerate cases
(only segments with distinct endpoints can be extended, and
the "inner Pasch" requires a non-colinear triangle and strict betweenness).
Finally, Beeson's axioms assume that the betweenness relation and the congruence
relation are "stable" propositions about points (a proposition P is stable
if (¬¬P) ⇒ P ).
The formal definition of a EuclideanPlane has the form
{e:EuclideanStructure| euclidean-axioms(e)} -- follow those links (right click) for
further documentation. ⋅
Definition: euclidean-structure
A dependent record type defines the basic types and operations
of Beeson's constructive version of Tarski's geometry.
The first "field" of the record is the type "Point" and the types
of the other fields depend on ⌜self."Point"⌝.
"E" is the congruence relation ⌜ab=cd⌝ and "B" is the strict betweeness
relation ⌜a-b-c⌝. "T" is the non-strict betweeness relation ⌜a_b_c⌝
but it is really a defined concept because the "Tdef" field forces
⌜a_b_c ⇐⇒ ¬((¬(a = b ∈ self."Point")) ∧ (¬(c = b ∈ self."Point")) ∧ (¬a-b-c))⌝.
Simlarly, ⌜Colinear(a;b;c)⌝ is introduced via "colinear" and defined
by "colineardef". These definitions are in the dependent record because
they are needed to give the constrained types for the
"extend", "inner-Pasch", "line-circle" and "middle" operators.
The fields "Estable" and "Bstable" force the congruence and betweeness
propositions to be stable (see Stable{P}, it says ⌜(¬¬P) ⇒ P⌝ ).⋅
EuclideanStructure ==
"Point":Type
"E":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"B":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"T":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"colinear":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"nontrivial":{trip:self."Point" × self."Point" × self."Point"|
let a,b,c = trip in
(¬(a = b ∈ self."Point")) ∧ (¬(self."colinear" a b c))}
"Tdef":∀[a,b,c:self."Point"].
(self."T" a b c ⇐⇒ ¬((¬(a = b ∈ self."Point")) ∧ (¬(c = b ∈ self."Point")) ∧ (¬(self."B" a b c))))
"colineardef":∀[a,b,c:self."Point"].
(self."colinear" a b c
⇐⇒ (¬(a = b ∈ self."Point"))
∧ (¬((¬(c = a ∈ self."Point"))
∧ (¬(c = b ∈ self."Point"))
∧ (¬(self."B" c a b))
∧ (¬(self."B" a c b))
∧ (¬(self."B" a b c)))))
"Estable":∀[a,b,c,d:self."Point"]. self."E" a b c d supposing ¬¬(self."E" a b c d)
"Bstable":∀[a,b,c:self."Point"]. self."B" a b c supposing ¬¬(self."B" a b c)
"extend":a:self."Point" ⟶ {b:self."Point"| ¬(a = b ∈ self."Point")} ⟶ self."Point" ⟶ self."Point" ⟶ self."Point"
"inner-Pasch":a:self."Point"
⟶ b:self."Point"
⟶ c:{c:self."Point"| ¬(self."colinear" a b c)}
⟶ {p:self."Point"| self."B" a p c}
⟶ {q:self."Point"| self."T" b q c}
⟶ self."Point"
"line-circle":a:self."Point"
⟶ b:self."Point"
⟶ x:{x:self."Point"| self."T" a x b}
⟶ y:{y:self."Point"| self."T" a b y}
⟶ p:{p:self."Point"| self."E" a p a x}
⟶ {q:self."Point"| (self."E" a q a y) ∧ (¬(q = p ∈ self."Point"))}
⟶ (self."Point" × self."Point")
"middle":a:self."Point" ⟶ b:self."Point" ⟶ c:{c:self."Point"| ¬(self."colinear" a b c)} ⟶ self."Point"
Lemma: euclidean-structure_wf
EuclideanStructure ∈ 𝕌'
Definition: eu-point
Point == e."Point"
Lemma: eu-point_wf
∀[e:EuclideanStructure]. (Point ∈ Type)
Definition: eu-congruent
ab=cd == e."E" a b c d
Lemma: eu-congruent_wf
∀[e:EuclideanStructure]. ∀[a,b,c,d:Point]. (ab=cd ∈ ℙ)
Lemma: stable__eu-congruent
∀e:EuclideanStructure. ∀[a,b,c,d:Point]. Stable{ab=cd}
Lemma: sq_stable__eu-congruent
∀e:EuclideanStructure. ∀[a,b,c,d:Point]. SqStable(ab=cd)
Definition: eu-between
a-b-c == e."B" a b c
Lemma: eu-between_wf
∀[e:EuclideanStructure]. ∀[a,b,c:Point]. (a-b-c ∈ ℙ)
Lemma: stable__eu-between
∀e:EuclideanStructure. ∀[a,b,c:Point]. Stable{a-b-c}
Lemma: sq_stable__eu-between
∀e:EuclideanStructure. ∀[a,b,c:Point]. SqStable(a-b-c)
Definition: eu-colinear
Colinear(a;b;c) == e."colinear" a b c
Lemma: eu-colinear_wf
∀[e:EuclideanStructure]. ∀[a,b,c:Point]. (Colinear(a;b;c) ∈ ℙ)
Definition: eu-nontrivial
eu-nontrivial(e) == e."nontrivial"
Lemma: eu-nontrivial_wf
∀[e:EuclideanStructure]
(eu-nontrivial(e) ∈ {triple:Point × Point × Point| let a,b,c = triple in (¬(a = b ∈ Point)) ∧ (¬Colinear(a;b;c))} )
Definition: eu-O
O == fst(eu-nontrivial(e))
Lemma: eu-O_wf
∀e:EuclideanStructure. (O ∈ Point)
Definition: eu-X
X == fst(snd(eu-nontrivial(e)))
Lemma: eu-X_wf
∀e:EuclideanStructure. (X ∈ Point)
Definition: eu-Y
Y == snd(snd(eu-nontrivial(e)))
Lemma: eu-Y_wf
∀[e:EuclideanStructure]. (Y ∈ Point)
Lemma: eu-colinear-def
∀e:EuclideanStructure
∀[a,b,c:Point].
(Colinear(a;b;c)
⇐⇒ (¬(a = b ∈ Point)) ∧ (¬((¬(c = a ∈ Point)) ∧ (¬(c = b ∈ Point)) ∧ (¬c-a-b) ∧ (¬a-c-b) ∧ (¬a-b-c))))
Lemma: stable__colinear
∀e:EuclideanStructure. ∀[a,b,c:Point]. Stable{Colinear(a;b;c)}
Lemma: sq_stable__colinear
∀e:EuclideanStructure. ∀[a,b,c:Point]. SqStable(Colinear(a;b;c))
Lemma: eu-not-not-colinear
∀e:EuclideanStructure
∀[a,b,c:Point].
(¬¬Colinear(a;b;c) ⇐⇒ (¬(a = b ∈ Point)) ∧ (¬¬((c = a ∈ Point) ∨ (c = b ∈ Point) ∨ c-a-b ∨ a-c-b ∨ a-b-c)))
Lemma: eu-not-colinear-OXY
∀[e:EuclideanStructure]. ((¬(O = X ∈ Point)) ∧ (¬Colinear(O;X;Y)))
Lemma: eu-not-equal-OXY
∀[e:EuclideanStructure]. ((¬(O = X ∈ Point)) ∧ (¬(O = Y ∈ Point)) ∧ (¬(X = Y ∈ Point)))
Definition: eu-between-eq
a_b_c == e."T" a b c
Lemma: eu-between-eq_wf
∀[e:EuclideanStructure]. ∀[a,b,c:Point]. (a_b_c ∈ ℙ)
Lemma: eu-between-eq-def
∀e:EuclideanStructure. ∀[a,b,c:Point]. (a_b_c ⇐⇒ ¬((¬(a = b ∈ Point)) ∧ (¬(c = b ∈ Point)) ∧ (¬a-b-c)))
Lemma: stable__eu-between-eq
∀e:EuclideanStructure. ∀[a,b,c:Point]. Stable{a_b_c}
Lemma: sq_stable__eu-between-eq
∀e:EuclideanStructure. ∀[a,b,c:Point]. SqStable(a_b_c)
Lemma: eu-between-eq-implies-colinear
∀e:EuclideanStructure. ∀[a,b,c:Point]. (Colinear(a;b;c)) supposing (a_b_c and (¬(a = b ∈ Point)))
Lemma: eu-between-implies-colinear
∀e:EuclideanStructure. ∀[a,b,c:Point]. (Colinear(a;b;c)) supposing (a-b-c and (¬(a = b ∈ Point)))
Lemma: eu-between-eq-implies-colinear2
∀e:EuclideanStructure. ∀[a,b,c:Point]. (Colinear(a;b;c)) supposing (c_a_b and (¬(a = b ∈ Point)))
Definition: eu-extend
(extend ab by cd) == e."extend" a b c d
Lemma: eu-extend_wf
∀[e:EuclideanStructure]. ∀[a:Point]. ∀[b:{b:Point| ¬(a = b ∈ Point)} ]. ∀[c,d:Point]. ((extend ab by cd) ∈ Point)
Definition: eu-inner-pasch
eu-inner-pasch(e;a;b;c;p;q) == e."inner-Pasch" a b c p q
Lemma: eu-inner-pasch_wf
∀[e:EuclideanStructure]. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ]\000C.
(eu-inner-pasch(e;a;b;c;p;q) ∈ Point)
Definition: eu-line-circle
intersect xy with Oab == e."line-circle" a b x y p q
Lemma: eu-line-circle_wf
∀[e:EuclideanStructure]. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ].
∀[q:{q:Point| aq=ay ∧ (¬(q = p ∈ Point))} ].
(intersect xy with Oab ∈ Point × Point)
Definition: eu-middle
middle(a;b;c) == e."middle" a b c
Lemma: eu-middle_wf
∀[e:EuclideanStructure]. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. (middle(a;b;c) ∈ Point)
Definition: euclidean-axioms
Twelve axioms about a EuclideanStructure
give Beeson's constructive version of Tarski's axioms.
They are reflexivity, transitivity, and identity of congruence;
"segment extension"; the "five-segment axiom"; "trivial strict betweeness";
the "inner-Pasch" axiom; the "upper-dimension" axiom;
the "triangle circumscription axiom" (equivalent to the parallel postulate);
the "line-circle continuity axiom"; symmetry and "inner transitivity" of
betweeness.⋅
euclidean-axioms(e) ==
(∀[a,b:Point]. ab=ba)
∧ (∀[a,b,p,q,r,s:Point]. (pq=rs) supposing (ab=rs and ab=pq))
∧ (∀[a,b,c:Point]. a = b ∈ Point supposing ab=cc)
∧ (∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point]. (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc))
∧ (∀[a,b,c,d,A,B,C,D:Point].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point))))
∧ (∀[a,b:Point]. (¬a-b-a))
∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
let x = eu-inner-pasch(e;a;b;c;p;q) in
p-x-b ∧ q-x-a)
∧ (∀[a,b,p,q,r:Point]. (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point))))
∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. let x = middle(a;b;c) in ax=bx ∧ ax=cx)
∧ (∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point|
aq=ay
∧ (¬(q = p ∈ Point))} ].
let uv = intersect xy with Oab in
afst(uv)=ab
∧ asnd(uv)=ab
∧ p_fst(uv)_q
∧ snd(uv)_p_q
∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point))
∧ (∀[a,b,c:Point]. c-b-a supposing a-b-c)
∧ (∀[a,b,c,d:Point]. (a-b-c) supposing (b-c-d and a-b-d))
Lemma: euclidean-axioms_wf
∀[e:EuclideanStructure]. (euclidean-axioms(e) ∈ ℙ)
Lemma: sq_stable_euclidean-axioms
∀e:EuclideanStructure. SqStable(euclidean-axioms(e))
Definition: euclidean-plane
Beeson's axioms for constructive geometry.
The EuclideanStructure includes the basic types and
four operations with constructive content.
The four basic constructions are
1) extending a segment,
2) intersecting lines,
3) intersecting a line and a circle,
4) circumscribing a triangle.
The euclidean-axioms(e)
are constraints on the euclidean structures that have no constructive
content -- they assert the congruence and betweeness properties of the
four basic constructions.
⋅
EuclideanPlane == {e:EuclideanStructure| euclidean-axioms(e)}
Lemma: euclidean-plane_wf
EuclideanPlane ∈ 𝕌'
Lemma: eu-extend-property
∀e:EuclideanPlane
∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point]. (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)
Lemma: eu-inner-pasch-property
∀e:EuclideanPlane
∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
(p-eu-inner-pasch(e;a;b;c;p;q)-b ∧ q-eu-inner-pasch(e;a;b;c;p;q)-a)
Lemma: eu-segments-cross
∀e:EuclideanPlane. ∀p,b,q,a:Point. ((∃c:Point. ((¬Colinear(a;b;c)) ∧ a-p-c ∧ b_q_c)) ⇒ (∃x:Point. (p-x-b ∧ q-x-a)))
Lemma: eu-extend-exists
∀e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| ¬(q = a ∈ Point)} . ∀b,c:Point. ∃x:Point. (q_a_x ∧ ax=bc)
Lemma: eu-between-trans
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (a-b-c) supposing (b-c-d and a-b-d)
Lemma: eu-between-sym
∀e:EuclideanPlane. ∀[a,b,c:Point]. a-b-c supposing c-b-a
Lemma: eu-between-trans2
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (a-b-c) supposing (d-b-c and d-a-b)
Lemma: eu-between-implies-between-eq
∀e:EuclideanPlane. ∀[a,b,c:Point]. a_b_c supposing a-b-c
Lemma: eu-between-eq-implies-colinear3
∀e:EuclideanPlane. ∀[a,b,c:Point]. (Colinear(a;b;c)) supposing (b_c_a and (¬(a = b ∈ Point)))
Lemma: eu-congruence-identity
∀[e:EuclideanPlane]. ∀[a,b,c:Point]. a = b ∈ Point supposing ab=cc
Lemma: eu-congruence-identity2
∀[e:EuclideanPlane]. ∀[a,b,c,d:Point]. (a = b ∈ Point) supposing (ab=cd and (c = d ∈ Point))
Lemma: stable_point-eq
∀[e:EuclideanPlane]. ∀[p,q:Point]. Stable{p = q ∈ Point}
Lemma: euclidean-point-eq
∀[e:EuclideanPlane]. ∀[p,q:Point]. p = q ∈ Point supposing ¬¬(p = q ∈ Point)
Lemma: eu-between-same
∀[e:EuclideanPlane]. ∀[a,b:Point]. (¬a-b-a)
Lemma: eu-between-same2
∀[e:EuclideanPlane]. ∀[a,b:Point]. False supposing a-b-a
Lemma: not-eu-between-same
∀e:EuclideanPlane. ∀[a,b:Point]. False supposing a-b-b
Lemma: not-eu-between-same2
∀e:EuclideanPlane. ∀[a,b:Point]. False supposing a-a-b
Lemma: eu-between-eq-same
∀[e:EuclideanPlane]. ∀[a,b:Point]. a = b ∈ Point supposing a_b_a
Lemma: eu-between-eq-same2
∀[e:EuclideanPlane]. ∀[a,b,c:Point]. (a = b ∈ Point) supposing ((a = c ∈ Point) and a_b_c)
Lemma: stable_eu-between-eq
∀e:EuclideanPlane. ∀[a,b,c:Point]. Stable{a_b_c}
Lemma: eu-between-eq-trivial-left
∀e:EuclideanPlane. ∀[a,b:Point]. a_a_b
Lemma: eu-between-eq-trivial-right
∀e:EuclideanPlane. ∀[a,b:Point]. a_b_b
Lemma: eu-between-eq-symmetry
∀e:EuclideanPlane. ∀[a,b,c:Point]. c_b_a supposing a_b_c
Lemma: eu-between-eq-inner-trans
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (a_b_c) supposing (b_c_d and a_b_d)
Lemma: eu-between-eq-exchange3
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (b_c_d) supposing (a_c_d and a_b_c)
Lemma: eu-congruent-refl
∀e:EuclideanPlane. ∀[a,b:Point]. ab=ab
Lemma: eu-congruent-flip
∀e:EuclideanPlane. ∀[a,b:Point]. ab=ba
Lemma: eu-congruent-symmetry
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. cd=ab supposing ab=cd
Lemma: eu-congruent-transitivity
∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point]. (ab=xy) supposing (cd=xy and ab=cd)
Lemma: eu-congruent-left-comm
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. ba=cd supposing ab=cd
Lemma: eu-congruent-right-comm
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. ab=dc supposing ab=cd
Lemma: eu-congruent-comm
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. ba=dc supposing ab=cd
Lemma: eu-congruent-trivial
∀e:EuclideanPlane. ∀[a,b:Point]. aa=bb
Lemma: eu-congruence-identity-sym
∀[e:EuclideanPlane]. ∀[a,b,c:Point]. a = b ∈ Point supposing cc=ab
Lemma: eu-congruence-identity3
∀[e:EuclideanPlane]. ∀[a,b,c,d:Point]. (a = b ∈ Point) supposing (cd=ab and (c = d ∈ Point))
Lemma: eu-five-segment
∀e:EuclideanPlane
∀[a,b,c,d,A,B,C,D:Point].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))
Lemma: eu-five-segment'
∀e:EuclideanPlane
∀[a,b,c,A,B,C:Point].
(∀d,D:Point. (cd=CD) supposing (bd=BD and ad=AD)) supposing
(bc=BC and
ab=AB and
A_B_C and
a_b_c and
(¬(a = b ∈ Point)))
Lemma: eu-three-segment
∀e:EuclideanPlane. ∀[a,b,c,A,B,C:Point]. (ac=AC) supposing (bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))
Lemma: eu-construction-unicity
∀e:EuclideanPlane. ∀[Q,A,X,Y:Point]. (X = Y ∈ Point) supposing (AY=AX and Q_A_X and Q_A_Y and (¬(Q = A ∈ Point)))
Lemma: eu-extend-equal-iff-congruent
∀e:EuclideanPlane
∀[a,b,c,d,c',d':Point]. uiff((extend ab by cd) = (extend ab by c'd') ∈ Point;cd=c'd') supposing ¬(a = b ∈ Point)
Lemma: eu-between-eq-outer-trans
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (a_c_d) supposing (b_c_d and a_b_c and (¬(b = c ∈ Point)))
Lemma: eu-between-eq-exchange4
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. (a_b_d) supposing (a_c_d and a_b_c)
Lemma: eu-exists-middle
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{p:Point| ¬Colinear(a;b;p)} . ∃m:Point. ((m = middle(a;b;c) ∈ Point) ∧ am=bm ∧ am=cm)
Lemma: eu-colinear-cases
∀e:EuclideanStructure
∀[a,b,c:Point].
∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) ⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) ⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b) ⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b) ⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c) ⇒ X)
⇒ ((¬Colinear(a;b;c)) ⇒ X)
⇒ X)
Lemma: eu-colinear-implies-1
∀e:EuclideanPlane. ∀x,a,b:Point. (Colinear(b;a;x) ⇒ Colinear(b;a;a))
Lemma: eu-colinear-permute
∀e:EuclideanPlane. ∀a,b,c:Point. ((¬(c = b ∈ Point)) ⇒ Colinear(a;b;c) ⇒ Colinear(c;b;a))
Lemma: eu-colinear-cycle
∀e:EuclideanPlane. ∀a,b,c:Point. ((¬(c = a ∈ Point)) ⇒ Colinear(a;b;c) ⇒ Colinear(c;a;b))
Lemma: eu-colinear-swap
∀e:EuclideanPlane. ∀a,b,c:Point. (Colinear(a;b;c) ⇒ Colinear(b;a;c))
Lemma: not-not-inner-pasch
∀e:EuclideanPlane. ∀a,b,c:Point. ∀p:{p:Point| a_p_c} . ∀q:{q:Point| b_q_c} . (¬¬(∃x:Point. (p_x_b ∧ q_x_a)))
Definition: eu-segment
Segment == Point × Point
Lemma: eu-segment_wf
∀[e:EuclideanStructure]. (Segment ∈ Type)
Definition: eu-mk-seg
ab == <a, b>
Lemma: eu-mk-seg_wf
∀[e:EuclideanStructure]. ∀[a,b:Point]. (ab ∈ Segment)
Definition: eu-seg1
s.1 == fst(s)
Lemma: eu-seg1_wf
∀[e:EuclideanStructure]. ∀[s:Segment]. (s.1 ∈ Point)
Definition: eu-seg2
s.2 == snd(s)
Lemma: eu-seg2_wf
∀[e:EuclideanStructure]. ∀[s:Segment]. (s.2 ∈ Point)
Lemma: eu_seg1_mk_seg_lemma
∀b,a:Top. (ab.1 ~ a)
Lemma: eu_seg2_mk_seg_lemma
∀b,a:Top. (ab.2 ~ b)
Definition: eu-seg-proper
proper(s) == ¬(s.1 = s.2 ∈ Point)
Lemma: eu-seg-proper_wf
∀[e:EuclideanStructure]. ∀[s:Segment]. (proper(s) ∈ ℙ)
Definition: eu-proper-segment
ProperSegment == {s:Segment| proper(s)}
Lemma: eu-proper-segment_wf
∀[e:EuclideanStructure]. (ProperSegment ∈ Type)
Definition: eu-seg-congruent
s1 ≡ s2 == s1.1s1.2=s2.1s2.2
Lemma: eu-seg-congruent_wf
∀[e:EuclideanStructure]. ∀[s1,s2:Segment]. (s1 ≡ s2 ∈ ℙ)
Lemma: sq_stable_eu-seg-congruent
∀e:EuclideanStructure. ∀[s1,s2:Segment]. SqStable(s1 ≡ s2)
Lemma: eu-seg-congruent_transitivity
∀e:EuclideanPlane. ∀[s1,s2,s3:Segment]. (s1 ≡ s3) supposing (s1 ≡ s2 and s2 ≡ s3)
Lemma: eu-seg-congruent_symmetry
∀e:EuclideanPlane. ∀[s1,s2:Segment]. s2 ≡ s1 supposing s1 ≡ s2
Lemma: eu-seg-congruent_weakening
∀e:EuclideanPlane. ∀[s1,s2:Segment]. s1 ≡ s2 supposing s1 = s2 ∈ Segment
Lemma: eu-seg-congruent-equiv
∀e:EuclideanPlane. EquivRel(Segment;s,t.s ≡ t)
Lemma: eu-seg-congruent-equiv-proper
∀e:EuclideanPlane. EquivRel(ProperSegment;s,t.s ≡ t)
Definition: eu-seg-extend
s + t == <s.1, (extend s.1s.2 by t.1t.2)>
Lemma: eu-seg-extend_wf
∀[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment]. (s + t ∈ ProperSegment)
Lemma: eu-seg-extend_functionality
∀e:EuclideanPlane. ∀[s1,s2:ProperSegment]. ∀[t1,t2:Segment]. (s1 + t1 ≡ s2 + t2) supposing (t1 ≡ t2 and s1 ≡ s2)
Lemma: eu-congruent-flip-seg
∀e:EuclideanPlane. ∀[a,b:Point]. ab ≡ ba
Definition: eu-length
|s| == (extend OX by s.1s.2)
Lemma: eu-length_wf
∀[e:EuclideanPlane]. ∀[s:Segment]. (|s| ∈ {p:Point| O_X_p} )
Definition: eu-le
p ≤ q == X_p_q
Lemma: eu-le_wf
∀[e:EuclideanPlane]. ∀[p,q:{p:Point| O_X_p} ]. (p ≤ q ∈ ℙ)
Lemma: eu-le_transitivity
∀e:EuclideanPlane. ∀[p,q,r:{p:Point| O_X_p} ]. (p ≤ r) supposing (q ≤ r and p ≤ q)
Definition: eu-lt
p < q == p ≤ q ∧ (¬(p = q ∈ Point))
Lemma: eu-lt_wf
∀[e:EuclideanPlane]. ∀[p,q:{p:Point| O_X_p} ]. (p < q ∈ ℙ)
Lemma: eu-lt_transitivity
∀e:EuclideanPlane. ∀[p,q,r:{p:Point| O_X_p} ]. (p < r) supposing (q < r and p ≤ q)
Lemma: eu-seg-congruent-iff-length
∀e:EuclideanPlane. ∀[s,t:Segment]. uiff(s ≡ t;|s| = |t| ∈ {p:Point| O_X_p} )
Lemma: eu-congruent-iff-length
∀e:EuclideanPlane. ∀[a,b,c,d:Point]. uiff(ab=cd;|ab| = |cd| ∈ {p:Point| O_X_p} )
Lemma: eu-length-flip
∀e:EuclideanPlane. ∀[a,b:Point]. (|ab| = |ba| ∈ {p:Point| O_X_p} )
Lemma: eu-proper-extend-exists
∀e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| ¬(q = a ∈ Point)} . ∀b:Point. ∀c:{c:Point| ¬(b = c ∈ Point)} .
∃x:Point. (q-a-x ∧ ax=bc)
Definition: eu-add-length
p + q == (extend Op by Xq)
Lemma: eu-add-length_wf
∀[e:EuclideanPlane]. ∀[x,y:{p:Point| O_X_p} ]. (x + y ∈ {p:Point| O_X_p} )
Lemma: eu-add-length-comm
∀[e:EuclideanPlane]. ∀[x,y:{p:Point| O_X_p} ]. (x + y = y + x ∈ {p:Point| O_X_p} )
Lemma: eu-add-length-zero
∀[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ]. (x + X = x ∈ {p:Point| O_X_p} )
Lemma: eu-length-null-segment
∀[e:EuclideanPlane]. ∀[a:Point]. (|aa| = X ∈ {p:Point| O_X_p} )
Lemma: eu-le-null-segment
∀e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point]. uiff(p ≤ |aa|;p = |aa| ∈ {p:Point| O_X_p} )
Lemma: eu-lt-null-segment
∀e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point]. uiff(p < |aa|;False)
Lemma: eu-lt-null-segment2
∀e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a,b:Point]. (False) supposing ((a = b ∈ Point) and p < |ab|)
Lemma: eu-add-length-zero2
∀[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ]. ∀[a:Point]. (x + |aa| = x ∈ {p:Point| O_X_p} )
Lemma: eu-add-length-zero3
∀[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ]. ∀[a:Point]. (|aa| + x = x ∈ {p:Point| O_X_p} )
Lemma: eu-add-length-between
∀[e:EuclideanPlane]. ∀[a,b,c:Point]. |ac| = |ab| + |bc| ∈ {p:Point| O_X_p} supposing a_b_c
Lemma: eu-add-length-assoc
∀[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ]. (x + y + z = x + y + z ∈ {p:Point| O_X_p} )
Lemma: eu-add-length-cancel-left
∀[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ]. x = y ∈ {p:Point| O_X_p} supposing z + x = z + y ∈ {p:Point| O_X_p}
Lemma: eu-add-length-cancel-right
∀[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ]. x = y ∈ {p:Point| O_X_p} supposing x + z = y + z ∈ {p:Point| O_X_p}
Lemma: eu-le-add1
∀e:EuclideanPlane. ∀[p,q:{p:Point| O_X_p} ]. p ≤ p + q
Lemma: eu-seg-length-extend
∀[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment]. (|s + t| = |s| + |t| ∈ {p:Point| O_X_p} )
Lemma: eu-inner-five-segment
∀e:EuclideanPlane
∀[a,b,c,d,A,B,C,D:Point]. (bd=BD) supposing (cd=CD and ad=AD and bc=BC and ac=AC and A_B_C and a_b_c)
Lemma: eu-inner-five-segment'
∀e:EuclideanPlane
∀[a,b,c,A,B,C:Point]. (∀d,D:Point. (bd=BD) supposing (cd=CD and ad=AD)) supposing (bc=BC and ac=AC and A_B_C and a_b\000C_c)
Lemma: eu-inner-three-segment
∀e:EuclideanPlane. ∀[a,b,c,A,B,C:Point]. (ab=AB) supposing (bc=BC and ac=AC and A_B_C and a_b_c)
Lemma: eu-congruent-between-implies-equal
∀e:EuclideanPlane. ∀[a,b,c,x:Point]. (b = x ∈ Point) supposing (a_b_c and ab=ax and bc=xc)
Lemma: eu-congruent-between-exists
∀e:EuclideanPlane. ∀a,b,c,a',c':Point.
(∃b':Point. (a'_b'_c' ∧ ab=a'b' ∧ bc=b'c')) supposing (a_b_c and ac=a'c' and (¬(a = b ∈ Point)))
Lemma: eu-congruent-preserves-between
∀e:EuclideanPlane. ∀[a,b,c,a',b',c':Point]. (a'_b'_c') supposing (bc=b'c' and ac=a'c' and ab=a'b' and a_b_c)
Lemma: eu-colinear-five-segment
∀e:EuclideanPlane
∀[a,b,c,d,A,B,C,D:Point]. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and ac=AC and Colinear(a;b;c))
Lemma: eu-colinear-equidistant
∀e:EuclideanPlane. ∀[a,b,c,p,q:Point]. (cp=cq) supposing (ap=aq and bp=bq and Colinear(a;b;c))
Lemma: eu-between-eq-same-side
∀e:EuclideanPlane. ∀[A,B,C,D:Point]. (¬((¬A_C_D) ∧ (¬A_D_C))) supposing ((¬(A = B ∈ Point)) and A_B_C and A_B_D)
Lemma: eu-between-eq-same-side2
∀e:EuclideanPlane. ∀[A,B,C,D:Point]. (¬((¬B_C_D) ∧ (¬B_D_C))) supposing ((¬(A = B ∈ Point)) and A_B_C and A_B_D)
Lemma: eu-colinear-same-side
∀e:EuclideanPlane
∀[A,B,C,D:Point]. (Colinear(B;C;D)) supposing ((¬(B = C ∈ Point)) and (¬(A = B ∈ Point)) and A_B_C and A_B_D)
Lemma: eu-colinear-same-side2
∀e:EuclideanPlane
∀[A,B,C,D:Point]. (Colinear(A;C;D)) supposing ((¬(A = C ∈ Point)) and (¬(A = B ∈ Point)) and A_B_C and A_B_D)
Lemma: eu-colinear-between
∀e:EuclideanPlane
∀[A,B,C,D:Point]. (Colinear(A;C;D)) supposing ((¬(A = C ∈ Point)) and (¬(A = B ∈ Point)) and A_C_B and A_D_B)
Lemma: eu-colinear-between2
∀e:EuclideanPlane
∀[A,B,C,D:Point]. (Colinear(B;C;D)) supposing ((¬(B = C ∈ Point)) and (¬(A = B ∈ Point)) and A_C_B and A_D_B)
Lemma: eu-colinear-from-between
∀e:EuclideanPlane
∀[A,C,D:Point]. ((¬(A = C ∈ Point)) ⇒ (∃B:Point. ((¬(A = B ∈ Point)) ∧ A_C_B ∧ A_D_B)) ⇒ Colinear(A;C;D))
Lemma: eu-colinear-transitivity
∀e:EuclideanPlane
∀[A,C,B,D:Point]. (Colinear(A;B;C) ⇒ Colinear(B;C;D) ⇒ {((¬(A = C ∈ Point)) ⇒ Colinear(A;C;D)) ∧ Colinear(A;B;D)})
Definition: eu-colinear-set
eu-colinear-set(e;L) == (∀A∈L.(∀B∈L.(∀C∈L.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
Lemma: eu-colinear-set_wf
∀[e:EuclideanPlane]. ∀[L:Point List]. (eu-colinear-set(e;L) ∈ ℙ)
Lemma: eu-colinear-is-colinear-set
∀e:EuclideanPlane. ∀A,B,C:Point. (Colinear(A;B;C) ⇒ eu-colinear-set(e;[A; B; C]))
Lemma: eu-colinear-cons
∀e:EuclideanPlane. ∀L:Point List. ∀A:Point.
(eu-colinear-set(e;[A / L]) ⇐⇒ eu-colinear-set(e;L) ∧ (∀B∈L.(∀C∈L.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
Lemma: eu-colinear-append
∀e:EuclideanPlane. ∀L1,L2:Point List.
((∃A,B:Point. ((¬(A = B ∈ Point)) ∧ ((A ∈ L1) ∧ (A ∈ L2)) ∧ (B ∈ L1) ∧ (B ∈ L2)))
⇒ eu-colinear-set(e;L1)
⇒ eu-colinear-set(e;L2)
⇒ eu-colinear-set(e;L1 @ L2))
Definition: eu-bisect-line
eu-bisect-line(e;a;b) == (¬(a = b ∈ Point)) ∧ (∃d:Point. (ad=db ∧ a_d_b))
Lemma: eu-bisect-line_wf
∀[e:EuclideanPlane]. ∀[a,b:Point]. (eu-bisect-line(e;a;b) ∈ ℙ)
Lemma: test-prove-distinct
∀e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
((Colinear(A;B;X) ∨ A-X-B ∨ B-X-A)
⇒ (A_B_C ∨ C_B_A)
⇒ (Y_C_A ∨ A_C_Y)
⇒ (ZW=AY ∨ ZW=YA)
⇒ ZW=UV
⇒ (¬(U = V ∈ Point)))
Lemma: test-colinear-sets
∀e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
(Colinear(A;B;X) ⇒ A_B_C ⇒ Y_C_A ⇒ (¬(Y = C ∈ Point)) ⇒ Colinear(C;Y;X))
Lemma: eu-add-length-between-iff
∀e:EuclideanPlane. ∀[a,b,c:Point]. uiff(a_b_c;|ac| = |ab| + |bc| ∈ {p:Point| O_X_p} )
Lemma: eu-seg-length-test
∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point]. (ba=xy) supposing (dc=yx and ab=cd)
Lemma: eu-seg-length-test2
∀e:EuclideanPlane. ∀s1,s2:ProperSegment. ∀t1,t2,t3:Segment. (s1 ≡ s2 ⇒ t1 ≡ t2 ⇒ t2 ≡ t3 ⇒ s1 + t1 ≡ s2 + t3)
Lemma: eu-seg-length-test-ext
∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point]. (ba=xy) supposing (dc=yx and ab=cd)
Definition: eu-tri
Triangle(a;b;c) == (¬(a = b ∈ Point)) ∧ (¬(a = c ∈ Point)) ∧ (¬(b = c ∈ Point))
Lemma: eu-tri_wf
∀e:EuclideanPlane. ∀[a,b,c:Point]. (Triangle(a;b;c) ∈ ℙ)
Lemma: line-circle-continuity
∀e:EuclideanPlane. ∀a,b,p:Point. ∀q:{q:Point| ¬(q = p ∈ Point)} .
((∃x:{x:Point| a_x_b ∧ (¬(x = b ∈ Point))} . ∃y:{y:Point| a_b_y} . (ap=ax ∧ aq=ay))
⇒ (∃y,z:Point. (ay=ab ∧ az=ab ∧ z_p_q ∧ p_y_q ∧ (¬(y = z ∈ Point)))))
Lemma: line-circle-continuity1
∀e:EuclideanPlane. ∀a,b,p:Point. ∀q:{q:Point| ¬(q = p ∈ Point)} .
((∃x:{x:Point| a_x_b} . ∃y:{y:Point| a_b_y} . (ap=ax ∧ aq=ay)) ⇒ (∃y,z:Point. (ay=ab ∧ az=ab ∧ z_p_q ∧ p_y_q)))
Lemma: circle-circle-continuity
∀e:EuclideanPlane. ∀a,b,c,d,p,q,x,z:Point.
(∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ ((¬(x = z ∈ Point)) ⇒ (¬(z1 = z2 ∈ Point))))) supposing
(a_b_z and
a_x_b and
cq=cd and
cp=cd and
aq=az and
ap=ax and
(¬(a = c ∈ Point)))
Lemma: circle-circle-continuity2
∀e:EuclideanPlane. ∀a,b,c,d:Point.
((¬(a = c ∈ Point))
⇒ (∃p,q,x,z:Point. ((a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd) ∧ (¬(x = z ∈ Point))))
⇒ (∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ (¬(z1 = z2 ∈ Point)))))
Lemma: circle-circle-continuity1
∀e:EuclideanPlane. ∀a,b,c,d:Point.
((¬(a = c ∈ Point))
⇒ (∃p,q,x,z:Point. (a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd))
⇒ (∃y:Point. (ay=ab ∧ cy=cd)))
Definition: eu-bisect-angle
eu-bisect-angle(e;a;b;c) ==
(¬(a = b ∈ Point)) ∧ (¬(b = c ∈ Point)) ∧ (∃d:Point. ((¬(d = a ∈ Point)) ∧ (¬(d = c ∈ Point)) ∧ abd = dbc))
Lemma: eu-bisect-angle_wf
∀e:EuclideanPlane. ∀a,b,c:Point. (eu-bisect-angle(e;a;b;c) ∈ ℙ)
Lemma: eu-5segSAS
∀e:EuclideanPlane. ∀a,b,c,f,g,A,B,C,F,G:Point.
(af=AF ∧ fb=FB ∧ bc=BC ∧ ag=AG ∧ gc=GC) ⇒ fg=FG
supposing (Triangle(a;f;g) ∧ Triangle(A;F;G)) ∧ a_f_b ∧ a_g_c ∧ A_F_B ∧ A_G_C
Definition: eu-cong-angle
abc = xyz ==
(¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(x = y ∈ Point))
∧ (¬(z = y ∈ Point))
∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba'=yx' ∧ bc'=yz' ∧ a'c'=x'z'))
Lemma: eu-cong-angle_wf
∀[e:EuclideanPlane]. ∀[a,b,c,x,y,z:Point]. (abc = xyz ∈ ℙ)
Lemma: eu-cong-angle-symm
∀e:EuclideanPlane. ∀a,b,c:Point. abc = cba supposing (¬(a = b ∈ Point)) ∧ (¬(c = b ∈ Point))
Lemma: eu-cong-angle-symm2
∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point. (xyz = abc ⇒ abc = xyz)
Definition: eu-cong-tri
Cong3(abc,a'b'c') == ab=a'b' ∧ bc=b'c' ∧ ca=c'a'
Lemma: eu-cong-tri_wf
∀[e:EuclideanPlane]. ∀[a,b,c,a',b',c':Point]. (Cong3(abc,a'b'c') ∈ ℙ)
Definition: eu-out
out(p ab) == (¬(p = a ∈ Point)) ∧ (¬(p = b ∈ Point)) ∧ (¬((¬p_a_b) ∧ (¬p_b_a)))
Lemma: eu-out_wf
∀[e:EuclideanPlane]. ∀[p,a,b:Point]. (out(p ab) ∈ ℙ)
Lemma: eu-out-refl
∀e:EuclideanPlane. ∀a,b,c:Point. (out(a bc) ⇒ out(a cb))
Definition: eu-five-seg-compressed
FSC(a;b;c;d a';b';c';d') == Colinear(a;b;c) ∧ Cong3(abc,a'b'c') ∧ ad=a'd' ∧ bd=b'd'
Lemma: eu-five-seg-compressed_wf
∀[e:EuclideanPlane]. ∀[a,b,c,d,a',b',c',d':Point]. (FSC(a;b;c;d a';b';c';d') ∈ ℙ)
Lemma: eu-fsc-ap
∀e:EuclideanPlane. ∀a,b,c,d,a',b',c',d':Point. (FSC(a;b;c;d a';b';c';d') ⇒ (¬(a = b ∈ Point)) ⇒ cd=c'd')
Definition: eu-midpoint
a=m=b == a_m_b ∧ am=mb
Lemma: eu-midpoint_wf
∀[e:EuclideanPlane]. ∀[m,a,b:Point]. (a=m=b ∈ ℙ)
Lemma: eu-midpoint-trivial
∀e:EuclideanPlane. ∀a,b:Point. (a=b=a ⇒ (a = b ∈ Point))
Definition: eu-perpendicular
Per(a;b;c) == ∃c':Point. (c=b=c' ∧ ac=ac')
Lemma: eu-perpendicular_wf
∀[e:EuclideanPlane]. ∀[a,b,c:Point]. (Per(a;b;c) ∈ ℙ)
Definition: eu-perp-in
ab ⊥x cd == Colinear(a;b;x) ∧ Colinear(c;d;x) ∧ (∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Per(u;x;v)))
Lemma: eu-perp-in_wf
∀[e:EuclideanPlane]. ∀[x,a,b,c,d:Point]. (ab ⊥x cd ∈ ℙ)
Definition: eu-perp
ab ⊥ cd == ∃x:Point. ab ⊥x cd
Lemma: eu-perp_wf
∀[e:EuclideanPlane]. ∀[a,b,c,d:Point]. (ab ⊥ cd ∈ ℙ)
Definition: eu-le-pt
ab≤cd == ∃y:Point. (c_y_d ∧ ab=cy)
Lemma: eu-le-pt_wf
∀[e:EuclideanStructure]. ∀[a,b,c,d:Point]. (ab≤cd ∈ ℙ)
Lemma: eu-perp-three
∀e:EuclideanPlane. ∀x,a,b,c:Point. (ba ⊥x ca ⇒ (x = a ∈ Point))
Lemma: eu-be-neq
∀e:EuclideanPlane. ∀a,b,c:Point. ((¬(a = b ∈ Point)) ⇒ a_b_c ⇒ (¬(a = c ∈ Point)))
Lemma: eu-conga-to-cong3
∀E:EuclideanPlane. ∀a,b,c,d,e,f:Point.
(abc = def ⇒ (∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))))
Lemma: eu-between-eq-seg-eq
∀e:EuclideanPlane. ∀a,b,c,a',b',c':Point. (a_b_c ⇒ a'_b'_c' ⇒ ab=a'b' ⇒ ac=a'c' ⇒ bc=b'c')
Lemma: eu-eqt
∀e:EuclideanPlane. ∀a,b,c:{p:Point| O_X_p} .
(((a = b ∈ {p:Point| O_X_p} ) ∧ (b = c ∈ {p:Point| O_X_p} )) ⇒ (a = c ∈ {p:Point| O_X_p} ))
Lemma: eu-eq-x-implies-eq
∀e:EuclideanPlane. ∀a,b:Point. ((X = |ab| ∈ {p:Point| O_X_p} ) ⇒ (a = b ∈ Point))
Lemma: eu-sum-eq-x
∀e:EuclideanPlane. ∀a,b,c,d:Point. ((X = |ab| + |cd| ∈ {p:Point| O_X_p} ) ⇒ ((a = b ∈ Point) ∧ (c = d ∈ Point)))
Lemma: eu-ab-eq-x
∀e:EuclideanPlane. ∀a,b:Point. ((a = b ∈ Point) ⇒ (X = |ab| ∈ {p:Point| O_X_p} ))
Lemma: eu-colinear-switch
∀e:EuclideanPlane. ∀a,b,c:Point. (Colinear(a;b;c) ⇒ (¬(a = c ∈ Point)) ⇒ Colinear(a;c;b))
Lemma: eu-colinear-switch2
∀e:EuclideanPlane. ∀a,b,c:Point. (Colinear(a;b;c) ⇒ Colinear(b;a;c))
Lemma: eu-colinear-switch3
∀e:EuclideanPlane. ∀a,b,c:Point. ((¬(c = b ∈ Point)) ⇒ Colinear(a;b;c) ⇒ Colinear(c;b;a))
Lemma: eu-colinear-trivial
∀e:EuclideanPlane. ∀a,b:Point. ((¬(a = b ∈ Point)) ⇒ (Colinear(a;b;b) ∧ Colinear(b;a;b)))
Lemma: eu-cong3-to-conga-aux
∀e:EuclideanPlane. ∀b,a,a',a0,e0,d,d',d0:Point.
(out(b aa') ⇒ out(e0 dd') ⇒ b_a_a0 ⇒ e0_d_d0 ⇒ ba'=e0d' ⇒ aa0=e0d ⇒ dd0=ba ⇒ (ba0=e0d0 ∧ a'a0=d'd0))
Lemma: eu-cong3-to-conga
∀e:EuclideanPlane. ∀a,b,c,d,E,f:Point.
((∃a',c',d',f':Point. (out(b a'a) ∧ out(b c'c) ∧ out(E d'd) ∧ out(E f'f) ∧ Cong3(a'bc',d'Ef'))) ⇒ abc = dEf)
Lemma: eu-be-compress
∀e:EuclideanPlane. ∀a,b,c:Point. (a_b_c ⇒ a_c_b ⇒ (b = c ∈ Point))
Lemma: eu-inner-pasch-ex
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| ¬Colinear(a;b;c)} . ∀p:{p:Point| a-p-c} . ∀q:{q:Point| b_q_c} .
∃x:Point. (p-x-b ∧ q-x-a ∧ (x = eu-inner-pasch(e;a;b;c;p;q) ∈ Point))
Lemma: eu-be-end-eq
∀e:EuclideanPlane. ∀a,b,c:Point. (a_b_c ⇒ ab=ac ⇒ (b = c ∈ Point))
Lemma: eu-between-eq-middle
∀e:EuclideanPlane. ∀a,b,c,d:Point. ((¬(a = d ∈ Point)) ⇒ a_b_d ⇒ a_c_d ⇒ (¬((¬b_c_d) ∧ (¬c_b_d))))
Lemma: eu-eq-implies-col
∀e:EuclideanPlane. ∀a,b,c:Point. ((¬(a = b ∈ Point)) ⇒ (b = c ∈ Point) ⇒ Colinear(a;b;c))
Lemma: eu-col-connect
∀e:EuclideanPlane. ∀a,b,c,d:Point. (Colinear(a;b;c) ⇒ Colinear(c;b;d) ⇒ Colinear(a;b;d))
Lemma: p8eu
∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
Cong3(abc,xyz) ⇒ (abc = xyz ∧ bac = yxz ∧ bca = yzx) supposing Triangle(a;b;c) ∧ Triangle(x;y;z)
Lemma: eu-bisect-angle
∀e:EuclideanPlane. ∀a,b,c:Point.
((¬(a = b ∈ Point)) ⇒ (¬(b = c ∈ Point)) ⇒ (∃d:Point. ((¬(d = a ∈ Point)) ∧ (¬(d = c ∈ Point)) ∧ abd = dbc)))
Lemma: eu-sas
∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
((ab=AB ∧ ac=AC) ∧ bac = BAC) ⇒ bc=BC supposing Triangle(a;b;c) ∧ Triangle(A;B;C)
Lemma: p5eu
∀e:EuclideanPlane. ∀a,b,c:Point. ((ab=ac ∧ Triangle(a;b;c)) ⇒ (∃j,k:Point. jbc = kcb))
Lemma: p4eu
∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
(ab=AB ∧ ac=AC ∧ bac = BAC) ⇒ (bc=BC ∧ abc = ABC ∧ bca = BCA ∧ Cong3(abc,ABC))
supposing Triangle(a;b;c) ∧ Triangle(A;B;C)
Comment: Editor aliases for Constructive Geometry
All theorems of constructive geometry have the form
⌜∀e:EuclideanPlane. [prop]⌝
(to enter that type "all" and then "eu-pl" in the [type] slot).
To edit formulas about geometry use the following editor aliases:
eu-pt ⌜eu-point([term])⌝ --then fill in e (your EuclideanPlane) and it will
display as ⌜Point⌝
eu-cong ⌜ab=cd⌝ --- first slot is e (your EuclideanPlane) then a, b, c, d.
eu-bt ⌜a-b-c⌝ -- this is strict betweeness, first slot is e.
eu-be ⌜a_b_c⌝ -- non-strict betweeness ( ⌜a = b ∈ Point⌝ and ⌜b = c ∈ Point⌝ are allowed).
⋅
Comment: Tactics for Constructive Geometry
All theorems of constructive geometry have the form
⌜∀e:EuclideanPlane. [prop]⌝
To prove a theorem like
⌜∀e:EuclideanPlane. ∀a,b:Point. (P (a; b) ⇒ (∃c:Point. Q (a; b; c)))⌝
one typically starts with
Auto and then "construct" the desired point c by instantiating
lemmas (that have already been proved to construct points)
or invoking the basic constructions.
To invove the construction that extends the segments AB by the segment CD,
use the tactic
Prolong ⌜A⌝ ⌜B⌝ `x' ⌜C⌝ ⌜D⌝
The points A, B, C, D will usually be variables (of type ⌜Point⌝) but
the can be expressions, too, so they are Nuprl terms
(type control-o to get a ⌜[term]⌝ slot). The `x' is a ML variable.
It is used to name the new endpoint of the extended segment.
We have added "circle-circle-continutity" as a theorem
(it is unproved, so far, but does follow from the axioms, so it is safe
to use it in proofs). It lets you construct the intersection point(s) of
two cicles that overlap.
To invoke that use either
CircleCircle1 ⌜a⌝;⌜b⌝ ⌜c⌝ ⌜d⌝ `x'
or
CircleCircle2 ⌜a⌝;⌜b⌝ ⌜c⌝ ⌜d⌝ `x' `y'
(for more information about these, see: Error :circle-circle-tactics).
"line-circle-continuity" is one of our axioms.
It lets you construct the intersection point(s) of a line and a circle
(that overlap).
Use
CircleLine1 ⌜a⌝;⌜b⌝ ⌜u⌝ ⌜v⌝ `x' `y'
or
CircleLine2 ⌜a⌝;⌜b⌝ ⌜u⌝ ⌜v⌝ `x' `y'
(see Error :line-circle-tactics for more information).
To construct the "crossing point" for segments ab and cd (and name it x),
use SegmentsCross ⌜a⌝ ⌜b⌝ ⌜c⌝ ⌜d⌝ `x'
.
⋅
Lemma: euclid-P1
∀e:EuclideanPlane. ∀A,B:Point. ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)
Lemma: euclid-P1-ext
∀e:EuclideanPlane. ∀A,B:Point. ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)
Lemma: euclid-P2
∀e:EuclideanPlane. ∀A,B,C:Point. ∃L:Point. AL=BC supposing ¬(A = B ∈ Point)
Comment: proposition 3
In proposition3, segment AB is "longer than" line C.
We use a segment C1C2 for C, but we still have to define
what it means for AB to be longer than C1C2.
We can use the lengths ⌜|AB|⌝ and ⌜|C1C2|⌝
(which are points in ⌜{p:Point| O_X_p} ⌝ )
but we need to define the "lt" (less-than) relation on them.
For p and q in ⌜{p:Point| O_X_p} ⌝ we say ⌜p ≤ q⌝ if
⌜X_p_q⌝ and ⌜p < q⌝ if ⌜p ≤ q ∧ (¬(p = q ∈ Point))⌝⋅
Lemma: euclid-P3
∀e:EuclideanPlane. ∀A,B,C1,C2:Point. ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (¬(C1 = C2 ∈ Point)) ∧ |C1C2| < |AB|
Lemma: euclid-P3-ext
∀e:EuclideanPlane. ∀A,B,C1,C2:Point. ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (¬(C1 = C2 ∈ Point)) ∧ |C1C2| < |AB|
Lemma: e1
∀e:EuclideanPlane. ∀A,B:Point. ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)
Lemma: p4eu
∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
(ab=AB ∧ ac=AC ∧ bac = BAC) ⇒ (bc=BC ∧ abc = ABC ∧ bca = BCA ∧ Cong3(abc,ABC))
supposing Triangle(a;b;c) ∧ Triangle(A;B;C)
Home
Index