Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with obtaining induction premises

Email Gateway (Aug 18 2022 at 09:39):

From: Vaidas Gasiunas <gasiunas@st.informatik.tu-darmstadt.de>
Hello,

Most of my Isabelle/Isar proofs are based on induction, and sometimes I
have problems when extracting the premises of the current inductive case,
something like:

lemma "?Q xs ==> ?P xs"
proof (induct xs)
case (Cons x xs) hence "?Q xs" by auto ...

Sometimes I can extract the premises with ".", but in the most of cases I
need to apply "auto". However, even this method is some cases does not
work. I attached a small test case which does not work. I use the build of
2006 Sep 12. Am I doing something wrong? If not, is there any workaround
for this?

Greetings,
Vaidas
Test.thy

Email Gateway (Aug 18 2022 at 09:40):

From: Makarius <makarius@sketis.net>
On Sat, 16 Sep 2006, Vaidas Gasiunas wrote:

I have problems when extracting the premises of the current inductive
case, something like:

lemma "?Q xs ==> ?P xs"
proof (induct xs)
case (Cons x xs) hence "?Q xs" by auto ...

Sometimes I can extract the premises with ".", but in the most of cases I
need to apply "auto".

Here the facts stemming from the Cons case consist of several things
simultaneously. The auto method silently ignores unused facts, while
single-step methods insist on being more thourough. This means a "."
proof has to be able to apply all given facts, which fails in the above
application.

You can try something like this to specify facts more precisely:

from Cons.hyps have "..." .

Another option is to retrieve premises out of the blue:

have "..." .

I use the build of 2006 Sep 12.

In that case you might want to read the NEWS file, which explains a few
additions to the induction setup, including common proof patterns. In
particular, the above from/have/. invocation can be replaced by

from ...

Note that your example in Test.thy will need a type constraint of
"!!ys :: 'a list. ..." here. This may change eventually, when the ...
notation becomes polymorphic.

Makarius

Email Gateway (Aug 18 2022 at 09:40):

From: Vaidas Gasiunas <gasiunas@informatik.tu-darmstadt.de>

Here the facts stemming from the Cons case consist of several things
simultaneously. The auto method silently ignores unused facts, while
single-step methods insist on being more thourough. This means a "."
proof has to be able to apply all given facts, which fails in the
above
application.

You can try something like this to specify facts more precisely:

from Cons.hyps have "..." .

I have tried following in my example:

from Cons.hyps have "!!ys. [| length zs = length ys; a \<in> set zs |]
==> !y. lookupEq zs ys a = Some y" .

It does not work, "by auto" does not help here either. At the end I
proved the lemma without explicifying the hypothesis, just by referring
to the fact Cons.hyps by its name. But I am still curious why "." or
"apply" cannot deal with such seemingly trivial step.

Another option is to retrieve premises out of the blue:

have "..." .

If I write

have "[| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs ys
a = Some y" .

then it works, but

have "!!ys. [| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq
zs ys a = Some y" .

does not work. But the latter is the hypothesis, which I see in the
context.

I use the build of 2006 Sep 12.

In that case you might want to read the NEWS file, which explains a
few
additions to the induction setup, including common proof patterns. In
particular, the above from/have/. invocation can be replaced by

from ...

Thanks, this can be very useful to make the proof more readable, because
now I invent a lot of fancy names to refer to the known facts.

Note that your example in Test.thy will need a type constraint of
"!!ys :: 'a list. ..." here. This may change eventually, when the
...
notation becomes polymorphic.

I don't know, but I somehow proved it without additional type
annotations.

Thanks,
Vaidas

Email Gateway (Aug 18 2022 at 09:40):

From: Makarius <makarius@sketis.net>
On Mon, 18 Sep 2006, Vaidas Gasiunas wrote:

I have tried following in my example:

from Cons.hyps have "!!ys. [| length zs = length ys; a \<in> set zs |]
==> !y. lookupEq zs ys a = Some y" .

It does not work, "by auto" does not help here either.

You also need a type constraints "!!ys :: 'a list. ..." here. Otherwise
this closed formula will be syntactically unrelated to the context of the
problem.

At the end I proved the lemma without explicifying the hypothesis, just
by referring to the fact Cons.hyps by its name.

This is a good strategy. It is usually easier (and more informative) to
derive immediate conclusions from the induction hypotheses, rather than
duplicate them literally.

But I am still curious why "." or "apply" cannot deal with such
seemingly trivial step.

Note that 'apply' merely applies a proof method. The "." abbreviates by this'', which can be expanded to apply this .'' The latter allows more
fine-grained debugging.

The single step methods (notably "this" and "rule") insist on being able
to apply all chained facts, without ignoring anything. Thus providing
excessive facts makes the method invocation fail.

This principle is important to achive some degree of robustness and
predictability of structured proof checking. In contrast, automated
methods readily ignore irrelevant facts. So it is easy to write proofs
that tell the wrong story, e.g. like this:

assume a: A
assume b: B

from a and b have C by auto

Here the ``auto'' step can ignore either a or b, or even worse ignore both
and use different facts declared in the context. The relevance of facts
is a fundamental problem in most automated proof tools.

If I write

have "[| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq zs ys
a = Some y" .

then it works, but

have "!!ys. [| length zs = length ys; a \<in> set zs |] ==> !y. lookupEq
zs ys a = Some y" .

does not work. But the latter is the hypothesis, which I see in the
context.

This is again a problem with unexpectedly general types. The first form
refers to the fixed variable ys of the context, i.e. gets the expected
type. The second is detached due to !! closure and gets a fresh type.

Makarius

Email Gateway (Aug 18 2022 at 09:41):

From: Vaidas Gasiunas <gasiunas@informatik.tu-darmstadt.de>
Indeed, when I write

from Cons.hyps have "!!(ys::'a list). [| length zs = length ys; a \<in>
set zs |] ==> !y. lookupEq zs ys a = Some y" .

then it works. Now I will know how to deal with such cases.

Thanks,
Vaidas

Last updated: Nov 21 2024 at 12:39 UTC