Structural Recursion Problem

Stream: lean4

[Marcus Rossel]

In the following, I feel like Lineage.container should be structurally recursive. Apparently it isn't though:

constant ID : Type _

-- A `Reactor` contains "things" identified by an `ID`. It also contains other `Reactor`s, thereby giving us a tree structure of reactors.
inductive Reactor
  | mk
    (things : ID → Option Nat)
    (nested : ID → Option Reactor)

-- Structure projections.
def Reactor.things : Reactor → ID → Option Nat     | mk t _ => t
def Reactor.nested : Reactor → ID → Option Reactor | mk _ n => n

-- A `Lineage` is supposed to express a "path" within a reactor tree.
-- E.g. a `Lineage rtr i` captures a path from the root reactor `rtr` to some thing identified by ID `i`.
inductive Lineage : Reactor → ID → Type _
  | thing {rtr i} : (∃ t, rtr.things i = some t) → Lineage rtr i
  | nested {rtr' i' rtr i} : (Lineage rtr' i) → (rtr.nested i' = some rtr') → Lineage rtr i

-- The `Lineage.container` function is supposed to return the reactor (along with its ID) that is the immediate parent of the thing reached by the lineage.
-- We therefore need to check "two steps deep":
def Lineage.container {rtr i} : Lineage rtr i → (Option ID × Reactor)
  -- If the lineage is still two or more "nestings" deep, perform a recursive call on the nested lineage.
  | .nested l@(.nested ..) _ => l.container
  -- If the lineage is nested only one layer deep, the nested lineage (`: Lineage rtr' i`) contains the thing identified by `i`.
  -- Therefore `rtr'` is the container, which in the context of `rtr` is identified by `i'`.
  | @nested rtr' i' .. => (i', rtr')
  -- If the lineage is not nested at all, we know that the root reactor `rtr` is the container, and we return no ID.
  | _ => (none, rtr)

On Lineage.container, Lean says:

fail to show termination for
  Lineage.container
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    container l

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

The formalization of Lineage has been giving me headaches in a couple of places now.
Would it be wise to change how it's formalized? If so, how?

[Gabriel Ebner]

This is related to https://github.com/leanprover/lean4/issues/501 (in the sense that @ does more than introduce an abbreviation for the subpattern)

[Gabriel Ebner]

The @ annotation has a lot of side effects.

[Gabriel Ebner]

It works if you remove the @:

-- The `Lineage.container` function is supposed to return the reactor (along with its ID) that is the immediate parent of the thing reached by the lineage.
-- We therefore need to check "two steps deep":
def Lineage.container {rtr i} : Lineage rtr i → (Option ID × Reactor)
  -- If the lineage is still two or more "nestings" deep, perform a recursive call on the nested lineage.
  | .nested (.nested x y) _ => container (.nested x y)
  -- If the lineage is nested only one layer deep, the nested lineage (`: Lineage rtr' i`) contains the thing identified by `i`.
  -- Therefore `rtr'` is the container, which in the context of `rtr` is identified by `i'`.
  | @nested rtr' i' .. => (i', rtr')
  -- If the lineage is not nested at all, we know that the root reactor `rtr` is the container, and we return no ID.
  | _ => (none, rtr)

[Marcus Rossel]

@Gabriel Ebner Thanks, that did the job!
I still have the following problem though, even after changing the definition of Lineage.container:

def Lineage.container {rtr i} : Lineage rtr i → (Option ID × Reactor)
  | .nested (.nested l h) _ => (Lineage.nested l h).container
  | @nested rtr' i' .. => (i', rtr')
  | _ => (none, rtr)

example {rtr : Reactor} {i} (h : ∃ t, rtr.things i = some t) : (Lineage.thing h).container = (none, rtr) := by
  simp [Lineage.container] -- failed to generate equality theorems for `match` expression `Lineage.container.match_1`
                           -- ...

I'm not sure if this is related to this topic, or if it's something completely different though.

[Leonardo de Moura]

@Marcus Rossel You can avoid the failure by avoiding the overlap between the first and second cases.

@[simp] def Lineage.container'' : Lineage rtr i → (Option ID × Reactor)
  | nested (nested l h) _ => (Lineage.nested l h).container''
  | nested (rtr := rtr') (i := i') (.thing h) _ => (i', rtr')
  | _ => (none, rtr)

We will try to improve the tactic used to prove the equations theorems, and make sure it can prove that the particular case in the error message is "unreachable".
You can use l@ notation if you provide additional annotations

@[simp] def Lineage.container : Lineage rtr i → (Option ID × Reactor)
  | nested l@h:(nested ..) _ => l.container
  | nested (rtr := rtr') (i := i') (thing h) _ => (i', rtr')
  | _ => (none, rtr)
termination_by _ r => sizeOf r
decreasing_by simp_wf; subst h; simp_arith

The h: at l@h:(nested ..) is instructing Lean to add a hypothesis h : l = nested ... I provided a custom decreasing_by to make sure this hypothesis is used. We will improve the default decreasing tactic.

[Leonardo de Moura]

@Marcus Rossel I pushed the two improvements described above. You can now write:

@[simp] def Lineage.container : Lineage rtr i → (Option ID × Reactor)
  | nested l@h:(nested ..) _ => l.container
  | @nested rtr' i' .. => (i', rtr')
  | _ => (none, rtr)

[Leonardo de Moura]

The h: annotation may look a bit weird because it looks like a dead variable, but it is used in the termination proof.

[Marcus Rossel]

It's now in nightly-2022-05-29. :tada:
Thanks so much Leo!