John Hughes (Mar 12 2024 at 15:42): John Hughes (Mar 12 2024 at 15:42):Here's a tiny theorem and somewhat wordy proof as I might write it as a mathematician, giving an example of induction to someone who's new to the idea.
Theorem: For any natural number k, there's a natural number n with k + 5 < n.
Proof: In the case where k is 0, the number 0 + 5 is less than n = 6, and we're done.
In the case where k is a successor, we suppose (inductive hypothesis) that m is a natural number with
k + 5 < m; we then need to exhibit a natural number larger than Succ(k) + 5.
Let n = Succ(m).
We have
k + 5 < m
Applying the successor operation to both sides, we get
Succ(k+5) < Succ(m)
and applying [a lemma about addition] we have
Succ(k) + 5 = Succ(k + 5).
Combining, we get
Succ(k) + 5 < Succ(m), and thus
Succ(k) + 5 < n
as needed. QED
I'd like to mimic this proof in Isabelle. I know that there are other easy proofs of this tiny theorem (presburger can do it, for instance), but I'd really like to write out this proof, and I'm failing in my attempts. So far I have
theory Scratch
imports Main
begin
lemma "T5": " ∃ (n::nat) . (k::nat) + 5 < n"
proof (induction k)
case 0
then show ?case by auto
next
case (Suc k)
then show ?case sorry (* problem *)
qed
end
My challenge is that at the line marked "problem", I have that this is ∃n. k + 5 < n, and the goal is ⋀k. ∃n. k + 5 < n ⟹ ∃n. Suc k + 5 < n.
I have three problems:
this, I'd like to say "OK, so there's some n with that property. Let's call it m.", but I don't know how to do that in Isabelle.Suc k + 5 < p for some p (as I did in the k = 0 case), Isabelle can infer the "there-exists" result from that instance, using P(a) => EX x . P(x). /\k at the front now. I can get rid of it by saying show ?case
proof -
but I honestly don't know why it's there in the first place.
If someone could complete my proof (mimicking the English-language proof), OR address any of these problems, I'd be grateful.
Mathias Fleury (Mar 12 2024 at 15:51):I am doing it this time, but you should look up the prog-prove for the Isabelle tutorial:
lemma "T5": " ∃ (n::nat) . (k::nat) + 5 < n"
proof (induction k)
case 0
then show ?case by auto
next
case (Suc k)
then obtain n where n: ‹k + 5 < n› ―‹From this, I'd like to say "OK, so there's some n with that property. Let's call it m.›
by blast
let ?p = ‹Suc n›
from n have ‹Suc k + 5 < ?p› ―‹I show that Suc k + 5 < p for some p (as I did in the k = 0 case)›
by auto
then show ?case
by (rule exI[of _ ‹Suc n›]) ―‹Isabelle can infer the "there-exists" result from that instance, using P(a) => EX x . P(x). ›
qed
I should have prefaced this with "I read the prog-prove discussion over and over and just couldn't piece it together after an hour of experimentation last night, which is why I've come back to the well again this morning" The word "obtain" is the one I needed, obviously. Having spent a lot of time answering naive questions on math stackexchange, I certainly appreciate your willingness to assist.
Mathias Fleury (Mar 12 2024 at 16:22):Generally having a look at the examples in src/HOL/Examples/ can be useful to see what constructs exists
Mathias Fleury (Mar 12 2024 at 16:23):The appendix https://isabelle.in.tum.de/doc/isar-ref.pdf can also give some hints
Last updated: Apr 28 2024 at 16:17 UTC