Stream: Beginner Questions

Topic: inductive definition fails

Jakob Schulz (Apr 06 2025 at 17:54):

Hi :)

I have an inductive definition of the following form:

definition P where "P ≡ undefined"

fun f :: "'a ⇒ nat" where "f x = undefined"

lemma "P a b ⟹ f a < f b"
  sorry

inductive i where
"f a = 0 ⟹ i a"
| "P a b ⟹ ¬ i a ⟹ i b"

Isabelle now failes at the inductive definition:

Proof failed.
 1. ⋀x y xa a b. x (?x24 x y xa a b) ⟶ y (?x24 x y xa a b) ⟹ y a ⟶ x a
The error(s) above occurred for the goal statement⌂:
mono (λp x. (∃a. x = a ∧ f a = 0) ∨ (∃a b. x = b ∧ P a b ∧ ¬ p a))

When I change the "¬ i a" to "i a", the definition succeeds. Does someone have an idea why this could be?

Many thanks in advance :)

Mathias Fleury (Apr 06 2025 at 18:13):

It seems to be only the generation of the simplification theorem

Mathias Fleury (Apr 06 2025 at 18:14):

This already triggers it:

inductive j :: ‹nat ⇒ bool› where
 ‹j (Suc b)› if  ‹¬j b›

Mathias Fleury (Apr 06 2025 at 18:14):

You should probably report that on the mailing list

Mathias Fleury (Apr 06 2025 at 18:15):

Mathias Fleury said:

It seems to be only the generation of the simplification theorem

However, I am actually not sure that it is possible to generate those theorems

Jan van Brügge (Apr 06 2025 at 22:03):

Isn't the problem here that these rules are not monotonic? There is no fixpoint (and thus no inductive predicate) of the rules if they are not monotonic

Jakob Schulz (Apr 07 2025 at 13:48):

Thank you for your responses!

Then it seems that an inductive definition might not be the correct choice here. I'm going to use a normal functioninstead:

function i where
"i a = ((f a = 0) ∨ (∃b. P b a ∧ i b))"
  by simp_all

Mathias Fleury (Apr 07 2025 at 13:50):

Don't forget to prove termination of this

Jakob Schulz (Apr 07 2025 at 13:54):

Mathias Fleury said:

Don't forget to prove termination of this

Oh, I thought this would only be required if I actually evaluate the function? :sweat_smile:

I would not know how to do a termination proof in this case...the type of b is infinite, but there are only finitely many b that satisfy P b a (and they all satisfy f b < f a by the lemma).

Mathias Fleury (Apr 07 2025 at 13:55):

Oh, I thought this would only be required if I actually evaluate the function?

Or prove anything about it

Mathias Fleury (Apr 07 2025 at 13:58):

Jakob Schulz said:

I would not know how to do a termination proof in this case...the type of b is infinite, but there are only finitely many b that satisfy P b a (and they all satisfy f b < f a by the lemma).

That sounds too weak to me. It should be possible to make it loop by having f 0 calling f 1 and f 1 calling f 0

Mathias Fleury (Apr 07 2025 at 14:03):

Mathias Fleury said:

Oh, I thought this would only be required if I actually evaluate the function?

Or prove anything about it

Okay, in some cases you can get away with not proving termination, but having only termination on local fragments. But you need termination to even be able to unfold the definition.

Last updated: Apr 18 2025 at 20:21 UTC