Say I'm proving a theorem that assumes "n ≥ m
" (both are natural numbers), and I apply induction on n
. In the base case, the assumption is that "n = 0
". With these two, we can conclude that, in the base case, "m = 0
".
However, I'm having trouble in using the statement "n = 0
":
lemma foo:
assumes "(n::nat) ≥ (m::nat)"
shows ...
proof (induct n)
case 0
have "m = 0" using <I don't know what to put here> assms by simp
...
qed
I've tried using "n = 0"
, but it appears to be an "Undefined fact
". I've also tried adding it as an assumption, but to no avail. Nonetheless, it is clear that it is an implicit assumption when analyzing the base case.
So, how may I use the assumption of the base case directly in my proof?
Any assumptions that you need to be part of the induction need to be part of the proof state when you call
induct
. In particular, that should be all assumptions that contain the thing you do the induction over (i.e. all the ones that containn
in your case).You should therefore do a
using assms
before theproof
. Then0 ≥ m
will be available to you in the base case, under the name"0.prems"
(or just0
for all of these plus the induction hypothesis, which in this case doesn't exist).