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



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