Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] inductive_set and ordinal induction

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,

after investigating a little, I learned that inductive_set builds on
inductive.

The same question applies to inductive: For an inductive predicate X,
can I somehow get an induction schema like
"[| ... |] ==> P X"
as opposed to
"[| X x; ... |] ==> P x"
?

If there is no way to get this automatically, is there maybe a way to
access the monotonicity rule of an inductive predicate, so that I can
apply lfp_ordinal_induct?

Christoph

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Tobias Nipkow <nipkow@in.tum.de>
Hopefully one can get access to the monotonicity theorem proved internally in
the cause of an inductive definition. But I don't know how. It is not called
X_mono or X.mono. In the worst case it is hidden...

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Indeed, inductive does not bind the monotonicity theorem to a theorem name and so the
monotonicity theorem is not accessible from user space. Moreover, the monotonicity prover
is not exported in the ML interface either, so you cannot even state the monotonicity
theorem yourself and have the monotonicity prover solve the goal once more.

Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Tobias Nipkow <nipkow@in.tum.de>
Bummer! Is there any reason not to make the monotonicity theorem availble in
user space? If not...

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
No, I'd be glad if it was made available. Probably nobody ever invested the time to adapt
the code base.

Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:35):

From: Stefan Berghofer <berghofe@in.tum.de>
Hi all,

monotonicity and similar theorems are not made available to the user because this would expose
the inner workings of the inductive definition package, which can change without prior notice.
For a more detailed discussion of this problem, see e.g. this thread:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-May/msg00079.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-June/msg00013.html

Greetings,
Stefan

view this post on Zulip Email Gateway (Aug 22 2022 at 11:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Stefan,

You are right in that the rules generated by the inductive package suffice for proving.
However, sometimes it is easier to prove some statement using a higher-level reasoning
principle than with the point-wise rules for inductive predicates. Thus, there may be
cases where it is easier to derive a property from the internal construction than from
what is exposed. Most of the other Isabelle packages I know follow the same principle: the
internal constructions are accessible, but normally not used. If anyone uses the internal
constructions, it is obvious that the proofs will break if the implementation is changed.

For comparison, partial_function also exposes the internal definition and the monotonicity
theorem and I actually use this frequently to derive better induction rules for my
functions. In principle, such rules could be derived from the induction rule provided, but
I would have to do the derivation for each function. By using the internal derivation, I
can do the derivation once and just instantiate the appropriate lemma. Of course, I know
that I have to change my proofs when partial_function changes, but as I am using the
internal definition only in a principled way, the required adaptations should also be
canonical.

Something similar can also be useful for the inductive package, as this request shows.

From what I saw in the Isabelle repository, this distinction between official and
internal theorems might be more explicit in the next release. The internal theorems are
only made available if a specific attribute is set at definition time. Something similar
could also be done for inductive.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:35):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
I don't see how ordinal induction (like lfp_ordinal_induct)
"[| ... |] ==> P X"
is derivable from the pointwise induction rule
"[| X x; ... |] ==> P x"
provided by the inductive package.

Or is it derivable?

Best,
Christoph

view this post on Zulip Email Gateway (Aug 22 2022 at 11:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Christoph,

The general answer first:
The rules generated by the inductive package suffice to prove that the predicate equals
the internal construction. Thus, you can prove the same as you can prove with access the
internal construction. However, this proof of equivalence can be quite tedious (which is
why I support making the internal construction accessible).

In the specific case of lfp_ordinal_induct, you just have to look at its proof. It uses
three properties of lfp and f:

  1. Monotonicity of f: You have to prove this yourself manually, but this is doable.
  2. lfp_unfold: This corresponds to X.simps[abs_def]
  3. lfp_lowerbound: This corresponds to X.induct

Hope this helps,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:35):

From: Johannes Hölzl <hoelzl@in.tum.de>
Dear Christoph,

the prove using lfp_ordinal_induct is quite different, the inductive
package does not produce it for you.

As Andreas points out, you can directly use the definition of the
predicate (<inductive pred>_def) and then manually prove monotonicity.
Then you can apply lfp_ordinal_induct.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:36):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Dear Johannes,

thank you, and also Andreas for your answers.

<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>".
Can I somehow bind <something_very_long> to a name so that I do not need
to copy&paste it?

I tried pattern matching like
note X_def (is "_ == lfp ?f")
but this doesn't work (the isar manual agrees).

Is <inductive_pred>_def considered part of the stable interface to the
inductive package? If not, maybe my approach of redefining the
inductive predicate explicitly via lfp and proving equality could be
more robust against changes in the inductive package?

Best,
Christoph

view this post on Zulip Email Gateway (Aug 22 2022 at 11:36):

From: Johannes Hölzl <hoelzl@in.tum.de>
As far as I understood Stefan, the _def theorems are actually internal.

I think you should be on the save side with your last suggestion, i.e.
defining the functional F_def and then prove:

inductive X ...

definition F where
"F = ..."

lemma "X = lfp F"
unfolding X_def F_def by simp

Then you should be on the save side if we change the internals of the
inductive package.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:36):

From: Tobias Nipkow <nipkow@in.tum.de>
On 27/10/2015 16:16, Johannes Hölzl wrote:

As far as I understood Stefan, the _def theorems are actually internal.

But it is exported, and hasn't changed over many years and I don't see any
impending change there either.

Tobias

I think you should be on the save side with your last suggestion, i.e.
defining the functional F_def and then prove:

inductive X ...

definition F where
"F = ..."

lemma "X = lfp F"
unfolding X_def F_def by simp

Then you should be on the save side if we change the internals of the
inductive package.

- Johannes

Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:

Dear Johannes,

thank you, and also Andreas for your answers.

On 10/27/2015 02:26 PM, Johannes Hölzl wrote:

As Andreas points out, you can directly use the definition of the
predicate (<inductive pred>_def) and then manually prove monotonicity.
Then you can apply lfp_ordinal_induct.

<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>".
Can I somehow bind <something_very_long> to a name so that I do not need
to copy&paste it?

I tried pattern matching like
note X_def (is "_ == lfp ?f")
but this doesn't work (the isar manual agrees).

Is <inductive_pred>_def considered part of the stable interface to the
inductive package? If not, maybe my approach of redefining the
inductive predicate explicitly via lfp and proving equality could be
more robust against changes in the inductive package?

Best,
Christoph

smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 11:36):

From: Tobias Nipkow <nipkow@in.tum.de>
On 27/10/2015 16:16, Johannes Hölzl wrote:

As far as I understood Stefan, the _def theorems are actually internal.

I think you should be on the save side with your last suggestion, i.e.
defining the functional F_def and then prove:

inductive X ...

definition F where
"F = ..."

lemma "X = lfp F"
unfolding X_def F_def by simp

Then you should be on the save side if we change the internals of the
inductive package.

No, you are not: the simp proof may well fail if X_def changes, and if it
disappears altogether the unfolding breaks.

Tobias

- Johannes

Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:

Dear Johannes,

thank you, and also Andreas for your answers.

On 10/27/2015 02:26 PM, Johannes Hölzl wrote:

As Andreas points out, you can directly use the definition of the
predicate (<inductive pred>_def) and then manually prove monotonicity.
Then you can apply lfp_ordinal_induct.

<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>".
Can I somehow bind <something_very_long> to a name so that I do not need
to copy&paste it?

I tried pattern matching like
note X_def (is "_ == lfp ?f")
but this doesn't work (the isar manual agrees).

Is <inductive_pred>_def considered part of the stable interface to the
inductive package? If not, maybe my approach of redefining the
inductive predicate explicitly via lfp and proving equality could be
more robust against changes in the inductive package?

Best,
Christoph

smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 11:36):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
I was thinking more of something like the proof of X_lfp_equiv I posted
in my original posting, without using X_def.

The only drawback is that I need to state the monotone function twice in
slightly different form, once for the inductive predicate and once again
to redefine it with lfp.

Best,
Christoph

view this post on Zulip Email Gateway (Aug 22 2022 at 11:37):

From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 27.10.2015, 16:33 +0100 schrieb Tobias Nipkow:

lemma "X = lfp F"
unfolding X_def F_def by simp

Then you should be on the save side if we change the internals of the
inductive package.

No, you are not: the simp proof may well fail if X_def changes, and if it
disappears altogether the unfolding breaks.

Okay, I should be more specific with safe side: You only need to perform
local changes. You need to adapt your proof only locally, only this
proof.

If you would sprinkle X_def all over the place and inductive changes it,
you can _not_ overwrite X_def like

lemma X_def: "X = lfp ..."

as Isabelle does not allow the same theorem name in one theory.

Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:

Dear Johannes,

thank you, and also Andreas for your answers.

On 10/27/2015 02:26 PM, Johannes Hölzl wrote:

As Andreas points out, you can directly use the definition of the
predicate (<inductive pred>_def) and then manually prove monotonicity.
Then you can apply lfp_ordinal_induct.

<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>".
Can I somehow bind <something_very_long> to a name so that I do not need
to copy&paste it?

I tried pattern matching like
note X_def (is "_ == lfp ?f")
but this doesn't work (the isar manual agrees).

Is <inductive_pred>_def considered part of the stable interface to the
inductive package? If not, maybe my approach of redefining the
inductive predicate explicitly via lfp and proving equality could be
more robust against changes in the inductive package?

Best,
Christoph

view this post on Zulip Email Gateway (Aug 22 2022 at 11:37):

From: Johannes Hölzl <hoelzl@in.tum.de>
Yes, it should be considered fixed, and I support Andreas' idea of
exporting the monotonicity theorem.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:38):

From: Tobias Nipkow <nipkow@in.tum.de>
Stefan, you could call it something like mono_internal, thus expressing that it
may change.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 11:45):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,

I would like to use lfp_ordinal_induct_set with inductive_set.

When I define:

inductive_set X where "⟦ ⋀b. f a b ⟹ b ∈ X ⟧ ⟹ a ∈ X"

I get an induction theorem X.induct for free. However, X.induct talks
about elements, not sets. The following induction schema based on least
fixed points also works:

lemma X_lfp_induct:
assumes step: "⋀S. P S ⟹ P (S ∪ {a. ∀b. f a b ⟶ b ∈ S})"
and union: "⋀M. ∀S ∈ M. P S ⟹ P (⋃M)"
shows "P X"
oops

I managed to prove X_lfp_induct (see attachment) by redefining X
manually via the lfp function and then showing that this definition is
equivalent to the inductive_set. Then X_lfp_induct follows from
lfp_ordinal_induct_set from ~~/src/HOL/Inductive.thy.

For this I needed to prove things like monotonicity, which I assume
inductive_set already proves internally. So my approach seems a little
redundant and I think there could be a better way.

Is there an easier way to get a least fixed point induction schema like
this for inductive_sets in general, maybe even fully automatic?

Thanks,
Christoph
lfp.thy

view this post on Zulip Email Gateway (Aug 22 2022 at 11:53):

From: Makarius <makarius@sketis.net>
A few notes on these questions about internal construction vs. external
results (or "interface") of derived definitional packages.

In conclusion, this is the relevant NEWS entry from Isabelle/ca53150406c9,
which is meant for the coming release:

* Inductive definitions ('inductive', 'coinductive', etc.) expose
low-level facts of the internal construction only if the option
"inductive_defs" is enabled. This refers to the internal predicate
definition and its monotonicity result. Rare INCOMPATIBILITY.

* Recursive function definitions ('fun', 'function', 'partial_function')
expose low-level facts of the internal construction only if the option
"function_defs" is enabled. Rare INCOMPATIBILITY.

This means the new situation is both more restrictive and more permissive.

There was also a discussion about the "stability of interfaces" in
Isabelle. It does not really exist. Everything may change at some point.
Of course, we don't change things at will, according to current weather
conditions. But we are still moving conceptually forward to a hopefully
better system.

A recent example for that is the upheaval of the 'datatype' package after
many years.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC