Freek, thanks for responding! You set me straight on my two points:
`?' means 0 or more, so <by refs> can be nothing.
A proof need have no steps, as in your example:
let FOO = thm `;
T proof end;`;;
Quick question: Doesn't `?' mean the same as `*'?
Two more questions, but first a manifesto:
I'd like you to help me with an miz3 documentation project. I'll do
as much of the work as necessary, but I think I need your help to get
started. And you may prefer to do the job yourself.
I wrote 1000 lines of Tarski axiomatic geometry miz3 proofs (below),
porting 1500 lines of Mizar code. I did it partly for the joy of it,
and to check my proofs were correct, but mostly I did it to cite in a
geometry paper I want to submit soon, probably to the Amer Math
Monthly, which has published a number of Hilbert axiom papers.
There are two holdups right now:
1) HOL Light must be easy to download & run. Right now I can't get
the latest version of ocaml to run, as it requires camlp5. I can
install both ocaml & camlp5, but then I can't make HOL Light. I sent
a bug report, and John will probably straighten this out. I assume
he's working hard at Intel at his real job, proving theorems about
floating point algorithms, and that's fine, I can wait.
2) There must be adequate documentation for how to use miz3 to concoct
the sort of 2-column proofs I did in my Tarski code. At least the dox
must be good enough for me, and all I need is the miz3 syntax and
semantics. Your paper arxiv.org/pdf/1201.3601 is not adequate dox,
but as John agreed, it wasn't intended to be, but instead to promote
your bold fusion of declarative and procedural proofs.
John just wrote:
I hope you manage to produce something. Curiously enough, Freek
wrote a lot of documentation to explicate Trybulec's Mizar, so
maybe you will end up doing the same for Freek's miz3.
http://cs.ru.nl/~freek/mizar/index.html
What I want (precise syntax & semantics) looks a lot different from
your Mizar dox. When I was learning Mizar, I relied heavily on your
work, although I didn't read it all. I didn't learn the precise
syntax & semantics of Mizar, so all the Mizar I did was trial and
error. I bet you can write the precise syntax & semantics easily,
though, and I'll help as much as I can or you want.
Putting aside manifestos, here are two questions I posted earlier:
3) My code, following your p 13--14 drinkers principle, violates your
grammar (this saved me 100s of lines, so thanks!). You wrote
Yes, the miz3 syntax is a bit more liberal than is presented in the
paper. (I think the "growing" stuff won't work then, though.)
Can we write down the actual syntax (grammar) of miz3? I don't know
what "growing" stuff means.
Basically, instead of `; formal proof ... end;`, you can
also use `; now ... end;`. And the "now/end" brackets are
optional, if the thing is not just a single statement with
proof/justification, they are added automatically.
Let me try to understand this. On p 15--18, you write
The now syntax can be used when the statement that is being proved
can be inferred from the skeleton steps in the proof (which is
generally the case). In that situation
phi proof ... end;
can be abbreviated as
now ... end;
That's interesting, and it sounds like it saves a line, as we don't
need the keyword `proof', and `now' won't go on its own line. But
what you wrote today says we indicates we can skip the "now/end"
brackets, which saves one more line. I didn't get that to work.
Evaluate my code below, and then paste in this lemma again:
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`;;
it works fine. But it seems you're saying I don't need the last
end. Since qed means thus thesis; end, this ought to work:
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;
thus thesis by -, A3`;;
But it doesn't work, and I get the error
::#9
:: 9: syntax error mizar
Probably I misunderstood what you wrote.
4) I think I have a semantics question: I have 38 lemmas in my miz3
code below. All of the proofs end in `qed' except for the 8 which end
in `cases' constructions, and they all end in `end'. Why?
--
Best,
Bill
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.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);;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("on_line",(12, "right"));;
parse_as_infix("equal_line",(12, "right"));;
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 Line_DEF = new_definition
`x on_line a,b <=>
~(a = b) /\ (Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b))`;;
let LineEq_DEF = new_definition
`a,b equal_line x,y <=>
~(a = b) /\ ~(x = y) /\ ! c . c on_line a,b <=> c on_line x,y`;;
(* ------------------------------------------------------------------------- *)
(* 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 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;
qed by -, H1, H2, is_ordered_DEF`;;
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;
qed by -, CongruenceDoubleSymmetry_THM`;;
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`;;
(* Using Gupta's theorem, we prove Hilbert's axiom I3; a line is
determined by two points. *)
let I1part1_THM = thm `;
let a b x be point;
assume ~(a = b) [H1];
assume ~(a = x) [H2];
assume x on_line a,b [H3];
thus ! c .
c on_line a,b ==> c on_line a,x
proof
let c be point;
assume c on_line a,b [H4];
Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) [X1]
by H3, Line_DEF;
Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) [X2]
by H4, Line_DEF;
x = b \/ b = c \/ (~(x = b) /\ ~(b = c));
cases by -;
suppose x = b [Case1];
qed by -, H4;
suppose b = c [Case3];
Between (a,c,x) \/ Between (a,x,c) \/ Between (x,a,c) by -, X1;
Between (a,c,x) \/ Between (a,x,c) \/ Between (c,a,x) by -, Bsymmetry_THM;
qed by -, H2, Line_DEF;
suppose ~(x = b) /\ ~(b = c) [Case2];
Between (a,x,c) \/ Between (a,c,x) \/ Between (x,a,c) [P]
proof
cases by X1;
suppose Between (a,b,x) [Y1];
cases by X2;
suppose Between (a,b,c) [Y11];
Between (b,x,c) \/ Between (b,c,x) by -, Y1, H1, Gupta_THM;
is_ordered (a,b,x,c) \/ is_ordered (a,b,c,x) by
Case2, Y1, Y11, -, BTransitivityOrdered_THM;
Between (a,x,c) \/ Between (a,c,x) by -, is_ordered_DEF;
qed by -;
suppose Between (a,c,b);
is_ordered (a,c,b,x) by -, Y1, B123and134Ordered_THM;
qed by -, is_ordered_DEF;
suppose Between (c,a,b);
is_ordered (c,a,b,x) by H1, -, Y1, BTransitivityOrdered_THM;
Between (c,a,x) by -, is_ordered_DEF;
qed by -, Bsymmetry_THM;
end;
suppose Between (a,x,b) [Y2];
cases by X2;
suppose Between (a,b,c);
is_ordered (a,x,b,c) by -, Y2, B123and134Ordered_THM;
qed by -, is_ordered_DEF;
suppose Between (a,c,b) [Y22];
consider m such that
Between (b,a,m) /\ a,m === a,b [X5] by -, A4;
~(a = m) [X6] by H1, X5, EquivSymmetric, A3;
Between (m,a,b) by X5, Bsymmetry_THM; :: m,a,c,b & m,a,x,b
Between (m,a,c) /\ Between (m,a,x) by -, Y22, Y2, B124and234then123_THM;
Between (a,c,x) \/ Between (a,x,c) by -, X6, Gupta_THM;
qed by -;
suppose Between (c,a,b);
Between (c,a,x) by -, Y2, B124and234then123_THM; :: c,a,x,b
qed by -, Bsymmetry_THM;
end;
suppose Between (x,a,b) [Y3];
cases by X2;
suppose Between (a,b,c);
is_ordered (x,a,b,c) by H1, -, Y3, BTransitivityOrdered_THM;
qed by -, is_ordered_DEF;
suppose Between (a,c,b);
qed by Y3, -, B124and234then123_THM; :: x,a,c,b
suppose Between (c,a,b);
Between (b,a,x) /\ Between (b,a,c) by Y3, -, Bsymmetry_THM;
Between (a,x,c) \/ Between (a,c,x) by -, H1, Gupta_THM;
qed by -;
end;
end;
Between (a,x,c) \/ Between (a,c,x) \/ Between (c,a,x) by P, Bsymmetry_THM;
c on_line a,x by -, H2, Line_DEF;
qed by -;
end`;;
let I1part2_THM = thm `;
let a b x be point;
assume ~(a = b) [H1];
assume ~(a = x) [H2];
assume x on_line a,b [H3];
thus a,b equal_line a,x
proof
! c . c on_line a,b <=> c on_line a,x [P]
proof
let c be point;
c on_line a,b ==> c on_line a,x [Imp1]
proof
assume c on_line a,b;
c on_line a,x by -, H1, H2, H3, I1part1_THM;
qed by -;
c on_line a,x ==> c on_line a,b [Imp2]
proof
assume c on_line a,x [H4];
Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF;
Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM;
b on_line a,x by -, H2, Line_DEF;
c on_line a,b by -, H1, H2, H4, I1part1_THM;
qed by -;
qed by Imp1, Imp2;
qed by H1, H2, P, LineEq_DEF`;;
let I1part2_THM = thm `;
let a b x be point;
assume ~(a = b) [H1];
assume ~(a = x) [H2];
assume x on_line a,b [H3];
thus a,b equal_line a,x
proof
Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF;
Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM;
b on_line a,x [Z1] by -, H2, Line_DEF;
! c . c on_line a,b ==> c on_line a,x [Z2] by H1, H2, H3, I1part1_THM;
! c . c on_line a,x ==> c on_line a,b [Z3] by H1, H2, Z1, I1part1_THM;
! c . c on_line a,x <=> c on_line a,b by Z2, Z3;
qed by H1, H2, -, LineEq_DEF`;;
let LineEqRefl_THM = thm `;
let a b be point;
assume ~(a = b) [H1];
thus a,b equal_line a,b
proof
! c . c on_line a,b <=> c on_line a,b;
a,b equal_line a,b by -, H1, LineEq_DEF;
qed by -`;;
let LineEqA1_THM = thm `;
let a b be point;
assume ~(a = b) [H1];
thus a,b equal_line b,a
proof
! c . c on_line a,b <=> c on_line b,a [P]
proof
let c be point;
c on_line a,b ==> c on_line b,a [Imp1]
proof
assume c on_line a,b;
Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) by -, Line_DEF;
Between (c,b,a) \/ Between (b,c,a) \/ Between (b,a,c) by -, Bsymmetry_THM;
qed by -, H1, Line_DEF;
c on_line b,a ==> c on_line a,b [Imp2]
proof
assume c on_line b,a [H3];
Between (b,a,c) \/ Between (b,c,a) \/ Between (c,b,a) by -, Line_DEF;
Between (c,a,b) \/ Between (a,c,b) \/ Between (a,b,c) by -, Bsymmetry_THM;
qed by -, H1, Line_DEF;
qed by Imp1, Imp2;
qed by H1, P, LineEq_DEF`;;
let LineEqSymmetric_THM = thm `;
let a b c d be point;
assume ~(a = b) /\ ~(c = d) [H1];
assume a,b equal_line c,d [H2];
thus c,d equal_line a,b
proof
! x . x on_line a,b <=> x on_line c,d by H2, LineEq_DEF;
! x . x on_line c,d <=> x on_line a,b by -;
c,d equal_line a,b by -, H1, LineEq_DEF;
qed by -`;;
let LineEqTrans_THM = thm `;
let a b c d e f be point;
assume ~(a = b) /\ ~(c = d) /\ ~(e = f) [H1];
assume a,b equal_line c,d [H2];
assume c,d equal_line e,f [H3];
thus a,b equal_line e,f
proof
(! y . y on_line a,b <=> y on_line c,d) /\
(! y . y on_line c,d <=> y on_line e,f) [X2] by H2, H3, LineEq_DEF;
(! y . y on_line a,b <=> y on_line e,f) by -;
qed by -, H1, LineEq_DEF`;;
let onlineEq_THM = thm `;
let a b c d x be point;
assume ~(a = b) /\ ~(c = d) [H1];
assume x on_line a,b [H2];
assume a,b equal_line c,d [H3];
thus x on_line c,d
proof
! y . y on_line a,b <=> y on_line c,d by -, LineEq_DEF;
qed by -, H2`;;
let I1part2Reverse_THM = thm `;
let a b y be point;
assume ~(a = b) /\ ~(b = y) [H1];
assume y on_line a,b [H3];
thus a,b equal_line y,b
proof
a,b equal_line b,a /\ b,y equal_line y,b [Y1] by H1, LineEqA1_THM;
y on_line b,a by H3, Y1, onlineEq_THM;
b,a equal_line b,y by -, H1, Y1, I1part2_THM;
a,b equal_line b,y by -, H1, Y1, LineEqTrans_THM;
a,b equal_line y,b by -, H1, Y1, LineEqTrans_THM;
qed by -`;;
let I1_THM = thm `;
let a b x y be point;
assume ~(a = b) [H1];
assume ~(x = y) [H2];
assume a on_line x,y [H3];
assume b on_line x,y [H4];
thus x,y equal_line a,b
proof
cases;
suppose (x = b) [H5];
~(b = y) [P1] by -, H2;
b,a equal_line a,b [P2] by H1, LineEqA1_THM;
x,y equal_line b,y [P3] by H2, H5, LineEqRefl_THM;
a on_line b,y by H3, H5;
b,y equal_line b,a by -, P1, H1, I1part2_THM;
x,y equal_line b,a by -, H1, H2, P1, P3, LineEqTrans_THM;
qed by -, H1, H2, P2, LineEqTrans_THM;
suppose
~(x = b) [H6];
x,y equal_line x,b [P4] by -, H2, H6, H4, I1part2_THM;
a on_line x,b by -, H2, H6, H3, onlineEq_THM;
x,b equal_line a,b by -, H6, H1, I1part2Reverse_THM;
qed by H1, H2, H6, P4, -, LineEqTrans_THM;
end`;;
|