Re: [isabelle] Interpreting feedback from Isabelle/HOL



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.


On 7/24/19 7:22 PM, Eugene W. Stark wrote:
> 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:
> 
>>       thus ?thesis by simp
>>       (* It feels as if the theorem should be proved by now *)
>>   qed
>> end
> 
> 
> On 7/24/19 5:18 PM, John F. Hughes wrote:
>> 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.