Email Gateway (Aug 22 2022 at 20:23): Email Gateway (Aug 22 2022 at 20:23):From: "John F. Hughes" <jfh@cs.brown.edu>
I often find myself trying to prove things in a context like this:
Theorem: Given this, that, and the other, there's a widget X with these
properties.
An example might be
Theorem: Given two real numbers r and s, with r < s there's a real number t
between them, i.e., with r < t and t < s.
My approach, as a mathematician, is often to explicitly construct the
widget described, and show it has the properties needed. In the example
theorem, I'd say: let t = (r+s)/2. Then because r < s, we know that r+r <
r + s, so (dividing by 2) r < (r+s)/2, so r < t. [Then I'd write a similar
proof for t < s. ]
I seem, in Isar, to often reach a state where I've done exactly this --
I've established the existence of the missing widget by explicitly
constructing it -- but I can't make Isar say, "Oh, good...we're done here!"
In the example above, Isar can figure out a proof all on its own, but since
that's not true in general (most of the constructive proofs I'm doing are
beyond its 'i can do that' skills), I'd like to work through the details to
get the general structure.
I have a feeling that part of the problem is that there's an implict
"forall r, forall s" in front of the theorem, while I want to do my proof
by doing it for a particular (but arbitrary) r (and s, of course).
I'm pretty sure I'm supposed to do that with "fix r" and "fix s". But then
I need to do something more. I figured that because I was trying to prove
that "r < s" implies something, I should assume that r < s, and proceed.
Here's a start:
theory Proof_practice
imports Complex_Main
begin
theorem mid: "(r::real) < s⟹∃t. ((r < t) ∧ (t < s))"
proof
fix r
fix s
assume "r < s"
let t = "(r+s)/2"
qed
end
The type-ascription on "r" seemed to be necessary; without it, auto
Quickcheck claimed to have a counterexample (apparently by assuming that I
meant r and s to be Enums rather than reals). Even so, the "r" in the first
line of the proof appears to be unrelated to the "r" in the theorem
statement, for it's described as a Skolem variable with type 'a, so that
the "let" line completely fails (complaining that "+" is not defined for
items of type 'a, quite reasonably).
Can someone describe a general pattern for proofs like this (where I
construct some object, and show that it has some properties, and then say
"see, that's proof that such a thing exists!"? It's clear that I'm headed
down the wrong path.
Email Gateway (Aug 22 2022 at 20:23):From: Tobias Nipkow <nipkow@in.tum.de>
theorem mid: "(r::real) < s⟹∃t. ((r < t) ∧ (t < s))"
You statement already introduces r and s, fixing them again introduces new r and
s, which is not what you want. You can also write the goal with assumes/shows
instead of ==> so you don't have to assume the assumptions once more but can
refer to them by the predefined name "assms". This leads to
theorem mid: assumes "(r::real) < s" shows "∃t. r < t ∧ t < s"
proof
let ?t = "(r+s)/2"
show "r < ?t ∧ ?t < s" using assms by simp
qed
Tobias
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC