# [isabelle] Interpreting feedback from Isabelle/HOL

```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):
1. ∃P Q R S.
P ≠ Q ∧
P ≠ R ∧
Q ≠ R ∧
P ≠ S ∧
Q ≠ S ∧ R ≠ S

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"

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,

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,
*)
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)"
have "meets Q PQ ∧ meets Q 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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.