Email Gateway (Aug 22 2022 at 20:26): Email Gateway (Aug 22 2022 at 20:26):From: "John F. Hughes" <jfh@cs.brown.edu>
I want to show that in the Euclidean plane, there is a unique line between
any two distinct points. I want to show this is a particular way, so that I
can later show that my notion of a point in the Euclidean plane being on a
line matches the requirements for defining a (more general) affine plane,
i.e., I want to show that the Euclidean plane is an affine plane. To get
there, I define a function "a2meets P l" that is true when P is a point on
the line l, false otherwise. Points are pairs of reals, lines are either
vertical or "ordinary" (i.e., have an equation like y = mx + b). I want to
prove this:
"P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
To keep things simple, I proved existence and uniqueness separately:
theorem a1a:
fixes P :: a2pt
fixes Q
assumes "P ≠ Q"
shows "∃ ls . a2meets P ls ∧ a2meets Q ls"
lemma a1b:
fixes P :: a2pt
fixes Q
fixes l
fixes m
assumes pq: "P ≠ Q"
assumes pl : "a2meets P l"
assumes ql : "a2meets Q l"
assumes pm : "a2meets P m"
assumes qm : "a2meets Q m"
shows "l = m"
I'd now like to conclude the overall theorem. It's pretty clear (to me!)
that a1a and a1b imply the result, but the only way I can coax Isar to get
there seems needlessly convoluted:
theorem a1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof -
assume "P ≠ Q"
show ?thesis
proof (cases P)
case (A2Point x0 y0)
then show ?thesis
proof (cases Q)
case (A2Point x1 y1)
have ?thesis using ‹P ≠ Q› a1a a1b by blast
show ?thesis by (simp add: ‹∃!l. a2meets P l ∧ a2meets Q l›)
qed
qed
qed
Of course, a1a and a1b do appear in there, but are the nested cases really
necessary? (I wouldn't ask if I hadn't tried about 15 other approaches)
More generally, is there structure for proofs of existence of a unique
item satisfying some criteria, analogous to the nice structures we have for
proof-by-cases, or proof-by-various-forms-of-induction? Complete .thy file
follows.
--John
theory Small
imports Complex_Main
begin
section {* The real affine plane *}
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)"
text{* Now show a basic property: through any two distinct points,
there's a unique line,
which, for consistency with the main theory, we want to write as
"P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l" *}
text{* Start with just existence *}
theorem a1a:
fixes P :: a2pt
fixes Q
assumes "P ≠ Q"
shows "∃ ls . a2meets P ls ∧ a2meets Q ls"
proof (cases P)
case P: (A2Point x0 y0)
then show ?thesis
proof (cases Q)
case Q: (A2Point x1 y1)
then show ?thesis
proof (cases "(x0 = x1)")
case True
assume f: "x0 = x1"
have x1x0: "x1 = x0" by (simp add: True)
let ?ll = "A2Vertical x0"
have m1: "a2meets P ?ll" using P by simp
have m2: "a2meets Q ?ll" using Q by (simp add: x1x0)
thus ?thesis using m1 by blast (* We've proved the theorem...in the
case where x0 = x1 *)
next
case False (* Now on to the other case, where x0 ≠ x1; it's clear
what the answer is,
but tought to coax Isabelle along to see it. *)
assume f: "x0 ≠ x1"
have x01 : "x1 - x0 ≠ 0" using f by simp
let ?ll = "A2Ordinary ((y1-y0)/(x1-x0)) (y0 -
((y1-y0)/(x1-x0))*x0) "
(* we want to show that P and Q are both on ll; P is easy for
some reason; Q is not *)
have m3: "a2meets P ?ll" using P by simp
(* Now address the case of Q by doing all the algebra one step
at a time *)
have s2: "((y1-y0)/(x1 - x0))* x1 + (y0 - ((y1-y0)/(x1 - x0) )*x0)
= ((y1-y0) * x1/(x1 - x0)) + (y0 - ((y1-y0)/(x1 - x0) )*x0)" by simp
also have s3 : "... = ((y1-y0) * x1/(x1 - x0)) + (y0 -
((y1-y0)*x0/(x1 - x0) ))" by simp
also have s4 : "... = ((y1x1-y0x1) /(x1 - x0)) + (y0 -
((y1x0-y0x0)/(x1 - x0) ))" by argo
also have s5 : "... = ((y1x1-y0x1) /(x1 - x0)) + (y0*(x1 -
x0)/(x1-x0) - ((y1x0-y0x0)/(x1 - x0) ))" using x01 by simp
also have s6 : "... = ((y1x1-y0x1) /(x1 - x0)) + ((y0*x1 -
y0x0)/(x1-x0) - ((y1x0-y0*x0)/(x1 - x0) ))" by argo
also have s7 : "... = (y1x1-y0x1) /(x1 - x0) + ((y0x1 - y0x0)
(y1x0-y0x0))/(x1 - x0) " by argo
also have s8 : "... = ((y1x1-y0x1) + (y0x1 - y0x0) -
(y1x0-y0x0))/(x1 - x0) " by argo
also have s9 : "... = (y1x1-y0x1 + y0x1 - y0x0 -
y1x0+y0x0)/(x1 - x0) " by argo
also have s10 : "... = (y1x1 - y0x0 - y1x0+y0x0)/(x1 - x0) "
by argo
also have s11 : "... = (y1x1 - y1x0)/(x1 - x0) " by argo
also have s12 : "... = (y1*(x1 - x0))/(x1 - x0) " by argo
also have s13 : "... = y1 " using x01 by simp
finally have s14: "((y1-y0)/(x1 - x0))* x1 + (y0 - ((y1-y0)/(x1 -
x0) )*x0) = y1" .
moreover have m4: "a2meets Q ?ll" using s14 by (simp add: Q)
show ?thesis using m3 m4 by auto
qed
qed
qed
text{*For this next theorem, it might make sense to phrase it as
lemma a1b: "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l", i.e., as the final
result,
but that would require proving the existence of l (which we just did in the
previous lemma) and
then proving that it's unique. Instead, we can just say that if l and m
both contain the
distinct points P and Q, then l must equal m. From this, and the previous
lemma, we can then
conclude that axiom 1 is true (which we'll do in a final theorem).
*}
lemma a1b:
fixes P :: a2pt
fixes Q
fixes l
fixes m
assumes pq: "P ≠ Q"
assumes pl : "a2meets P l"
assumes ql : "a2meets Q l"
assumes pm : "a2meets P m"
assumes qm : "a2meets Q m"
shows "l = m"
proof (cases P)
case (A2Point x0 y0)
then show ?thesis
proof (cases Q)
case (A2Point x1 y1)
have ?thesis
proof (cases l)
case (A2Ordinary s1 b1) (* l is ordinary *)
assume lo: "l = A2Ordinary s1 b1"
then show ?thesis
proof (cases m) (* Handle m ordinary, vertical in two steps *)
case (A2Ordinary s2 b2)
then show ?thesis by (smt A2Point a2ln.inject(1) a2meets.elims(2)
a2meets.simps(1) a2pt.inject crossproduct_noteq lo pl pm pq ql qm)
next
case (A2Vertical x2)
then have ?thesis using A2Point a2meets.elims(2) pl pm pq ql qm
by fastforce
show ?thesis by (simp add: ‹l = m›)
qed
next
case (A2Vertical x2) (* l is vertical *)
then show ?thesis by (smt a2ln.inject(1) a2meets.elims(2)
a2meets.simps(2) pl pm pq ql qm)
qed
show ?thesis by (simp add: ‹l = m›)
qed
qed
theorem a1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof -
assume "P ≠ Q"
show ?thesis
proof (cases P)
case (A2Point x0 y0)
then show ?thesis
proof (cases Q)
case (A2Point x1 y1)
have ?thesis using ‹P ≠ Q› a1a a1b by blast
show ?thesis by (simp add: ‹∃!l. a2meets P l ∧ a2meets Q l›)
qed
qed
qed
Email Gateway (Aug 22 2022 at 20:26):From: Thomas Sewell <sewell@chalmers.se>
I think that your nested proof of theorem a1 is just a long version of this:
theorem a1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
using a1a a1b by blast
The core of your proof is that blast knows how to show exists-unique properties if you give it both a1a and a1b.
I think that blast solves this using a default introduction rule for exists-unique, which is either ex1I or ex_ex1I. Here's a more Isar approach to the problem using ex_ex1I. I think that this style of using goal_cases is considered standard:
theorem a1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof (rule ex_ex1I, goal_cases)
case 1
assume "P ≠ Q"
then show ?case by (rule a1a)
next
case (2 l y)
then show ?case by (simp add: a1b)
qed
I'm not sure what else to say. Perhaps you're looking for a particular style of proof?
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 20:26):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks, Thomas. that "using a1a a1b by blast" thing was exactly what I was
looking for. In particular, it gives me confidence that my phrasing of a1b
wasn't getting the way of things; I find it's easy to say (for real
numbers, for instance) something like "x1 != x2" instead of "x1 - x2 != 0"
(which seem completely equivalent to me), and have it make a huge
difference to the complexity of a proof, so knowing that this pattern makes
things work is great.
I now see that using "try" right after the statement of the theorem
produces your "blast" proof. Instead of doing that, I had tried
theorem a1 : "P ≠ Q ⟹ ∃! l . a2meets P l ∧ a2meets Q l"
proof -
try
and gotten a "tried in vain" result. I'm not sure I understand why there's
a difference.
But more generally, you recommend an alternate Isar-idiomatic proof using
"ex_ex1I, goal_cases", and (like the "blast" case), I'm wondering how I can
learn
(a) that these rules/provers exist at all, and
(b) what each of these rules or provers is actually good at.
Looking at "Programming and Proving", for instance, the word "metis"
appears exactly four times, once with a brief description that suggests
that IT should be the tool used here rather than "blast". As a new user,
I'm constantly being surprised by new tools like "goal_cases" and
"ex_ex1l", neither of which is mentioned at all in P&P.
--John
Email Gateway (Aug 22 2022 at 20:26):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I would add:
theorem a1 :
assumes "P ≠ Q"
shows "∃! l . a2meets P l ∧ a2meets Q l"
proof -
have "∃l. a2meets P l ∧ a2meets Q l"
using assms a1a by simp
moreover have "⋀l l'. ⟦ a2meets P l ∧ a2meets Q l; a2meets P l' ∧ a2meets Q l' ⟧ ⟹ l' = l"
using assms a1b by simp
ultimately show ?thesis by blast
qed
Maybe this is more the structure John is looking for.
The default method for ∃! demands that the witness be exhibited:
theorem a1 :
assumes "P ≠ Q"
shows "∃! l . a2meets P l ∧ a2meets Q l"
proof
show "a2meets P XXX ∧ a2meets Q XXX"
sorry
show "⋀l. a2meets P l ∧ a2meets Q l ⟹ l = XXX"
sorry
qed
so it is not very convenient with the lemmas that have already been set up.
Email Gateway (Aug 22 2022 at 20:26):From: Thomas Sewell <sewell@chalmers.se>
OK, let's clarify a bit. The ex_ex1I here is a theorem, not a mechanism. It's being used as an introduction rule here via "rule".
I'd recommend people learning Isabelle to learn (roughly) what the rule-application calculus is, what intro/dest/elim rules do, and thus how to use them manually and also how to supply them to some tools, e.g. (clarsimp dest!: ...) or (blast intro: ...). Unfortunately I don't actually know where in the reference material to point you.
Since it's a rule, you can search for it with find_theorems. I found the theorem by searching for rules that can prove exists-unique properties, like so:
find_theorems "_ ⟹ ∃!_. _"
I actually didn't know what goal_cases did until an hour or two ago. I was looking for a way to use ex_ex1I in an Isar-like way, and I vaguely recalled that there was a new feature with cases in its name, and managed to figure it out from there. Roughly speaking, it sets you up to continue in an Isar structured proof from some goal state, which I created here by applying a rule.
I think it is a real problem of a big complex system like this that there are features out there which you have likely forgotten about. In a long former Isabelle project, I famously forgot about a feature that I had implemented myself. You can find rules with both the sledgehammer and try, but there's no equivalent gadget for finding tools or understanding what they do.
Quick primer: blast and metis are both first-order solvers. Blast does a search which involves introduction/elimination steps similar to Isabelle rule steps, and it uses the default rule sets. That's how it knew how to prove an exists-unique without being told a rule about it, ex_ex1I is a global default introduction rule. Metis doesn't have that global setup, but it understand equality better and generally has a smarter search strategy, if it's given enough information. There are, of course, many other variants.
Asking the list: is there a good cheat-sheet or primer for commonly used methods/tactics and quick intuitions of when they're likely to be useful?
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 20:27):From: Karn Kallio <tierpluspluslists@skami.org>
With respect to this comment:
I have been making an on and off investigation into Isabelle, and have
found the only practical way to learn these sorts of things is to spend
a lot of time reading the developments in the AFP. The you will
discover them, and by the context of use get an idea of when they may
be helpful.
Last updated: Apr 26 2024 at 04:17 UTC