Counting applications of a function

Stream: Is there code for X?

[Peter Nelson]

I would like to talk about an ENat-valued parameter measuring the number of times a function needs to be applied until some property holds, and then to prove an obvious fact about this definition.

Is there API for anything like this, or a good way to golf the proof below? If not, is this worth a PR? The code feels like I'm going against the grain.

import Mathlib.Data.ENat.Lattice

variable {α : Type*}

/--  Given a function from `f : α → α` and a predicate `P : α → Prop`,
the minimum number of iterations of `f` required to make `a : α` satisfy `P`,
or `⊤` if no number suffices. -/
noncomputable def depth (f : α → α) (P : α → Prop) (a : α) : ℕ∞ :=
  sInf ((↑) '' {i | P (f^[i] a)})

/-- If `d : α → ℕ∞` is a 'weight' function that drops by one whenever `f` is applied to an element
of nonzero weight, then `d` is equal to the `depth` for the property that `d = 0`. -/
lemma foo {f : α → α} (d : α → ℕ∞) (hdf : ∀ a, d a ≠ 0 → d a = d (f a) + 1) {a : α} :
    depth f (fun a ↦ d a = 0) a = d a := by
  refine le_antisymm ?_ (le_sInf ?_)
  · generalize hk : d a = k
    cases k with
    | top => simp
    | coe k =>
    · suffices d (f^[k] a) = 0 from sInf_le <| by simpa
      induction k generalizing a with
      | zero => simpa using hk
      | succ n IH =>
      · apply IH
        rwa [hdf _ (by simp [hk]), Nat.cast_add, Nat.cast_one,
          WithTop.add_right_inj (by simp)] at hk
  suffices ∀ k, d (f^[k] a) = 0 → d a ≤ k by simpa
  intro k hk
  induction k generalizing a with
  | zero => simpa using hk
  | succ n IH =>
  · simp at hk
    obtain h0 | hne := eq_or_ne (d a) 0
    · simp [h0]
    grw [hdf _ hne, IH hk, Nat.cast_add, Nat.cast_one]

[Peter Nelson]

As an aside, am I right in feeling like the syntax for induction has changed a lot recently? I can't find a way to avoid indenting, even when there is just one goal remaining.

[Edward van de Meent]

interestingly, you can do the following:

def depth' (f : α → α) (P : α → Prop) [DecidablePred P] (a : α) : ℕ∞ :=
  go a 0 where
  go a n := if P a then n else go (f a) (n + 1)
partial_fixpoint

[Edward van de Meent]

i'm not sure it gives the correct default value tho... i'm testing...

[Aaron Liu]

It looks like the default value is Classical.ofNonempty

[Aaron Liu]

so you can't prove anything about it :(

[Edward van de Meent]

/me is sad now :sad: