Email Gateway (Aug 22 2022 at 20:20): Email Gateway (Aug 22 2022 at 20:20):From: "John F. Hughes" <jfh@cs.brown.edu>
I'm trying to prove a small result in synthetic projective geometry,
namely, that a projective plane contains at least four points. I've worked
my way through many stages of the proof, and arrived at a state where the
"State" panel in Isabelle shows this:
proof (state)
this:
∃P Q R S.
P ≠ Q ∧
P ≠ R ∧
Q ≠ R ∧
P ≠ S ∧ Q ≠ S ∧ R ≠ S
goal (1 subgoal):
Aside from the numbering ("1.") and a line break, these appear to me to be
identical, so I would have expected to be able to say something like "hence
?thesis by ...", where the ellipsis would be filled in with, well, some
proof method. In my mind, I'm thinking the proof method should be "any fool
can see this!", but I don't think that's one of the available ones. "try0"
suggests "by blast", so I add "by blast", and everything seems OK, but
after that line, the proof state looks exactly the same as before, and
typing "qed" tells me that I failed to finish the proof (with one subgoal
remaining).
I have no doubt that I'm doing something wrong, but what I'm wondering is
how am I supposed to interpret the feedback I'm getting., I've got a state
that looks promising; the proof assistant suggests a step...and I end up at
exactly the same state. At this point "assistant" is looking like a bit of
a misnomer to me, although I'll doubtless learn otherwise.
For those who want to see the whole story, in case that's useful in
answering my question, here it is:
theory Question6
imports Main
begin
locale affine_plane_data =
fixes meets :: "'point ⇒ 'line ⇒ bool"
begin
definition parallel:: "'line ⇒ 'line ⇒ bool" (infix "||" 50)
where "l || m ⟷ (l = m ∨ ¬ (∃ P. meets P l ∧ meets P m))"
definition collinear :: "'point ⇒ 'point ⇒ 'point ⇒ bool"
where "collinear A B C ⟷ (∃ l. meets A l ∧ meets B l ∧ meets C l)"
end
locale affine_plane =
affine_plane_data meets
for meets :: "'point ⇒ 'line ⇒ bool" +
assumes
a1: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l" and
a2: "¬ meets P l ⟹ ∃!m. l || m ∧ meets P m" and
a3: "∃P Q R. P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R"
begin
(* Every point lies on some line *)
lemma containing_line: " ∀S. ∃l. meets S l"
using a2 by blast
(* Every line contains at least one point *)
lemma contained_point: "∀l. ∃S. meets S l"
using a1 a2 a3 parallel_def collinear_def by metis
lemma symmetric_parallel: "l || m ⟹ m || l"
using parallel_def by auto
lemma reflexive_parallel: "l || l"
by (simp add: parallel_def)
lemma transitive_parallel: "⟦l || m ; m || n⟧ ⟹ l || n"
by (metis a2 parallel_def)
(* Two lines meet in at most one point *)
lemma (in affine_plane) prop1H2: "⟦l ≠ m; meets P l; meets P m; meets Q
l; meets Q m⟧ ⟹ P = Q"
using a1 by auto
(* We now try to prove that every affine plane contains at least four
points. Sledgehammer
doesn't get anywhere with this one. Here's a proof, though:
i. by A3 there are three distinct non-collinear points; call them P,Q,R.
ii. By A1, there's a line, which I'll call QR, through Q and R.
iii. By A2, there's a line l through P, parallel to QR.
iv. Similarly, there's a line PQ containing P and Q.
v. There's a line m through R, parallel to the line PQ.
CASES: l is parallel to m, or it is not.
vi. l is not parallel to m, for if it were, then PQ || m || l || QR, hence
PQ || QR (by
the lemmas about |⦈ and since both contain Q, they are identical, but then
P,Q,R are collinear,
which is a contradiction.
vii. So l and m are nonparallel, and they share some point S.
viii. S lies on m, which is parallel to PQ but not equal to it,
hence disjoint from it (see definition of parallel), so S is not on PQ.
ix. Hence S != P, S != Q.
x. Similar (arguing about l), we get S != R.
xi. Hence the four points P,Q,R,S are all distinct, and we are done.
The proof below attempts to mimic this structure.
*)
proposition four_points: "∃(P :: 'point) (Q :: 'point) (R :: 'point) (S
:: 'point). P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S"
proof -
obtain P Q R where PQR: "P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R"
using a3 by auto
(* ii. By A1, there's a line, which I'll call QR, through Q and R. *)
obtain QR where QR: "meets Q QR ∧ meets R QR"
using PQR a1 by blast
(* iii. By A2, there's a line l through P, parallel to QR. *)
obtain l where l: "meets P l ∧ l || QR"
using a2 parallel_def by metis
(* iv. Similarly to ii, there's a line PQ containing P and Q. *)
obtain PQ where PQ: "meets P PQ ∧ meets Q PQ"
using PQR a1 by blast
(* v. and similar to iii, here's a line m through R, parallel to the
line PQ. *)
obtain m where m: "meets R m ∧ m || PQ"
using a2 parallel_def by metis
(* CASES: l is parallel to m, or it is not. *)
(*
vi. l is not parallel to m, for if it were, then PQ || m || l ||
QR, hence PQ || QR (by
the lemmas about |⦈ and since both contain Q, they are identical,
but then P,Q,R are collinear,
which is a contradiction.
*)
have "¬ (l || m)"
proof
assume 1: "l || m"
hence "m || l"
using 1 symmetric_parallel by simp
moreover have "PQ || m ∧ l || QR"
using m l symmetric_parallel by blast
ultimately have "PQ || QR"
using transitive_parallel by blast
hence "PQ = QR ∨ ¬ (∃ H. meets H PQ ∧ meets H QR)"
by (simp add: parallel_def)
have "meets Q PQ ∧ meets Q QR"
by (simp add: PQ QR)
hence "PQ = QR"
using ‹PQ = QR ∨ (∄H. meets H PQ ∧ meets H QR)› by blast
hence c1: "collinear P Q R"
using PQ QR collinear_def by blast
moreover have c2: "¬ (collinear P Q R)"
using PQR by blast
thus False
using PQR calculation by blast
qed
obtain S where S: "meets S l ∧ meets S m"
using ‹¬ l || m› parallel_def by blast
have "¬ meets S PQ"
using PQ PQR S affine_plane_data.collinear_def m parallel_def by
fastforce
hence "S ≠ P ∧ S ≠ Q"
using PQ by blast
have "¬ meets S QR"
by (metis PQR QR S collinear_def parallel_def l)
hence "S ≠ R"
using QR by auto
hence "P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S"
using PQR ‹S ≠ P ∧ S ≠ Q› by blast
hence "∃(P :: 'point) (Q :: 'point) (R :: 'point) (S :: 'point). P ≠
Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S"
by auto
hence ?thesis by simp
(* It feels as if the theorem should be proved by now *)
qed
qed
Email Gateway (Aug 22 2022 at 20:20):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
You need to use "thus" (or "then show") if you want the subgoal to be discharged.
"Hence" asserts a fact, but does not discharge any subgoal.
Lines 152-155 of your Question6.thy should be:
Email Gateway (Aug 22 2022 at 20:20):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
You can still get some mileage from sledgehammer, once you got off on the right start:
(* CASES: l is parallel to m, or it is not. *)
(*
vi. l is not parallel to m, for if it were, then PQ || m || l ||
QR, hence PQ || QR (by
the lemmas about |⦈ and since both contain Q, they are identical,
but then P,Q,R are collinear,
which is a contradiction.
*)
have "¬ (l || m)"
by (metis PQ PQR QR a2 affine_plane_data.parallel_def collinear_def l m)
obtain S where S: "meets S l ∧ meets S m"
using ‹¬ l || m› parallel_def by blast
have "¬ meets S PQ"
using PQ PQR S affine_plane_data.collinear_def m parallel_def by fastforce
thus ?thesis
by (metis PQ PQR QR S affine_plane_data.collinear_def affine_plane_data.parallel_def l)
qed
end
Using "try" found one of the proofs by "metis" directly.
For the other, an "smt" proof was reported, supposedly timing out, but pasting
in the suggested proof worked OK and changing "smt" to "metis" also worked OK,
though slightly slower. If you don't want proofs by "smt" (the AFP doesn't allow them,
and they tend to be more fragile in my experience), then it is frequently a cheap win
to change "smt" to "metis", "metis (no_types)" or "metis (no_types, lifting)".
Of course your original version was more useful to the human reader, but depending
on how interesting the particular fact and its proof was, you might well deem it more
important and maintainable to have a shorter proof text.
Last updated: Nov 21 2024 at 12:39 UTC