Freek and John, here's 2 miz3 bug reports. First, John, thanks for
spotting my funny ∧ (should be /\) in my `on_line' def!
BUG1) Paste in my Tarski geometry miz3 code (updated version below) or
any reasonable version of it, and then paste in
let I1part1_THM = thm `;
let a b c x be point;
assume Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) [X1];
thus Between (a,b,x) \/ Between (b,x,a) \/ Between (x,a,b)
proof
qed by X1,Bsymmetry_THM`;;
This works, and gives the expected output
|- !a b c x.
Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b)
==> Between (a,b,x) \/ Between (b,x,a) \/ Between (x,a,b)
The bug is that this code (like Freek's drinker's code on p 13--14)
does not seem to fit Freek's grammer on p 16, which say on the top
line that a lemma must be of the form
let ident = thm `; formula proof; `;;
This doesn't happen unles we say that the let, assume and thus lines
comprise a formula. There's no definition of formula, and I wouldn't
expect formulas to contain labels or semicolons.
The let and assume lines are proof steps, but the thus line is not.
I don't say this to nitpick, but out of a real interest in
understanding first the syntax and then the semantics of miz3.
BUG2) A modification of the above working code doesn't not work:
let I1part1_THM = thm `;
let a b c x be point;
assume Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) [X1];
assume Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) [X2];
thus ((Between (a,b,x) /\ Between (a,b,c)) \/
(Between (a,b,x) /\ Between (a,c,b)) \/
(Between (a,b,x) /\ Between (c,a,b)) \/
(Between (a,x,b) /\ Between (a,b,c)) \/
(Between (a,x,b) /\ Between (a,c,b)) \/
(Between (a,x,b) /\ Between (c,a,b)) \/
(Between (x,a,b) /\ Between (a,b,c)) \/
(Between (x,a,b) /\ Between (a,c,b)) \/
(Between (x,a,b) /\ Between (c,a,b)))
proof
qed by X1, X2`;;
The error at the end is
::#2
:: 2: inference time-out
`,
(0, 1, 0)).
--
Best,
Bill
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.ml";;
#use "John5-8ModelTarski.ml";;
then paste in the following file*)
(* ================================================================= *)
(* HOL Light Tarski geometry axiomatic proofs up to Gupta's theorem. *)
(* ================================================================= *)
(* Proof assistants like HOL Light can be used to help teach rigorous
axiomatic geometry in high school using Hilbert's axioms, and
introduce students to the world of formal proofs, which should
become a hot area in debugging computer software.
This is a port, mostly due to John Harrison, of Mizar code, which
was heavily influenced by Julien Narboux's Coq pseudo-code
http://dpt-info.u-strasbg.fr/~narboux/tarski.html and Wojciech
A. Trybulec's incsp_1.miz in the MML library on axioms of incidence
geometry. We partially prove the theorem of the 1983 book
Metamathematische Methoden in der Geometrie by Schwabhäuser,
Szmielew, and Tarski, that Tarski's (extremely weak!) plane
geometry axioms imply Hilbert's axioms. We get about as far as
Narboux, with Gupta's amazing proof which implies Hilbert's axiom
I1 that two points determine a line.
Thanks to Mizar folks who wrote an influential language I was able
to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
Light, and especially John Harrison, who came up with the entire
framework of porting my axiomatic proofs to HOL Light. *)
new_type("point",0);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("equal_line",(12, "right"));;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
let cong_DEF = new_definition
`a,b,c cong x,y,z <=>
a,b === x,y /\ a,c === x,z /\ b,c === y,z`;;
let is_ordered_DEF = new_definition
`is_ordered (a,b,c,d) <=>
Between (a,b,c) /\ Between (a,b,d) /\ Between (a,c,d) /\ Between (b,c,d)`;;
let Collinear_DEF = new_definition
`Collinear(a,b,c) <=>
Between (a,b,c) \/ Between (b,c,a) \/ Between (c,a,b)`;;
let Line_DEF = new_definition
`on_line(x,a,b) <=>
~(a = b) /\ (Between (a,b,x) \/ Between (b,x,a) \/ Between (x,a,b))`;;
let LineEq_DEF = new_definition
`a,b equal_line x,y <=>
~(a = b) ∧ ~(x = y) ∧ ! c . on_line(c,a,b) <=> c on_line(c,x,y);
end;
(* ------------------------------------------------------------------------- *)
(* The axioms. *)
(* ------------------------------------------------------------------------- *)
let A1 = new_axiom
`!a b. a,b === b,a`;;
let A2 = new_axiom
`!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`;;
let A3 = new_axiom
`!a b c. a,b === c,c ==> a = b`;;
let A4 = new_axiom
`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;
let A5 = new_axiom
`!a b c x a' b' c' x'.
~(a = b) /\ a,b,c cong a',b',c' /\
Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x'
==> c,x === c',x'`;;
let A6 = new_axiom
`!a b. Between(a,b,a) ==> a = b`;;
let A7 = new_axiom
`!a b p q z.
Between(a,p,z) /\ Between(b,q,z) ==>
?x. Between(p,x,b) /\ Between(q,x,a)`;;
(* A4 is the Segment Construction axiom, A5 is the SAS axiom and A7 is
the Inner Pasch axiom. There are 4 more axioms we're not using yet:
there exist 3 non-collinear points;
3 points equidistant from 2 distinct points are collinear;
Euclid's parallel postulate;
a first order version of Hilbert's Dedekind Cuts axiom.
We shall say we apply SAS to a+cbx and a'+c'b'x'. Normally one
applies SAS by showing cb = c'b' bx = b'x' (which we assume) and
angle cbx cong angle c'b'x'. One might prove the angle congruence
by showing that the triangles abc /\ a'b'c' were congruent by SSS
(which we also assume) and then apply the theorem that complements
of congruent angles are congruent. Hence Tarski's axiom. *)
(* ------------------------------------------------------------------------- *)
(* Now Mizarlight versions of the actual proofs. *)
(* ------------------------------------------------------------------------- *)
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let EquivReflexive = thm `;
!a b. a,b === a,b
proof
let a b be point;
b,a === a,b by A1;
qed by -, A2`;;
let EquivSymmetric = thm `;
!a b c d. a,b === c,d ==> c,d === a,b
proof
let a b c d be point;
assume a,b === c,d [1];
a,b === a,b by EquivReflexive;
qed by -, 1, A2`;;
let EquivTransitive = thm `;
!a b p q r s . a,b === p,q /\ p,q === r,s ==> a,b === r,s
proof
let a b p q r s be point;
assume a,b === p,q [H1];
assume p,q === r,s [H2];
p,q === a,b by H1, EquivSymmetric;
qed by -, H2, A2`;;
let Baaa_THM = thm `;
!a b. Between (a,a,a) /\ a,a === b,b
proof
let a b be point;
consider x such that Between (a,a,x) /\ a,x === b,b [X1] by A4;
a = x by -, A3;
qed by -, X1`;;
let Bqaa_THM = thm `;
!a q. Between(q,a,a)
proof
let a q be point;
consider x such that Between(q,a,x) /\ a,x === a,a [X1] by A4;
a = x by -, A3;
qed by -, X1`;;
let C1_THM = thm `;
let a b x y be point;
assume ~(a = b) [H1];
assume Between (a,b,x) [H2];
assume Between (a,b,y) [H3];
assume b,x === b,y [H4];
thus y = x
proof
a,b === a,b /\ a,y === a,y /\ b,y === b,y by EquivReflexive;
a,b,y cong a,b,y by -, cong_DEF;
y,x === y,y by -, H1, H2, H3, H4, A5;
qed by -, A3`;;
let Bsymmetry_THM = thm `;
let a p z be point;
thus Between (a,p,z) ==> Between (z,p,a)
proof
assume Between (a,p,z) [H1];
Between (p,z,z) by Bqaa_THM;
consider x such that
Between (p,x,p) /\ Between (z,x,a) [X1] by -, H1, A7;
x = p by -, A6;
qed by -, X1`;;
let Baaq_THM = thm `;
let a q be point;
thus Between (a,a,q)
proof
Between (q,a,a) by Bqaa_THM;
qed by -, Bsymmetry_THM`;;
let BEquality_THM = thm `;
let a b c be point;
thus Between (a,b,c) /\ Between (b,a,c) ==> a = b
proof
assume Between (a,b,c) [H1];
assume Between (b,a,c);
? x . Between (b,x,b) /\ Between (a,x,a) by -, H1, A7;
consider x such that
Between (b,x,b) /\ Between (a,x,a) [X1] by -;
b = x by X1, A6;
Between (a,b,a) by -, X1;
qed by -, A6`;;
let B124and234then123_THM = thm `;
let a b c d be point;
assume Between (a,b,d) [H1];
assume Between (b,c,d) [H2];
thus Between (a,b,c)
proof
? x . Between (b,x,b) /\ Between (c,x,a) by H1, H2, A7;
consider x such that
Between (b,x,b) /\ Between (c,x,a) [X1] by -;
b = x by X1, A6;
Between (c,b,a) by -, X1;
qed by -, Bsymmetry_THM`;;
let BTransitivity_THM = thm `;
let a b c d be point;
assume ~(b = c) [H1];
assume Between (a,b,c) [H2];
assume Between (b,c,d) [H3];
thus Between (a,c,d)
proof
consider x such that
Between (a,c,x) /\ c,x === c,d [X1] by A4;
Between (x,c,a) [X2] by -, Bsymmetry_THM;
Between (c,b,a) by H2, Bsymmetry_THM;
Between (x,c,b) by -, X2, B124and234then123_THM;
Between (b,c,x) by -, Bsymmetry_THM;
x = d by -, H1, H3, X1, C1_THM;
qed by -, X1`;;
let BTransitivityOrdered_THM = thm `;
let a b c d be point;
assume ~(b = c) [H1];
assume Between (a,b,c) [H2];
assume Between (b,c,d) [H3];
thus is_ordered (a,b,c,d)
proof
Between (a,c,d) [X1] by H1, H2, H3, BTransitivity_THM;
Between (d,c,b) [X2] by H3, Bsymmetry_THM;
Between (c,b,a) by -, H2, Bsymmetry_THM;
Between (d,b,a) by -, H1, X2, BTransitivity_THM;
Between (a,b,d) by -, Bsymmetry_THM;
qed by H2, -, X1, H3, is_ordered_DEF`;;
(*
let BTransitivityOrdered_THM = thm `;
! a b c d .
~(b = c) /\ Between (a,b,c) /\ Between (b,c,d) ==> ORDERED a,b,c,d
proof
let a b c d be point;
assume ~(b = c) [H1];
assume Between (a,b,c) [H2];
assume Between (b,c,d) [H3];
Between (a,c,d) [X1] by H1, H2, H3, BTransitivity_THM;
Between (d,c,b) [X2] by H3, Bsymmetry_THM;
Between (c,b,a) by -, H2, Bsymmetry_THM;
Between (d,b,a) by -, H1, X2, BTransitivity_THM;
Between (a,b,d) by -, Bsymmetry_THM;
thus ORDERED a,b,c,d by H2, -, X1, H3, ORDERED_DEF;
end`;;
*)
let B124and234Ordered_THM = thm `;
let a b c d be point;
assume Between (a,b,d) [H1];
assume Between (b,c,d) [H2];
thus is_ordered (a,b,c,d)
proof
cases;
suppose b = c [P1];
Between (a,b,c) [P2] by -, Bqaa_THM;
Between (a,c,d) by P1, H1;
qed by P2, H1, -, H2, is_ordered_DEF;
suppose ~(b = c) [Q1];
Between (a,b,c) by H1, H2, B124and234then123_THM;
qed by -, Q1, H2, BTransitivityOrdered_THM;
end`;;
let SegmentAddition_THM = thm `;
let a b c a' b' c' be point;
assume Between (a,b,c) [H1];
assume Between (a',b',c') [H2];
assume a,b === a',b' [H3];
assume b,c === b',c' [H4];
thus a,c === a',c'
proof
cases;
suppose a = b [Y1];
a,a === a',b' by H3, Y1;
a',b' === a,a by -, EquivSymmetric;
a' = b' by -, A3;
qed by -, H4, Y1;
suppose ~(a = b) [Z1];
b,a === a,b by A1;
b,a === a',b' [Z2] by -, H3, EquivTransitive;
a',b' === b',a' by A1;
b,a === b',a' [Z3] by -, Z2, EquivTransitive;
a,a === a',a' by Baaa_THM;
a,b,a cong a',b',a' by -, H3, Z3, cong_DEF;
qed by -, Z1, H1, H2, H4, A5;
end`;;
let CongruenceDoubleSymmetry_THM = thm `;
let a b c d be point;
assume a,b === c,d [H1];
thus b,a === d,c
proof
b,a === a,b /\ c,d === d,c [X1] by H1, A1;
a,b === d,c by H1, X1, EquivTransitive;
qed by -, X1, EquivTransitive`;;
let C1prime_THM = thm `;
let a b x y be point;
assume ~(a = b) [H1];
assume Between (a,b,x) [H2];
assume Between (a,b,y) [H3];
assume a,x === a,y [H4];
thus x = y
proof
consider m such that
Between (b,a,m) /\ a,m === a,b [X1] by A4;
Between (m,a,b) [X2] by X1, Bsymmetry_THM;
~(m = a) [X3] by X1, EquivSymmetric, A3, H1;
is_ordered (m,a,b,x) by H1, X2, H2, BTransitivityOrdered_THM;
Between (m,a,x) [X4] by -, is_ordered_DEF;
is_ordered (m,a,b,y) by H1, X2, H3, BTransitivityOrdered_THM;
Between (m,a,y) by -, is_ordered_DEF;
qed by -, X3, X4, H4, C1_THM`;;
let SegmentSubtraction_THM = thm `;
let a b c a' b' c' be point;
assume Between (a,b,c) [H1];
assume Between (a',b',c') [H2];
assume a,b === a',b' [H3];
assume a,c === a',c' [H4];
thus b,c === b',c'
proof
cases;
suppose a = b [Y1];
a,a === a',b' by -, H3;
a',b' === a,a by -, EquivSymmetric;
a' = b' by -, A3;
qed by -, H4, Y1;
suppose ~(a = b) [Z1];
consider x such that
Between (a,b,x) /\ b,x === b',c' [Z2] by A4;
a,x === a',c' [Z3] by Z2, H2, H3, SegmentAddition_THM;
a',c' === a,c by H4, EquivSymmetric;
a,x === a,c by -, Z3, EquivTransitive;
x = c by -, Z1, Z2, H1, C1prime_THM;
qed by -, Z2;
end`;;
let EasyAngleTransport_THM = thm `;
let a O b be point;
assume ~(O = a) [H1];
thus ? x y .
Between (b,O,x) /\ Between (a,O,y) /\ x,y,O cong a,b,O
proof
consider x such that
Between (b,O,x) /\ O,x === O,a [X2] by A4;
x,O === a,O [X3] by -, CongruenceDoubleSymmetry_THM;
a,O === x,O [X4] by -, EquivSymmetric;
a,x === x,a by A1;
a,O,x cong x,O,a [X5] by X4, -, X2, cong_DEF;
consider y such that
Between (a,O,y) /\ O,y === O,b [X6] by A4;
Between (x,O,b) by X2 ,Bsymmetry_THM;
x,y === a,b [X7] by H1, X5, X6, -, A5;
y,O === b,O by X6, CongruenceDoubleSymmetry_THM;
x,y,O cong a,b,O by X7, X3, -, cong_DEF;
qed by X2, X6, -`;;
let B123and134Ordered_THM = thm `;
let a b c d be point;
assume Between (a,b,c) [H1];
assume Between (a,c,d) [H2];
thus is_ordered (a,b,c,d)
proof
Between (d,c,a) /\ Between (c,b,a) by H2, H1, Bsymmetry_THM;
is_ordered (d,c,b,a) by -, B124and234Ordered_THM;
Between (d,b,a) /\ Between (d,c,b) by -, is_ordered_DEF;
Between (a,b,d) /\ Between (b,c,d) by -, Bsymmetry_THM;
thus is_ordered (a,b,c,d) by -, H1, H2, is_ordered_DEF;
end`;;
let BextendToLine_THM = thm `;
let a b c d be point;
assume ~(a = b) [H1];
assume Between (a,b,c) [H2];
assume Between (a,b,d) [H3];
thus ? x .
is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x)
proof
consider u such that
Between (a,c,u) /\ c,u === b,d [X1] by A4;
is_ordered (a,b,c,u) [X2] by H2, X1, B123and134Ordered_THM;
Between (b,c,u) by X2, is_ordered_DEF;
Between (u,c,b) [X3] by -, Bsymmetry_THM;
u,c === c,u by A1;
u,c === b,d [X4] by -, X1, EquivTransitive;
Between (a,b,u) [X5] by X2, is_ordered_DEF;
consider x such that
Between (a,d,x) /\ d,x === b,c [Y1] by A4;
is_ordered (a,b,d,x) [Y2] by H3, Y1, B123and134Ordered_THM;
Between (b,d,x) [Y3] by -, is_ordered_DEF;
b,c === d,x [Y4] by Y1, EquivSymmetric;
c,b === b,c by A1;
c,b === d,x [Y5] by -, Y4, EquivTransitive;
Between (a,b,x) [Y6] by Y2, is_ordered_DEF;
u,b === b,x [X6] by X3, Y3, X4, Y5, SegmentAddition_THM;
b,u === u,b by A1;
b,u === b,x by -, X6, EquivTransitive;
u = x by -, H1, X5, Y6, C1_THM;
qed by -, X2, Y2`;;
let GuptaEasy_THM = thm `;
let a b c d be point;
assume ~(a = b) [H1];
assume Between (a,b,c) [H2];
assume Between (a,b,d) [H3];
assume ~(b = c) [H4];
assume ~(b = d) [H5];
thus ~ Between (c,b,d)
proof
cases;
suppose ~ Between (c,b,d);
qed by -;
suppose Between (c,b,d) [H6];
? x . is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x)
by H1, H2, H3, BextendToLine_THM;
consider x such that
is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) [X1] by -;
Between (b,d,x) by X1, is_ordered_DEF;
is_ordered (c,b,d,x) by -, H5, H6, BTransitivityOrdered_THM;
Between (b,c,x) /\ Between (c,b,x) by -, X1, is_ordered_DEF;
b = c [X2] by -, BEquality_THM;
F by -, H4, X2;
qed by -;
end`;;
(* The next result is like SAS: there are 5 pairs of segments 4
equivalent. We say we apply Inner5Segments to abc-x and a'b'c'-x' *)
let Inner5Segments_THM = thm `;
let a b c x a' b' c' x' be point;
assume a,b,c cong a',b',c' [H1];
assume Between (a,x,c) [H2];
assume Between (a',x',c') [H3];
assume c,x === c',x' [H4];
thus b,x === b',x'
proof
a,b === a',b' /\ a,c === a',c' /\ b,c === b',c' [X1] by H1, cong_DEF;
cases;
suppose x = c [Case1];
c',x' === c,c by H4, Case1, EquivSymmetric;
x' = c' by -, A3;
qed by -, Case1, X1;
suppose ~(x = c) [Case2];
~(a = c) [X2] by H2, A6, Case2;
consider y such that
Between (a,c,y) /\ c,y === a,c [X3] by A4;
consider y' such that
Between (a',c',y') /\ c',y' === a,c [X4] by A4;
a,c === c',y' by X4, EquivSymmetric;
c,y === c',y' [X5] by -, X3, EquivTransitive;
c,b === c',b' [X6] by X1, CongruenceDoubleSymmetry_THM;
a,c,b cong a',c',b' by cong_DEF, X1, X6;
b,y === b',y' [X7] by -, X2, X3, X4, X5, A5;
~(y = c) [X8] by X3, EquivSymmetric, A3, X2;
Between (y,c,a) /\ Between (c,x,a) by X3, H2, Bsymmetry_THM;
Between (y,c,x) [X9] by -, B124and234then123_THM;
Between (y',c',a') /\ Between (c',x',a') by -, X4, H3, Bsymmetry_THM;
Between (y',c',x') [X10] by -, B124and234then123_THM;
y,c === y',c' /\ y,b === y',b' by X5, X7, CongruenceDoubleSymmetry_THM;
y,c,b cong y',c',b' by -, cong_DEF, X6;
qed by -, X8, X9, X10, H4, A5;
end`;;
let RhombusDiagBisect_THM = thm `;
let b c d c' d' be point;
assume Between (b,c,d') [H1];
assume Between (b,d,c') [H2];
assume c,d' === c,d [H3];
assume d,c' === c,d [H4];
assume d',c' === c,d [H5];
thus ? e .
Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e
proof
Between (d',c,b) /\ Between (c',d,b) [X1] by H1, H2, Bsymmetry_THM;
consider e such that
Between (c,e,c') /\ Between (d,e,d') [X2] by X1, A7;
c,d === c,d' [X3] by H3, EquivSymmetric;
c,c' === c,c' [X4] by EquivReflexive;
c,d === d',c' by H5, EquivSymmetric;
d,c' === d',c' by -, H4, EquivTransitive;
c,d,c' cong c,d',c' by -, X3, X4, cong_DEF;
d,e === d',e [X5] by -, X2, EquivReflexive, Inner5Segments_THM;
d,c === c,d [X6] by A1;
c,d === d,c' by H4, EquivSymmetric;
d,c === d,c' [X7] by -, X6, EquivTransitive;
d,d' === d,d' [X8] by EquivReflexive;
c,d === d',c' [X9] by H5, EquivSymmetric;
d',c' === c',d' by A1;
c,d === c',d' by -, X9, EquivTransitive;
c,d' === c',d' [X10] by -, H3, EquivTransitive;
d,d' === d,d' by EquivReflexive;
d,c,d' cong d,c',d' by -, X7, X8, X10, cong_DEF;
c,e === c',e by -, X2, EquivReflexive, Inner5Segments_THM;
qed by -, X2, X5`;;
let FlatNormal_THM = thm `;
let a b c d d' e be point;
assume Between (b,c,d') [H1];
assume Between (d,e,d') [H2];
assume c,d' === c,d [H3];
assume d,e === d',e [H4];
assume ~(c = d) [H5];
assume ~(e = d) [H6];
thus ? p r q .
Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\
r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e
proof
~(c = d') by H5, H3, EquivSymmetric, A3;
consider p r such that
Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by
-, EasyAngleTransport_THM;
p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1, cong_DEF;
d',e === d,e by H4, EquivSymmetric;
p,r === d,e [X3] by -, X2, EquivTransitive;
~(p = r) [X4] by -, EquivSymmetric, H6, A3;
consider q such that
Between (p,r,q) /\ r,q === e,d [X5] by A4;
Between (d',e,d) [X6] by H2, Bsymmetry_THM;
c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM;
c,p === c,d [X7] by -, H3, EquivTransitive;
:: Apply SAS to p+crq /\ d'+ced
c,q=== c,d by X4, X1, X5, X6, A5;
c,d=== c,q by -, EquivSymmetric;
c,p=== c,q [X8] by -, X7, EquivTransitive;
r,c=== r,c [X9] by EquivReflexive;
r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM;
e,d=== r,q by X5, EquivSymmetric;
r,p=== r,q by -, X10, EquivTransitive;
r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF;
Between (r,c,d') [X12] by X1, Bsymmetry_THM;
qed by -, X5, X11, X12, X2, X1, X3`;;
let EqDist2PointsBetween_THM = thm `;
let a b c p q be point;
assume ~(a = b) [H1];
assume Between (a,b,c) [H2];
assume a,p === a,q /\ b,p === b,q [H3];
thus c,p === c,q
:: a & b are equidistant from p & q. Apply SAS to a+pbc /\ a+qbc.
proof
a,b === a,b /\ b,c === b,c [X1] by EquivReflexive;
a,b,p cong a,b,q by -, H3, cong_DEF;
p,c === q,c by H1, -, H2, X1, A5;
qed by -, CongruenceDoubleSymmetry_THM`;;
let EqDist2PointsInnerBetween_THM = thm `;
let a x c p q be point;
assume Between (a,x,c) [H1];
assume a,p === a,q /\ c,p === c,q [H2];
thus x,p === x,q
:: a and c are equidistant from p and q. Apply Inner5Segments to
:: apb-x /\ aqb-x.
proof
a,c === a,c /\ c,x === c,x [X1] by EquivReflexive;
p,c === q,c by H2, CongruenceDoubleSymmetry_THM;
a,p,c cong a,q,c by -, H2, X1, cong_DEF;
p,x === q,x by -, H1, X1, Inner5Segments_THM;
thus x,p === x,q by -, CongruenceDoubleSymmetry_THM;
end`;;
let Gupta_THM = thm `;
let a b c d be point;
assume ~(a = b) [H1];
assume Between (a,b,c) [H2];
assume Between (a,b,d) [H3];
thus Between (b,d,c) \/ Between (b,c,d)
proof
cases;
suppose b = c \/ b = d \/ c = d;
Between (b,d,c) \/ Between (b,c,d) by -, Baaq_THM, Bqaa_THM;
qed by -;
suppose ~(b = c) /\ ~(b = d) /\ ~(c = d) [H4];
assume ~ (Between (b,d,c)) [H5];
consider d' such that
Between (a,c,d') /\ c,d' === c,d [X1] by A4;
consider c' such that
Between (a,d,c') /\ d,c' === c,d [X2] by A4;
is_ordered (a,b,c,d') by H2, X1, B123and134Ordered_THM;
Between (a,b,d') /\ Between (b,c,d') [X3] by -, is_ordered_DEF;
is_ordered (a,b,d,c') by H3, X2, B123and134Ordered_THM;
Between (a,b,c') /\ Between (b,d,c') [X4] by -, is_ordered_DEF;
~(c = d') [X5] by X1, H4, A3, EquivSymmetric;
~(d = c') [X6] by X2, H4, A3, EquivSymmetric;
~(b = d') [X7] by X3, H4, A6;
~(b = c') [X8] by X4, H4, A6;
:: In the proof below, we prove a stronger result than
:: BextendToLine_THM with much the same proof. We find u /\ b'
:: with essentially a,b,c,d',u and a b,d,c',b' ordered 5-tuples
:: with d'u === db /\ cb' === bc. *)
consider u such that
Between (c,d',u) /\ d',u === b,d [Y1] by A4;
is_ordered (b,c,d',u) by X5, X3, Y1, BTransitivityOrdered_THM;
Between (b,c,u) /\ Between (b,d',u) [Y2] by -, is_ordered_DEF;
consider b' such that
Between (d,c',b') /\ c',b' === b,c [Y3] by A4;
is_ordered (b,d,c',b') by X6, X4, Y3, BTransitivityOrdered_THM;
Between (b,d,b') /\ Between (b,c',b') [Y4] by -, is_ordered_DEF;
Between (c',d,b) [Y5] by X4, Bsymmetry_THM;
d,c' === c',d /\ b,d === d,b [Y6] by A1;
c,d === d,c' by X2, EquivSymmetric;
c,d' === d,c' by -, X1, EquivTransitive;
c,d' === c',d [Y7] by -, Y6, EquivTransitive;
d',u === d,b by Y1, Y6, EquivTransitive;
c,u === c',b [Y8] by -, Y1, Y5, Y7, SegmentAddition_THM;
c',b' === b',c' /\ b',b === b,b' [Y9] by A1;
b,c === c',b' by Y3, EquivSymmetric;
b,c === b',c' [Y10] by -, Y9, EquivTransitive;
Between (b',c',b) by Y4, Bsymmetry_THM;
b,u === b',b by -, Y2, Y10, Y8, SegmentAddition_THM;
b,u === b,b' [Y11] by -, Y9, EquivTransitive;
is_ordered (a,b,d',u) [Y12] by X7, X3, Y2, BTransitivityOrdered_THM;
is_ordered (a,b,c',b') by X8, X4, Y4, BTransitivityOrdered_THM;
Between (a,b,u) /\ Between (a,b,b') by -, Y12, is_ordered_DEF;
u = b' [Y13] by -, H1, Y11, C1_THM;
:: Show c'd' === cd by applying SAS to b+c'cd /\ b'+cc'd.
c',b === c,b' by Y13, Y8, EquivSymmetric;
b,c' === b',c [Z1] by -, CongruenceDoubleSymmetry_THM;
c,c' === c',c by A1;
b,c,c' cong b',c',c [Z2] by -, Y10, Z1, cong_DEF;
Between (b',c',d) by Y3, Bsymmetry_THM;
c',d' === c,d [Z3] by -, H4, Z2, X3, Y7, A5;
d',c' === c',d' by A1;
d',c' === c,d by -, Z3, EquivTransitive;
:: c,d',c',d is a "flat" rhombus. The diagonals bisect each other.
consider e such that
Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e
[Z4] by -, X3, X4, X1, X2, RhombusDiagBisect_THM;
~(e = c) [U1]
proof
cases;
suppose ~(e = c);
qed by -;
suppose e = c [U2];
c' = e by U2, Z4, EquivSymmetric, A3;
c' = c by -, U2;
Between (b,d,c) [U3] by -, X4;
F by -, U3, H5;
qed by -;
end;
e = d [V1]
proof
cases;
suppose e = d;
qed by -;
suppose ~(e = d) [V2];
consider p r q such that
Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\
r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e [W1]
by X3, Z4, X1, H4, V2, FlatNormal_THM;
r,p === r,q /\ c,p === c,q [W2] by W1, cong_DEF;
:: r and c are equidistant from p and q, r <> c, Between r,c,d', thus
also d'
~(c = r) by W1, U1, EquivSymmetric, A3;
d',p === d',q [W3] by -, W1, W2, EqDist2PointsBetween_THM;
:: c and d' are equidistant from p and q, c <> d',
:: Between c,d',b', thus also b'.
Between (c,d',b') by Y1, Y13;
b',p === b',q [W4] by -, X5, W2, W3, EqDist2PointsBetween_THM;
:: d' and c are equidistant from p and q, d' <> c, Between d',c,b, thus
also b.
Between (d',c,b) by X3, Bsymmetry_THM;
b,p === b,q [W5] by -, X5, W3, W2, EqDist2PointsBetween_THM;
:: b and b' are equidistant from p and q, Between b,c',b, thus also c'.
c',p === c',q [W7]by Y4, W4, W5, EqDist2PointsInnerBetween_THM;
:: c' and c are equidistant from p and q, c' <> c, Between c',c,p, thus
also p.
Between (c',e,c) by Z4, Bsymmetry_THM;
is_ordered (c',e,c,p) by -, U1, W1, BTransitivityOrdered_THM;
Between (c',c,p) [W8] by -, is_ordered_DEF;
~(c' = c) by Z4, U1, A6;
p,p === p,q by -, W8, W7, W2, EqDist2PointsBetween_THM;
:: Now we deduce a contradiction from p = q.
q = p by -, EquivSymmetric, A3;
p = r by -, W1, A6;
e = d [W9] by -, W1, EquivSymmetric, A3;
F by -, W9, V2;
qed by -;
end;
d' = e by V1, Z4, EquivSymmetric, A3;
d' = d by -, V1;
Between (b,c,d) by -, X3;
qed by -;
end`;;
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
