Email Gateway (Aug 22 2022 at 17:36): Email Gateway (Aug 22 2022 at 17:36):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have a problem with bindings in a double inductive rule inductive proof.
The following is a contrived example:
inductive P :: "nat ⇒ bool"
and Q :: "nat ⇒ bool"
where
"Q n ⟹ P (n+1)"
| "P n ⟹ Q (n+1)"
lemma
fixes x::nat
shows "P n ⟹ Q m ⟹ P (n+m) "
and "Q n ⟹ Q m1 ⟹ P (n+m1)"
proof(induction arbitrary: m m1 rule: P_Q.inducts)
case (1 n)
then show ?case sorry
next
case (2 n)
then show ?case sorry
qed
If I put the cursor at the proof line I see:
m1 is a free variable; m is bound.
Why is m1 still free even though I have specified that it should be
arbitrary? Including m1 in the arbitrary specification makes no difference
however removing m from the specification does make m free (as expected).
Cheers
Mark
Email Gateway (Aug 22 2022 at 17:36):From: Lars Hupel <hupel@in.tum.de>
Hi Mark,
try this:
proof(induction arbitrary: m and m1 rule: P_Q.inducts)
Does that yield the proof state that you expected?
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:36):From: Mark Wassell <mpwassell@gmail.com>
Hi,
Yes it does. Thank you.
Mark
Last updated: Nov 21 2024 at 12:39 UTC