Email Gateway (Aug 22 2022 at 19:24): Email Gateway (Aug 22 2022 at 19:24):From: "John F. Hughes" <jfh@cs.brown.edu>
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, 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).
--John
Email Gateway (Aug 22 2022 at 19:24):From: Lawrence Paulson <lp15@cam.ac.uk>
Maybe you are over complicating things with your definitions. Isn’t your statement simply the thing below?
lemma "a ≠ b ⟹ disjnt (range (λy. (a,y))) (range (λy. (b,y)))"
by (auto simp: disjnt_def)
Larry Paulson
Email Gateway (Aug 22 2022 at 19:24):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi John,
On 28. Mar 2019, at 14:39, John F. Hughes <jfh@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
Email Gateway (Aug 22 2022 at 19:24):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks...this is exactly what I was looking for. It leads me to a few
more questions, though,
that with the different background. You want something along:
obtain T where
‹…›
* Similarly, you have to use obtain for u and v, not fix.
Can you suggest somewhere that I can learn the distinction between "obtain"
and "fix"? The reference manual has a paragraph that's too cryptic for my
current understanding of logic (which is quite basic); Ballarin's tutorial
slides basically say "they're different". I think I need something in the
middle. :)
* 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.
If I actually wanted to do a proof by contradiction, even though it's not
necessary here, would I have to start with
proof (rule ccontr)
assume "¬¬ (∃ T. a2meets T l ∧ a2meets T k)"
Perhaps choosing a theorem with a negation in the conclusion was a bad
place to start trying to use proof-by-contradiction. But I'd really like to
see how to do such a proof.
Later you suggest restating the theorem as its contrapositive (which may or
may not be a good idea...I don't know whether Isabelle can use the
contrapositive as effectively for what I need to do next), and propose
three things (which I've reordered):
My questions:
-- Typing double-quotes is easy; typing cartouches is tough (for me) ---
is there some simple way to do this, and are they the preferred form now?
-- the reference manual, page 102) says that 'defines" defines a
previously declared parameter, but in your use
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)the parameters l and k haven't been previously declared (as far as I can
tell). Of course, that description of "defines" is in the section about
locales in the reference manual, so it's probably the wrong one. But it's
the only mention of that keyword in the whole manual, so I'm at a loss for
what this actually means here.
-- does this form of the statement really remove the "exists" quantifier?
Or is there an implicit "exists" in the "assumes" line? And does removing
it (assuming it's really gone) make things easier for the prover?
--John
Email Gateway (Aug 22 2022 at 19:24):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Have you studied the tutorial “Programming and Proving in Isabelle/HOL”
(prog-prove)? I find it extremely helpful for getting started with
Isabelle. It also mentions obtain.
You use fix if you want to prove a ⋀-statement; fix x means that
the following lines work under the assumption that an x is given to
you. You use obtain x where P if you can prove that there is an x
for which P is true and you want to get hold of such an x.
All the best,
Wolfgang
Last updated: Apr 24 2024 at 20:16 UTC