Email Gateway (Aug 23 2022 at 08:12): Email Gateway (Aug 23 2022 at 08:12):From: "John F. Hughes" <jfh@cs.brown.edu>
I've finally gotten to a state where I can prove multiple small lemmas
(with a great deal of help from "try") fairly smoothly. But I'm stuck on
something that seems... well, as usual, it seems completely obvious to me,
but none of Isabelle's solvers can get anywhere at all, apparently.
I'm trying to prove things about the ordinary affine plane. I'm using
"a2meets P k" to mean "the point P is on the line k". Lines are either
Vertical or Ordinary, the latter being lines with equations of the form y =
mx + b. Here's the set-up for all that:
datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real" | A2Vertical "real"
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)"
definition a2parallel:: "a2ln ⇒ a2ln ⇒ bool" (infix "a2||" 50)
where "l a2|| m ⟷ (l = m ∨ (∀ P. (¬ a2meets P l) ∨ (¬a2meets P m)))"
I'm in the middle of proving that if you have a line l and a point P not on
l, there's a unique line l' parallel to l and containing p. I've shown that
such an l' exists; now I'm trying to show uniqueness.
So I'm trying to show that given a line l and a point P not on l, if m and
k are both parallel to l and both contain P, then m = k.
lemma A2_a2b:
fixes P
fixes l
fixes m
fixes k
assumes pl : "¬ a2meets P l"
assumes pm : "a2meets P m"
assumes pk : "a2meets P k"
assumes lm_parr : "l a2|| m"
assumes lk_parr : "l a2|| k"
shows "m = k"
I'm doing this by cases on l, and working on the case where l is Ordinary.
Using some lemmas, I'm able to show that k and m are both ordinary, and
both have the same slope as l:
proof (cases l)
case (A2Ordinary s1 b1)
fix s1 b1 assume lo: "l = A2Ordinary s1 b1"
fix x0 y0 assume P: "P = A2Point x0 y0"
then have mform: "∃b2. m = A2Ordinary s1 b2 " using A2_parallel_2
A2_parallel_3 lm_parr lo by fastforce
also have kform: "∃b3. k = A2Ordinary s1 b3 " by (metis A2Ordinary
A2_parallel_2 A2_parallel_3 calculation lk_parr lm_parr)
So at this point, I have that k is and ordinary line with slope s1 and
intercept b3. I know, from the hypotheses, that "a2meets P k", i.e., that
the point P = A2Point x0 y0 lies on k, which (by the definition of a2meets)
says that y0 = s1*x0 + b3". But when I assert this and use "try" to find a
proof...it tries in vain:
also have "y0 = s1*x0 + b3" try
It even tries in vain if I try to help it along by suggesting some useful
tips:
also have "y0 = s1*x0 + b3" using kform pk try
I have the feeling that I'm approaching this kind of thing completely
wrong, because even the most obvious things like this one seem tough.
Email Gateway (Aug 23 2022 at 08:12):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I might have reproduced your theory incorrectly but:
The b3 you have in
"∃b3. k = A2Ordinary s1 b3 "
is not the same as the b3 you have in
also have "y0 = s1*x0 + b3"
The first is bound and the second is free. The Isabelle IDE might be
indicating this by drawing the background of the b3 in
also have "y0 = s1*x0 + b3"
differently.
You will need to use something like obtain to fix the b3. For example,
replace
"∃b3. k = A2Ordinary s1 b3 "
with
obtain b3 where "k = A2Ordinary s1 b3 " <you will need some proof of this>
You will need to do similar for b2 and then prove b2 = b3.
Cheers
Mark
Email Gateway (Aug 23 2022 at 08:13):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks, Thomas and Mark.
Or, the short form of all this, it's easy to think that the problem is
proving true statements in a formal system.
Actually the first challenge is to state a true statement.
That's a fun way to put it, but ... with a half-century of practice, I'm
pretty good at proving things (and stating true things to prove). I'm just
not good at understanding Isabelle/Isar (to put it very mildly!)
Your answer says a bunch of useful things, like:
You begin your proof with "cases l", and the first case with "case (A2Ordinary
s1 b1)". This automatically fixes variables
s1 and b1 and assumes that "l = A2Ordinary s1 b1". The assumption is
initially named A2Ordinary (the name of the case), and also "this".
The assume gadget is just for restating existing assumptions.
You need to tell it you want x to be a new name for a thing. As Mark
said, the right thing in this case is "obtain", which was also the right
way to handle "P = A2Point x0 y0".
...and I'd like to know whether there's DOCUMENTATION anywhere that
actually says these things. I'd be very very happy to read it and stop
asking naive questions if I possibly could.
I'd also like to understand why the "State" sidebar seems to not know about
s1 and b1. For instance, after I've written
case (A2Ordinary s1 b1)
then
have mform: "∃b. m = A2Ordinary s1 b"
using A2Ordinary A2_parallel_2 A2_parallel_3 lm_parr by fastforce
and click just after "then" the sidebar says:
proof (chain)
picking this:
l = A2Ordinary s1 b1
but clicking after "fastforce" it says
proof (state)
this:
∃b. m =
A2Ordinary s1 b
goal (2 subgoals):
⋀x11 x12.
l =
A2Ordinary x11
x12 ⟹
m = k
⋀x2. l = A2Vertical
x2 ⟹
m = k
I don't understand why the "goal" still has two subgoals, even though I'm
in the "Ordinary" case, and why those subgoals use x11 and x12 rather than
s1 and b1, for instance. This is clearly a problem, because even after I do
a bunch more steps eventually showing that m = k, the proof-state still
looks the same (except that "this" is now "m = k")
On Tue, Jan 21, 2020 at 11:05 AM Thomas Sewell <sewell@chalmers.se> wrote:
Mark seems to have said similar things, here's my version:
The short answer is, "try" can't prove some of the goals you've stated
because they aren't true.The script you've attached contains a bunch of confusion about how Isar
proof syntax works. Let me point out three cases:You begin your proof with "cases l", and the first case with "case (A2Ordinary
s1 b1)". This automatically fixes variables s1 and b1 and assumes that "l
= A2Ordinary s1 b1". The assumption is initially named A2Ordinary (the
name of the case), and also "this". You've fixed new copies of s1 and b1
and assumed the assumption again. I'm not sure if that's a problem but it
is a possible source of confusion.You then assume "P = A2Point x0 y0" which is definitely a problem. You're
in danger of the "fails to refine any pending goal" error. The assume
gadget is just for restating existing assumptions, and this isn't an
existing assumption.Finally, having proven "∃b2. m = A2Ordinary s1 b2", you attempt to show "y0
= s1*x0 + b2". The misunderstanding here is that the exists syntax is a
binder, and the syntactic name b2 is meaningful only within the scope of
the exists. Mark pointed this out.Isar forces you to be intentional about these things. You can prove that "∃x.
..." with some property, and it won't try to unpack that x. If it did, you
might get confusion between different instances of x. You need to tell it
you want x to be a new name for a thing. As Mark said, the right thing in
this case is "obtain", which was also the right way to handle "P =
A2Point x0 y0". You want to obtain x0/y0/b2 at the proof scope with these
properties.To clarify:
obtain x0 y0 where P: "P = A2Point x0 y0"
by (cases P; simp)Or, the short form of all this, it's easy to think that the problem is
proving true statements in a formal system. Actually the first challenge is
to state a true statement.Cheers,
Thomas.
From: cl-isabelle-users-bounces@lists.cam.ac.uk <
cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of John F. Hughes <
jfh@cs.brown.edu>
Sent: Tuesday, January 21, 2020 3:49:08 PM
To: Cl-isabelle Users
Subject: [isabelle] Why can't Isabelle seem to get anywhere on this
apparently simple problem?I've finally gotten to a state where I can prove multiple small lemmas
(with a great deal of help from "try") fairly smoothly. But I'm stuck on
something that seems... well, as usual, it seems completely obvious to me,
but none of Isabelle's solvers can get anywhere at all, apparently.I'm trying to prove things about the ordinary affine plane. I'm using
"a2meets P k" to mean "the point P is on the line k". Lines are either
Vertical or Ordinary, the latter being lines with equations of the form y =
mx + b. Here's the set-up for all that:datatype a2pt = A2Point "real" "real"
datatype a2ln = A2Ordinary "real" "real" | A2Vertical "real"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)"definition a2parallel:: "a2ln ⇒ a2ln ⇒ bool" (infix "a2||" 50)
where "l a2|| m ⟷ (l = m ∨ (∀ P. (¬ a2meets P l) ∨ (¬a2meets P
m)))"I'm in the middle of proving that if you have a line l and a point P not on
l, there's a unique line l' parallel to l and containing p. I've shown that
such an l' exists; now I'm trying to show uniqueness.So I'm trying to show that given a line l and a point P not on l, if m and
k are both parallel to l and both contain P, then m = k.lemma A2_a2b:
fixes P
fixes l
fixes m
fixes k
assumes pl : "¬ a2meets P l"
assumes pm : "a2meets P m"
assumes pk : "a2meets P k"
assumes lm_parr : "l a2|| m"
assumes lk_parr : "l a2|| k"
shows "m = k"I'm doing this by cases on l, and working on the case where l is Ordinary.
Using some lemmas, I'm able to show that k and m are both ordinary, and
both have the same slope as l:proof (cases l)
case (A2Ordinary s1 b1)
fix s1 b1 assume lo: "l = A2Ordinary s1 b1"
fix x0 y0 assume P: "P = A2Point x0 y0"
then have mform: "∃b2. m = A2Ordinary s1 b2 " using A2_parallel_2
A2_parallel_3 lm_parr lo by fastforce
also have kform: "∃b3. k = A2Ordinary s1 b3 " by (metis A2Ordinary
A2_parallel_2 A2_parallel_3 calculation lk_parr lm_parr)So at this point, I have that k is and ordinary line with slope s1 and
intercept b3. I know, from the hypotheses, that "a2meets P k", i.e., that
the point P = A2Point x0 y0 lies on k, which (by the definition of a2meets)
says that y0 = s1*x0 + b3". But when I assert this and use "try" to find a
proof...it tries in vain:also have "y0 = s1*x0 + b3" try
It even tries in vain if I try to help it along by suggesting some useful
tips:also have "y0 = s1*x0 + b3" using kform pk try
I have the feeling that I'm approaching this kind of thing completely
wrong, because even the most obvious things like this one seem tough.
Email Gateway (Aug 23 2022 at 08:13):From: Peter Zeller <p_zeller@cs.uni-kl.de>
On 21.01.20 18:03, John F. Hughes wrote:
...and I'd like to know whether there's DOCUMENTATION anywhere that
actually says these things. I'd be very very happy to read it and stop
asking naive questions if I possibly could.
For me the best resource was Chapter 4 in the prog-prove documentation
(in the documentation Sidebar of jedit or at
https://isabelle.in.tum.de/doc/prog-prove.pdf). If you already know how
to do proofs on paper, this chapter gives you the basic patterns to
express the proofs in Isabelle.
I don't understand why the "goal" still has two subgoals, even though I'm
in the "Ordinary" case, and why those subgoals use x11 and x12 rather than
s1 and b1, for instance. This is clearly a problem, because even after I do
a bunch more steps eventually showing that m = k, the proof-state still
looks the same (except that "this" is now "m = k")
You have to use "show" to complete a goal. "have" is just for
intermediate steps.
The fact that variables are not renamed in the proof state is something
I also find annoying. Sometimes I temporarily use rename_tac to make it
easier to copy formulas from the proof panel. Sometimes it's possible to
use "show ?case" or "show ?thesis" to see the goal with the correct
variable names.
-- Peter
Last updated: Nov 21 2024 at 12:39 UTC