Hi Bill,
| John, thank you very much for writing the Tarski geometry miz3 code!
You're welcome, though I'm not quite satisfied with it for exactly the
reasons you mentioned:
| I don't mind quantifying over free variables. I prefer to. But these
| 6 lines in every theorem/proof hurt readability.
They do, although maybe in larger proofs later on the relative
uglification is less. I'm sure there is a nicer solution, possibly
using assumptions on the theorems instead of antecedents of
implications, though I would need to experiment a bit, and possibly
tweak miz3 or use a less obvious entry point to it.
Actually, I still incline towards the direct approach. If you start
with that, the day-to-day proofs will be much nicer, and it certainly
won't be difficult to generalize it afterwards. I'll even volunteer
to do it for you :-) In case you are tempted, the extract below is
how I would start. I now prove all the axioms (you'll need the latest
HOL Light svn version though to get a critical lemma) and then
launch into a direct port of your proof, and the result is pretty
clear and uncluttered.
| What if we go to the mile long theorem, so we'd only state these 6
| lines once. Or can me make some, uh, global declaration?
That's possible, but you'd need to do all the proofs together as a
single Mizar block, I think. It's still not a completely satisfying
solution, as far as I can see, and I'm sure we can do better.
| Thanks, that's nice, and I should read your book. But of course using
| such a simple self-coded basic proof checker defeats my selling point
| of propelling my students into the new hot world of proof assistants.
Yes, that's true.
John.
(* ========================================================================= *)
(* Model for Tarski axioms and port of Bill Richter's geometry proofs. *)
(* ========================================================================= *)
needs "Multivariate/convex.ml";;
(* ------------------------------------------------------------------------- *)
(* Define a new type "point" in bijection with real^2. *)
(* ------------------------------------------------------------------------- *)
let Plane_TYBIJ =
let th = prove(`?x:real^2. T`,REWRITE_TAC[]) in
let def = new_type_definition "point" ("planify","coords") th in
REWRITE_RULE[] def;;
(* ------------------------------------------------------------------------- *)
(* Define notions of congruence and between-ness as Euclidean equivalents. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("===",(12, "right"));;
let Congruent_DEF = new_definition
`a,b === c,d <=> dist(coords a,coords b) = dist(coords c,coords d)`;;
let Between_DEF = new_definition
`Between (a,b,c) <=> between (coords b) (coords a,coords c)`;;
(* ------------------------------------------------------------------------- *)
(* The derived notion of triangle congruence. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("cong",(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`;;
(* ------------------------------------------------------------------------- *)
(* Simple tactic to switch variables from "point" to "real^2". *)
(* ------------------------------------------------------------------------- *)
let PLANE_COORD_TAC =
let PLANE_QUANT_THM = MESON[Plane_TYBIJ]
`((!x. P x) <=> (!x. P(planify x))) /\
((?x. P x) <=> (?x. P(planify x)))`
and PLANE_EQ_THM = MESON[Plane_TYBIJ] `planify x = planify y <=> x = y` in
REWRITE_TAC[PLANE_QUANT_THM; Congruent_DEF; Between_DEF; PLANE_EQ_THM;
Plane_TYBIJ];;
(* ------------------------------------------------------------------------- *)
(* Derivation of the axioms. *)
(* ------------------------------------------------------------------------- *)
let A1 = prove
(`!a b. a,b === b,a`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let A2 = prove
(`!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let A3 = prove
(`!a b c. a,b === c,c ==> a = b`,
PLANE_COORD_TAC THEN NORM_ARITH_TAC);;
let A4 = prove
(`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`,
PLANE_COORD_TAC THEN GEOM_ORIGIN_TAC `a:real^2` THEN REPEAT GEN_TAC THEN
REWRITE_TAC[DIST_0] THEN ASM_CASES_TAC `q:real^2 = vec 0` THENL
[ASM_SIMP_TAC[BETWEEN_REFL; VECTOR_CHOOSE_SIZE; DIST_POS_LE];
EXISTS_TAC `--(dist(b:real^2,c) / norm(q) % q):real^2` THEN
REWRITE_TAC[between; DIST_0] THEN
REWRITE_TAC[dist; NORM_MUL; NORM_NEG; REAL_ABS_DIV; REAL_ABS_NORM;
VECTOR_ARITH `q - --(a % q) = (&1 + a) % q`] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(REAL_RING `a = &1 + b ==> a * q = q + b * q`) THEN
SIMP_TAC[REAL_ABS_REFL; REAL_POS; REAL_LE_ADD; REAL_LE_DIV; NORM_POS_LE];
ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0]]]);;
let A5 = prove
(`!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 lemma = prove
(`!a b x:real^N.
between b (a,x) /\ ~(b = a) ==> ?d. &0 <= d /\ x = b + d % (b - a)`,
REPEAT GEN_TAC THEN REWRITE_TAC[BETWEEN_NORM] THEN STRIP_TAC THEN
EXISTS_TAC `norm(x - b:real^N) / norm(b - a)` THEN
SIMP_TAC[REAL_LE_DIV; NORM_POS_LE] THEN FIRST_X_ASSUM
(MP_TAC o AP_TERM `(%) (inv(norm(b - a:real^N))):real^N->real^N`) THEN
ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; NORM_EQ_0; VECTOR_SUB_EQ] THEN
VECTOR_ARITH_TAC) in
REWRITE_TAC[cong_DEF] THEN PLANE_COORD_TAC THEN REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`;
`a':real^2`; `b':real^2`; `c':real^2`]
RIGID_TRANSFORMATION_BETWEEN_3) THEN
ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0; DIST_SYM]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `k:real^2`
(X_CHOOSE_THEN `f:real^2->real^2` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC))) THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST_ALL_TAC) THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `x:real^2`] lemma) THEN
MP_TAC(ISPECL [`k + (f:real^2->real^2) a`;
`k + (f:real^2->real^2) b`; `x':real^2`] lemma) THEN
ASM_REWRITE_TAC[VECTOR_ARITH `k + a:real^N = k + b <=> a = b`;
VECTOR_ARITH `(k + a) - (k + b):real^N = a - b`] THEN
ANTS_TAC THENL
[ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_INJECTIVE]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d':real` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
UNDISCH_TAC `dist(b:real^2,x) = dist (k + f b:real^2,x')` THEN
ASM_REWRITE_TAC[GSYM VECTOR_ADD_ASSOC;
NORM_ARITH `dist(a + b:real^N,a + c) = dist(b,c)`] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP ORTHOGONAL_TRANSFORMATION_LINEAR) THEN
ASM_SIMP_TAC[GSYM LINEAR_SUB; GSYM LINEAR_CMUL; GSYM LINEAR_ADD] THEN
RULE_ASSUM_TAC(REWRITE_RULE[ORTHOGONAL_TRANSFORMATION_ISOMETRY]) THEN
ASM_REWRITE_TAC[NORM_ARITH `dist(a:real^N,a + c) = norm c`] THEN
ASM_REWRITE_TAC[NORM_MUL; REAL_EQ_MUL_RCANCEL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
ASM_SIMP_TAC[real_abs]);;
let A6 = prove
(`!a b. Between(a,b,a) ==> a = b`,
PLANE_COORD_TAC THEN SIMP_TAC[between] THEN NORM_ARITH_TAC);;
let A7 = prove
(`!a b p q z.
Between(a,p,z) /\ Between(b,q,z) ==>
?x. Between(p,x,b) /\ Between(q,x,a)`,
PLANE_COORD_TAC THEN REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `z:real^2` THEN
REPEAT GEN_TAC THEN REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SEGMENT_SYM] THEN
GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV o RAND_CONV o RAND_CONV)
[SEGMENT_SYM] THEN
REWRITE_TAC[IN_SEGMENT] THEN
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `p:real` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `q:real` STRIP_ASSUME_TAC)) THEN
REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
REWRITE_TAC[MESON[]
`(?x. (?u. &0 <= u /\ u <= &1 /\ x = f u) /\
(?u. &0 <= u /\ u <= &1 /\ x = g u)) <=>
?u v. (&0 <= u /\ &0 <= v) /\ (u <= &1 /\ v <= &1) /\ f u = g v`] THEN
SUBGOAL_THEN `p * q <= &1` MP_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[];
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th)] THEN
REWRITE_TAC[REAL_ARITH `p * q <= &1 <=> p * q = &1 \/ p * q < &1`] THEN
STRIP_TAC THENL
[FIRST_ASSUM(SUBST_ALL_TAC o SYM o MATCH_MP REAL_MUL_LINV_UNIQ) THEN
SUBGOAL_THEN `q = &1` SUBST_ALL_TAC THENL
[ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
UNDISCH_TAC `inv q <= &1` THEN
REWRITE_TAC[GSYM REAL_NOT_LT; CONTRAPOS_THM] THEN
DISCH_TAC THEN MATCH_MP_TAC REAL_LT_RINV THEN
ASM_CASES_TAC `q = &0` THENL
[UNDISCH_TAC `inv q * q = &1` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
ASM_REAL_ARITH_TAC;
REPEAT(EXISTS_TAC `&1 / &2`) THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
VECTOR_ARITH_TAC];
EXISTS_TAC `q * (&1 - p) / (&1 - p * q)` THEN
EXISTS_TAC `(&1 - p) / (&1 - p * q)` THEN CONJ_TAC THENL
[CONJ_TAC THENL
[MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC REAL_LE_DIV THEN ASM_REWRITE_TAC[REAL_SUB_LE];
ALL_TAC] THEN
CONJ_TAC THENL
[CONJ_TAC THENL
[GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC REAL_LE_DIV THEN ASM_REWRITE_TAC[REAL_SUB_LE]; ALL_TAC];
ALL_TAC] THEN
ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_SUB_LT] THEN
REWRITE_TAC[REAL_ARITH `&1 - p <= &1 * (&1 - p * q) <=>
p * q <= p * &1`] THEN
MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
UNDISCH_TAC `p * q < &1` THEN CONV_TAC REAL_FIELD]]);;
(* ------------------------------------------------------------------------- *)
(* Now miz3 versions of the actual proofs. *)
(* ------------------------------------------------------------------------- *)
loadt "miz3/make.ml";;
let EquivReflexive = thm `;
!a b. a,b === a,b
proof
let a b be point;
b,a === a,b by A1;
thus a,b === a,b by A2;
end`;;
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;
thus c,d === a,b by 1, A2;
end`;;
let EquivTransitive = thm `;
!a b p q r s : point. 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 [1];
assume p,q === r,s [2];
p,q === a,b by 1, EquivSymmetric;
thus a,b === r,s by 2, A2;
end`;;
let Baaa_THM = thm `;
!a b. Between (a,a,a) /\ a,a === b,b
proof
let a b be point;
?x. Between (a,a,x) /\ a,x === b,b by A4;
consider x such that Between (a,a,x) /\ a,x === b,b [1];
a = x by 1, A3;
thus Between (a,a,a) /\ a,a === b,b by 1;
end`;;
let Bqaa_THM = thm `;
!a q. Between(q,a,a)
proof
let a q be point;
? x : point . Between(q,a,x) /\ a,x === a,a by A4;
consider x such that Between(q,a,x) /\ a,x === a,a [1];
a = x by 1, A3;
thus Between(q,a,a) by 1;
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
