## Stream: Coq users

### Topic: ✔ Nested recursion

#### James Wood (Sep 05 2022 at 12:33):

My example uses `Equations`, but I think the real issue is with Coq's `fix`. I've been looking through Examples.RoseTree for inspiration on how to handle nested recursion. I was surprised that there, nested recursion seems to "just work" -- for example, `size` does not require inlining of `list_size` to satisfy termination checking. Even `alt_size`, which there is written in inlined style, can be rewritten in terms of `map` and `list_max`. However, when I try to write a size function on a more complex data structure -- intrinsically typed STLC with n-ary functions -- I get the error `Cannot guess decreasing argument of fix.` (see working example below). So, what termination heuristics are being hit by the rose tree example but not my STLC example, and is there any way that I could hit them?

``````Require Import List.
Import ListNotations.
From Equations Require Import Equations.

Inductive env {A} {T : A -> Type} : list A -> Type :=
| enil : env []
| econs {x xs} : T x -> env xs -> env (x :: xs).
Arguments env {A} T xs.

Equations env_map {A} {S T : A -> Type} :
(forall x, S x -> T x) ->
(forall xs, env S xs -> env T xs) :=
| f, _, enil => enil
| f, _, econs s ss => econs (f _ s) (env_map f _ ss).

Equations list_of_env {A T xs} : @env A (fun _ => T) xs -> list T :=
| enil => []
| econs t ts => t :: list_of_env ts.

Inductive type : Type :=
| base
| func (Ga : list type) (A : type).

Inductive elem {X} {x : X} : list X -> Type :=
| ze {xs} : elem (x :: xs)
| su {y xs} : elem xs -> elem (y :: xs).
Arguments elem {X} x xs.

Inductive term (Ga : list type) : type -> Type :=
| var {A} : elem A Ga -> term Ga A
| app {De A} : term Ga (func De A) -> env (term Ga) De -> term Ga A
| lam {De A} : term (De ++ Ga) A -> term Ga (func De A).
Arguments var {Ga A} & e.
Arguments app {Ga De A} M & Ns.
Arguments lam {Ga De A} M.

Fail Equations size {Ga A} : term Ga A -> nat :=
| var _ => 0
| app M Ns => S (size M + list_sum (list_of_env (env_map (fun _ => size) _ Ns)))
| lam M => S (size M)
.
Equations size {Ga A} : term Ga A -> nat := {
| var _ => 0
| app M Ns => S (size M + total_size Ns)
| lam M => S (size M)
}
where total_size {Ga De} : env (term Ga) De -> nat := {
| enil => 0
| econs t ts => size t + total_size ts
}
.
``````

#### Li-yao (Sep 05 2022 at 12:41):

The trick in RoseTree is that in `list_size` the function `f` is introduced outside the `Fixpoint`.

#### Gaëtan Gilbert (Sep 05 2022 at 12:42):

the problem is probably env_map recursing with too much generality
consider

``````Inductive rose := Node (_:list rose).

Fixpoint map1 {A B} (f:A->B) l :=
match l with
| nil => nil
| cons x l => cons (f x) (map1 f l)
end.

Definition map2 {A B} (f:A->B) :=
fix map2 l :=
match l with
| nil => nil
| cons x l => cons (f x) (map2 l)
end.

Axiom sum : list nat -> nat.

Fail Fixpoint size t :=
match t with
| Node l => sum (map1 size l)
end.

Fixpoint size t :=
match t with
| Node l => sum (map2 size l)
end.
``````

`map2` is the same as stdlib List.map
it can also be defined as

``````Section S.
Context {A B} (f:A->B).
Fixpoint map2 l :=
match l with
| nil => nil
| cons x l => cons (f x) (map2 l)
end.
``````

so you can try defining env_map in sections with the arguments that are constant in the recursion pulled out as section variables to get equations to do the right thing.

#### James Wood (Sep 05 2022 at 12:46):

Aha, indeed, defining `env_map` in a section fixed it!

#### James Wood (Sep 05 2022 at 12:49):

So is the later `fix` doing some analysis of `map1`/`map2`/`env_map` that gets caught up when that earlier `fix`-expression is too complicated?

#### Gaëtan Gilbert (Sep 05 2022 at 12:54):

it does some reduction ending up with seeing

``````(fix map1 A B f l := ...) _ _ size l
``````

vs

``````(fix map2 l := ... size ...) l
``````

the information that `l` is a subterm of `t` is propagated through the fixes in both cases, but in the first case it still sees a not applied `size` so rejects it

#### Notification Bot (Sep 05 2022 at 12:56):

James Wood has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC