Email Gateway (Aug 19 2022 at 09:33): Email Gateway (Aug 19 2022 at 09:33):From: Edward Schwartz <edmcman@cmu.edu>
Hi,
I am trying to prove a fairly straight-forward property in Isar:
Assumption S ==> P S
I am trying to prove P by induction on S.
proof -
assume Asm: "Assumption S"
have "P S"
proof (induct S)
case (Foo arg) from Asm show ?case by simp
And here is where the problem occurs. Asm refers to S. But all of the
current proof goals and assumptions are in terms of Foo arg. There doesn't
seem to be any fact that says S = Foo arg.
How can I structure my proof so this works?
Thanks,
Ed
Email Gateway (Aug 19 2022 at 09:33):From: Julian Brunner <julianbrunner@gmail.com>
Hello,
You'll want to change your proof to something like
proof -
assume Asm: "Assumption S"
from Asm have "P S"
proof (induct S)
case (Foo arg) from Foo show ?case by simp
That way, your assumption is included in the induction and will
reappear as part of Foo.
Cheers,
Julian
Email Gateway (Aug 19 2022 at 09:33):From: Tobias Nipkow <nipkow@in.tum.de>
Alternatively you can usually state and prove your implication directly:
... "Assumption S ==> P S"
proof(induct S)
Regards
Tobias
Email Gateway (Aug 19 2022 at 09:33):From: Edward Schwartz <edmcman@cmu.edu>
Thank you! In retrospect, this makes perfect sense.
Email Gateway (Aug 19 2022 at 09:34):From: Edward Schwartz <edmcman@cmu.edu>
Hi,
I just wanted to follow-up in case anyone finds this thread in the archive.
I spoke too quickly. Julian's solution does ensure that the Assumption
S fact is available during the induction. However, S still remains
unconnected to Foo arg, the current induction form. Because of this, I
cannot show Assumption (Foo arg).
I was able to get the proof to work by including the assumption as part of
the induction hypothesis, as Tobias suggested. I had tried this before,
actually, but was running into trouble because I did not use the next
command between induction cases. This was very confusing to me, because I
normally don't need to use next. I guess it matters here because each
induction case will add to the assumptions, and so it needs to be reset.
Thank you to both Julian and Tobias for the help.
Edward
Last updated: Apr 26 2024 at 20:16 UTC