Re: [isabelle] Proof by contradiction



Hi John,

> On 28. Mar 2019, at 14:39, John F. Hughes <jfh at cs.brown.edu> wrote:
> 
> I'm struggling with trying to encode a proof by contradiction in Isar.
> 
> In the euclidean plane, I'm trying to prove that if two vertical lines l
> and k lie at different x-coordinates, then they have no points in common.
> In a math book, I'd write:
> 
> Suppose (u,v) is on both x = a and x = b, and a \ne b; then u = a and u =
> b, so a = b. Contradiction.
> 
> With Isabelle in the back of my mind, perhaps I'd write this:
> 
> Proof: Because l is vertical, it's defined by an equation  x = a ;
> similarly k is defined by x = b, and we're given that a \ne b.
> Suppose T = (u,v) lies on both. Then u = a because T is on l, and u = b
> because T is on k, and thus a = b. That's a contradiction with the given
> fact a \ne b. Hence T cannot lie on both lines. QED.
> 
> I've attempted to mimic this proof in Isar below, and it's fairly readable,
> I hope. "a2meets P m" is my way of saying "the point P is on the line m",
> and it's written this way to make it consistent with other stuff I'm
> writing about general affine geometries.
> 
> Although the resulting proof is wordy,  I feel as if I'm headed in the
> right direction. But I cannot figure out the syntax for saying "OK, I've
> proved False. Surely we can conclude the theorem by contradiction!":
> 
> theory Brief6
> imports Complex_Main
> begin  datatype a2pt = A2Point "real" "real"
> 
>  datatype a2ln = A2Ordinary "real" "real"
>                | A2Vertical "real"
>  text "Ordinary m b represents the line y = mx+b; Vertical xo is the line
> x = xo "
> 
>  fun a2meets :: "a2pt ⇒ a2ln ⇒ bool" where
>    "a2meets (A2Point x y) (A2Ordinary m b) = (y = m*x + b)" |
>    "a2meets (A2Point x y) (A2Vertical xi) = (x = xi)"
> 
> (* Lemma: vertical lines with different x-coords are disjoint *)
> lemma A2_vert: "x0 ≠ x1 ∧ l = A2Vertical x0 ∧ k = A2Vertical x1   ⟹  ¬ (∃
> T. a2meets T l  ∧ a2meets T k)"
> proof -
>  assume diff_x: "x0 ≠ x1"
>  assume l_form: "l = A2Vertical x0"
>  assume k_form: "k = A2Vertical x1"
>  have "¬ (∃ T. a2meets T l  ∧ a2meets T k)"
>  proof (rule ccontr)
>    assume "∃ T. a2meets T l  ∧ a2meets T k"
>    fix u v
>    assume T_form: "T = A2Point u v"
>    have T_on_l: "a2meets T l"
>      by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2)
> a2meets.simps(2) diff_x k_form l_form)
>    have T_on_k: "a2meets T k"
>      by (metis ‹∃T. a2meets T l ∧ a2meets T k› a2meets.elims(2)
> a2meets.simps(2) diff_x k_form l_form)
>    have "u = x0"
>      using T_form T_on_l l_form by auto
>    have "u = x1"
>      using T_form T_on_k k_form by auto
>    have False
>      using ‹u = x0› ‹u = x1› diff_x by blast
>  qed
> =======
> 
> I'd appreciate it if (a) someone could add whatever last line or two is
> needed to finish this proof,

There are several things which don't work in your proof:
  * First, T (from "T = A2Point u v") is not bound. Isabelle/jEdit is showing that with the different background. You want something along:
    obtain T where
      ‹…›

  * Similarly, you have to use obtain for u and v, not fix.

  * Then the last step has to be "show False" instead of "have False". Then you will get an error ("Failed to refine any pending goal"), because "rule ccontr is only negating once more ‹¬ (∃ T. a2meets T l  ∧ a2meets T k)›. You can fix that by removing "rule ccontr" and rely on the default rule to do the right thing.


This brings us to this proof:

lemma A2_vert: "x0 ≠ x1 ∧ l = A2Vertical x0 ∧ k = A2Vertical x1   ⟹  ¬ (∃
T. a2meets T l  ∧ a2meets T k)"
proof -
 assume diff_x: "x0 ≠ x1"
 assume l_form: "l = A2Vertical x0"
 assume k_form: "k = A2Vertical x1"
 have "¬ (∃ T. a2meets T l  ∧ a2meets T k)"
 proof
   assume "∃ T. a2meets T l  ∧ a2meets T k"
   then obtain T where T_on_l: ‹a2meets T l› and T_on_k: ‹a2meets T k›
     by blast
   obtain u v where T_form: "T = A2Point u v"
     by (cases T)
   have "u = x0"
     using T_form T_on_l l_form by auto
   have "u = x1"
     using T_form T_on_k k_form by auto
   show False
     using ‹u = x0› ‹u = x1› diff_x by blast
 qed


A version with fewer repetition is:

lemma A2_vert:
  assumes
    diff_x: ‹x0 ≠ x1› and
    l_form: ‹l = A2Vertical x0› and 
    k_form: ‹k = A2Vertical x1›
  shows ‹¬ (∃T. a2meets T l  ∧ a2meets T k)›
proof
  assume "∃ T. a2meets T l  ∧ a2meets T k"
  then obtain T where T_on_l: ‹a2meets T l› and T_on_k: ‹a2meets T k›
    by blast
  obtain u v where T_form: "T = A2Point u v"
    by (cases T)
  have "u = x0"
    using T_form T_on_l l_form by auto
  have "u = x1"
    using T_form T_on_k k_form by auto
  show False
    using ‹u = x0› ‹u = x1› diff_x by blast
qed


Now, you might wonder, why did the proof actually work in the first place with the free T? And why does metis warn that "Metis: The assumptions are inconsistent"? That happens because metis is able to find the contradiction directly, which leads to the following shorter proof:

lemma A2_vert: 
  assumes
    diff_x: ‹x0 ≠ x1› and
    l_form: ‹l = A2Vertical x0› and 
    k_form: ‹k = A2Vertical x1›
  shows ‹¬ (∃T. a2meets T l  ∧ a2meets T k)›
  by (metis assms a2meets.elims(2)
      a2meets.simps(2) diff_x k_form l_form)



> and (b) someone could show how to make the
> proof more idiomatic and perhaps briefer (which might entail rewriting the
> lemma itself, and if that's necessary, it's fine with me).


Additionally, I would replace the assumptions on l and k by a defines, remove the exist quantifier, use cartouche, reverse the theorem, and use auto:


lemma A2_vert2:
  fixes x0 x1 :: real
  defines l_form: ‹l ≡ A2Vertical x0› 
  defines k_form: ‹k ≡ A2Vertical x1›
  assumes ‹a2meets T l› and ‹a2meets T k›
  shows ‹l = k› 
  by (cases T) (use assms in auto)


However, that is only a matter of taste. This version means something slightly different (if two parallel vertical intersect, then they are equal).



Mathias


> 
> --John




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