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
}
.
```

The trick in RoseTree is that in `list_size`

the function `f`

is introduced outside the `Fixpoint`

.

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.

Aha, indeed, defining `env_map`

in a section fixed it!

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?

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

James Wood has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC