I have a nested inductive type along with a recursive program on it, defined using a `where`

clause and a subprogram to handle the nesting. Now I'm trying to prove some theorem on it, but for the nested object that theorem is expressed using the subprogram's return value. The subprogram appears to be hidden, and according to the documentation `where`

clauses are elaborated as `let`

bindings inside the main function. How should I go to reason about that subprogram?

Silly example:

```
From Coq Require Import List.
From Equations Require Import Equations.
Import ListNotations.
Inductive NaryTree (α: Type): Type :=
| Leaf
| Node (children: list (NaryTree α)).
Arguments Leaf {α}.
Arguments Node {α} (_).
Equations NaryTree_map {α β} (f: α -> β) (t: NaryTree α): NaryTree β :=
NaryTree_map f Leaf := Leaf;
NaryTree_map f (Node children) := Node (NaryTree_mapchildren children)
where NaryTree_mapchildren (l: list (NaryTree α)): list (NaryTree β) :=
NaryTree_mapchildren [] := [];
NaryTree_mapchildren (t::l) := NaryTree_map f t :: NaryTree_mapchildren l.
Check NaryTree_mapchildren.
(* Error: The reference NaryTree_mapchildren was not found in the current environment. *)
```

pretty much every functional programming language semantics I've seen defines the meaning of a `let`

binding via substitution. This means the `let`

binding basically can't be called a subprogram in any meaningful sense, and can't be reasoned about separately

to my knowledge the bottom line is: reasoning in isolation about let bindings in Coq can't be done

Right, seems reasonable. Can I define `NaryTree_map`

and `NaryTree_mapchildren`

in any other way with equations so that they're two separate functions?

Why not just use regular `map`

?

```
Equations NaryTree_map {α β} (f: α -> β) (t: NaryTree α): NaryTree β :=
NaryTree_map f Leaf := Leaf;
NaryTree_map f (Node children) := Node (map (NaryTree_map f) children).
```

That would be ideal. My particular use case is with different higher-order functions on a dependent vector type though, and the recursive calls do not seem to be recognized, leading to usual "cannot guess the decreasing argument of fix messages". Are there any tricks to improve my chances here? I can make a MWE if needed.

"cannot guess decreasing arg" is usually a hint to switch to using explicit well-founded relations with Equations (`Equations ... by wf <expression> <rel> := ...`

)

doesn't sound like you would gain anything by defining the vector `map`

together with other function

Right, inlining the nested type is my gut reaction, but it is quite unsatisfying. Let me see if I can get the `wf`

option to work. I've tried to use the subterm relation as a first test below (not sure if it's good enough):

```
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Arguments vec_nil {α}.
Arguments vec_cons {α N}.
Equations Derive NoConfusion Subterm for vec.
Equations vec_map {N α β} (f: α -> β) (v: vec α N): vec β N :=
vec_map f vec_nil := vec_nil;
vec_map f (vec_cons a u) := vec_cons (f a) (vec_map f u).
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion Subterm for M.
Equations identity {R} (m: M R): M R by wf m M_subterm :=
identity (Ret r) := Ret r;
identity (Blocks blocks k) :=
Blocks (vec_map (fun b t => identity (b t)) blocks) (fun t => identity (k t)).
```

I get *"The carrier type of the recursion order cannot depend on the arguments"* though, and judging from the manual which has this example

```
Equations unzip {n} (v : vector (A × B) n) : vector A n × vector B n
by wf (signature pack v ) (@t subterm (A × B)) :=
```

It does seem on the surface that using `m`

could be legal. :thinking:

"signature pack v" isn't syntax I've seen (got a link?); but that + your error suggests the following trick: to ensure the carrier doesn't depend on earlier arguments, maybe the well-founded recursion could be defined on `{ R & M R }`

? "Signature pack" might be syntax to ask Equations to do this internally?

OTOH, if R is constant throughout the recursion, maybe you could declare it as a section parameter:

```
Section foo.
Context {R : Type}.
Equations identity (m : M R) ...
End foo.
```

Ok, I'm making progress. For "signature pack v", some underscores actually disappeared when I copied from the manual. The example reads

```
Equations unzip {n} (v : vector (A × B) n) : vector A n × vector B n
by wf (signature_pack v) (@t_subterm (A × B)) :=
```

where `t_subterm`

is from `Derive Subterm`

and `signature_pack`

is a generic `Equations`

function which connects to the signature obtained from `Derive Signature`

, and does what you suggested with the index. In my case `R`

isn't constant so the signature pack feels like the correct approach.

I've been trying to build a subterm relation, which seems to me like it should be straightforward by inlining the nested inductive. However deriving `Subterm`

leaves me with a basic `M_direct_subterm`

which ignores the sub-terms in the vector.

```
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion NoConfusionHom Subterm Signature for M vec.
Print M_direct_subterm. (* only one case for k *)
```

Can I get such a subterm relation automatically, or do I have to build it?

Indeed, Equations does not yet generate automatically the subterm relation for nested inductive types like M. You could either derive it yourself or write a `size`

function like the last example here http://mattam82.github.io/Coq-Equations/examples/Examples.mutualwfrec.html

However your definition of `identity`

is fine using structural recursion, you only need to define `vec_map`

in a section with `f : alpha -> beta`

as a parameter, so that the syntactic guard checking can recognize it.

This is a common problem, already with `list`

Thanks, this is exactly what I'd like to know more about. Could you elaborate just a bit? Setting `f`

as a `Variable`

in a section for `vec_map`

yields the same result, while setting it as a `Parameter`

makes it a free variable of `vec_map`

even outside the section (!).

Right, I should have said `Variable`

indeed. Once you have that the structural definition should go through

Cool, I should be close then. I do get obligations about the subterms in the vector though. Is that what you mean?

```
Inductive vec (α: Type): nat -> Type :=
| vec_nil: vec α 0
| vec_cons {N} (a: α) (u: vec α N): vec α (S N).
Arguments vec_nil {α}.
Arguments vec_cons {α N}.
Inductive M: Type -> Type :=
| Ret {R} (r: R): M R
| Blocks {R T} {N: nat} (blocks: vec (T -> M T) N) (k: T -> M R): M R.
Equations Derive NoConfusion NoConfusionHom Subterm Signature for vec M.
Section VecMap.
Variables (α β: Type) (f: α -> β).
Equations vec_map {N} (v: vec α N): vec β N :=
vec_map vec_nil := vec_nil;
vec_map (vec_cons a u) := vec_cons (f a) (vec_map u).
End VecMap.
Arguments vec_map {α β} (f) {N}.
Equations? identity {R} (m: M R): M R by wf (signature_pack m) M_subterm :=
identity (Ret r) := Ret r;
identity (Blocks blocks k) :=
Blocks (vec_map (fun b t => identity (b t)) blocks) (fun t => identity (k t)).
```

Try without the `wf`

annotation?

It appears to work with `Equations?`

. Great! Strangely with `Equations`

I get the following message

```
Obligation 1 of identity_graph_correct:
(forall (R : Type) (m : M R), identity_graph R m (identity m)).
Functional induction principle could not be proved automatically, it is left as an obligation.
```

But there is no obligation. :sweat_smile:

Ah yes, it's another limitation when working with nested inductive types, the elimination principle generation doesn't catch recursive calls under `vec_map`

You can use `#[derive(eliminator=no)] Equations`

to a avoid the generation and error

Right, I had to prove the induction principle manually in some other case. Well this is all very helpful, I think I can now go back to my code and make some progress. Thanks for the help!

Last updated: Jan 29 2023 at 14:02 UTC