Proving nonexistence of inductive fixpoints?

Stream: lean4

[Andrés Goens]

I'm trying to figure out how to prove that a term that I cannot construct a term that would be some sort of (coinductive?) fixpoint of an inductive term. The catch is that the recursion is 'hidden' by a function term. Something like this:

inductive Object
  | mk : (subobjects : Nat → Option Object) → Object

def Object.subobjects : Object → Nat → Option Object
  | .mk sub => sub

theorem no_suboject_self : ∀ o : Object, ¬∃ n, o.subobjects n = some o := sorry

I'm sure there's some nice type-theoretic background to this that I don't have :sweat_smile: can someone here maybe help me out, how would I prove something like no_subobject_self?

(BTW: I posted this here since I'm working with Lean4, but happy to move it if it makes more sense in a different stream)

[Mario Carneiro]

Unfortunately that's a really bad combination of features for lean right now. induction doesn't support nested inductives, and well founded recursion doesn't support inductives with rank higher than omega (in your case, this is caused by the (Nat -> T) -> T style constructor

[Mario Carneiro]

You can do it but you basically have to construct the proof term manually