*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Interpreting feedback from Isabelle/HOL*From*: "John F. Hughes" <jfh at cs.brown.edu>*Date*: Wed, 24 Jul 2019 17:18:09 -0400

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" 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

**Follow-Ups**:**Re: [isabelle] Interpreting feedback from Isabelle/HOL***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term
- Next by Date: Re: [isabelle] Interpreting feedback from Isabelle/HOL
- Previous by Thread: [isabelle] UNSW postdoc position for Verified Time Protection
- Next by Thread: Re: [isabelle] Interpreting feedback from Isabelle/HOL
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list