Email Gateway (Aug 18 2022 at 17:41): Email Gateway (Aug 18 2022 at 17:41):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Sorry for just sending an incomplete message.
In the following example (taken from
~~/src/HOL/Induct/Common_Patterns.thy) there is apparently unnecessary
duplication.
lemma
fixes n :: nat
shows "P n" and "Q n"
proof (induct n)
case 0 case 1
show "P 0" sorry
next
case 0 case 2
show "Q 0" sorry
next
case (Suc n) case 1
note hyps = P n Q n (** this line ... **)
show "P (Suc n)" sorry
next
case (Suc n) case 2
note hyps = P n Q n (** ... duplicated *)
show "Q (Suc n)" sorry
qed
I want to know how to avoid this duplication. I have the common example
lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...) case 1 have "P x0" by fact show "Q1 x0" ...
case 2 have "P x0" by fact show "Q2 x0" ...
I want to eliminate the duplication in the last two lines.
In fact, playing with examples shows that
lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...x0...) ( the fact "P x0" is not known here )
case 1 have j:"P x0" by fact
show "Q1 x0" proof (... j ...)
case 2 show "Q2 x0" proof (... j ...) ( why is j in scope here? )
works. I don't understand the scoping of facts in this example.
Thanks,
Randy
Email Gateway (Aug 18 2022 at 17:42):From: Brian Huffman <brianh@cs.pdx.edu>
On Sun, May 15, 2011 at 3:25 PM, Randy Pollack <rpollack@inf.ed.ac.uk> wrote:
lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...) case 1 have "P x0" by fact show "Q1 x0" ...
case 2 have "P x0" by fact show "Q2 x0" ...I want to eliminate the duplication in the last two lines.
I think I understand your problem now. Did you mean to say, "using h j
proof (induct)" above?
Here is another example adapted from HOL/Induct/Common_Patterns.thy;
I've added the extra assumption "C n" which is added to the inductive
hypothesis. At the point of "case (Suc n)", you might like to be able
to use the assumption "C (Suc n)" to derive some other facts, and use
those in both subcases 1 and 2. The problem is that the "case" command
does not assume "C (Suc n)" for you until you get all the way down to
the subcases.
lemma
fixes n :: nat
assumes "C n"
shows "A n ==> P n"
and "B n ==> Q n"
using C n proof (induct n)
case 0
{
case 1 note A 0 show "P 0" sorry
next
case 2 note B 0 show "Q 0" sorry
}
next
case (Suc n)
note A n ==> C n ==> P n
and B n ==> C n ==> Q n
(* C (Suc n) has not been assumed yet at this point *)
{
case 1
note A (Suc n) and C (Suc n)
show "P (Suc n)" sorry
next
case 2
note B (Suc n) and C (Suc n)
show "Q (Suc n)" sorry
}
qed
I can think of two solutions, one of which you already discovered:
In fact, playing with examples shows that
lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...x0...) ( the fact "P x0" is not known here )
case 1 have j:"P x0" by fact
show "Q1 x0" proof (... j ...)
case 2 show "Q2 x0" proof (... j ...) ( why is j in scope here? )works. I don't understand the scoping of facts in this example.
By omitting the "next" between subcases 1 and 2, Isabelle doesn't
reset the proof context, so "j" is still in scope. This technique
wouldn't work for my example above though, since when you use two
"case" commands without using "next" in between, you get a proof
context that is essentially the union of the two cases. Here the
second subcase fails because too many assumptions are in scope.
lemma
fixes n :: nat
assumes "C n"
shows "A n ==> P n"
and "B n ==> Q n"
using C n
proof (induct n)
case (Suc n)
case 1
note A (Suc n) and C (Suc n)
show "P (Suc n)" sorry
case 2
note C (Suc n) and C (Suc n)
show "Q (Suc n)" (*** error because assumption A (Suc n) is
still in scope ***)
Solution 2: If the "case" command doesn't make the necessary
assumptions early enough for you, you can always "assume" them
yourself, like this:
lemma
fixes n :: nat
assumes "C n"
shows "A n ==> P n"
and "B n ==> Q n"
using C n proof (induct n)
case 0
{
case 1 note A 0 show "P 0" sorry
next
case 2 note B 0 show "Q 0" sorry
}
next
case (Suc n)
assume foo: "C (Suc n)"
from foo have bar: ...
{
case 1
note A (Suc n)
show "P (Suc n)" using bar sorry
next
case 2
note B (Suc n)
show "Q (Suc n)" using bar sorry
}
qed
The validity of this might make a bit more sense if you remember that
the "case" command is essentially syntactic sugar for a bunch of "fix"
and "assume" commands. Whenever you do a "show" command, Isar only
requires that the assumptions in scope are a subset of the ones in the
goal you are trying to solve.
Hope this helps,
Email Gateway (Aug 18 2022 at 17:42):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Thanks Brian,
You understood the question as I meant it. I consider it a weakness
that the fact C (Suc n) is not in scope where it logically should
be. Of the two solutions you suggest, the one I first discovered is
illogical, and the second one you point out is less comfortable for
the user because the assumption isn't checked by Isabelle at the point
it is introduced. Due to the profusion of renamed variables under the
"case" it is easy to misstate such assumptions.
Best,
Randy
Email Gateway (Aug 18 2022 at 17:42):From: Makarius <makarius@sketis.net>
On Sun, 15 May 2011, Randy Pollack wrote:
In the following example (taken from
~~/src/HOL/Induct/Common_Patterns.thy) there is apparently unnecessary
duplication.lemma
fixes n :: nat
shows "P n" and "Q n"
proof (induct n)
case 0 case 1
show "P 0" sorry
next
case 0 case 2
show "Q 0" sorry
next
case (Suc n) case 1
note hyps =P nQ n(** this line ... **)
show "P (Suc n)" sorry
next
case (Suc n) case 2
note hyps =P nQ n(** ... duplicated *)
show "Q (Suc n)" sorry
qedI want to know how to avoid this duplication.
First of all, the boundaries of nested cases are determined by the
"induct" method. Further refinement of this behaviour is on the TODO list
for several years, but that method has accumulated so many features
already, that it takes a long time to clear it out again.
Given the current behaviour there are still many ways how to express the
proof. The "Common_Patterns" are just some examples to explain the main
ideas. E.g. the above duplication of "P n" and "Q n" as propositions can
be avoided by using the fact names produced by each case, i.e. "Suc",
"Suc.hyps", "Suc.prems". You can also project from there using syntax
such as "Suc(2)" although such numbers make proofs a bit hard to read and
maintain.
In fact, playing with examples shows that
lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...x0...) ( the fact "P x0" is not known here )
case 1 have j:"P x0" by fact
show "Q1 x0" proof (... j ...)
case 2 show "Q2 x0" proof (... j ...) ( why is j in scope here? )works. I don't understand the scoping of facts in this example.
This is another example why it is a bad idea to invent new Isar
indentation rules on the spot. The indentation that is hard-wired into
Proof General is quite precise approximation of important semantic aspects
of the language. In particular, the 'case' command merely augments the
context monotonically, without introducing any block structure on its own.
So no change of indentation here.
I've also made a mistake many years ago in calling it 'case' in the first
place, which sounds too much like a rigid structure in corellation with
the goal state, which it isn't.
To understand Isar block structure in general, you can always use { ... }
explicitly, but in practice it is usually suppressed due to the following
implicit principles -- using ( ... ) for the true internal parantheses
that do not have concrete syntax:
(1) a proof body opens an extra pair of spare parentheses like this:
(
have A
(
proof method
body
qed method
)
)
(2) concrete user commands are defined as follows:
{ == ((
} == ))
next == )(
More precisely
next == ) note nothing (
which explains why you cannot push results over that boundary.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC