Nested recursion and `Program Fixpoint` or `Function`

I’d like to define the following function using Program Fixpoint or Function in Coq:

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.

Inductive Tree := Node : nat -> list Tree -> Tree.

Fixpoint height (t : Tree) : nat :=
  match t with
   | Node x ts => S (fold_right Nat.max 0 (map height ts))
  end.

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map (fun t => mapTree f t) ts)
  end.
Next Obligation.

Unfortunately, at this point I have a proof obligation height t < height (Node x ts) without knowing that t is a member of ts.

Similarly with Function instead of Program Fixpoint, only that Function detects the problem and aborts the definition:

Error:
the term fun t : Tree => mapTree f t can not contain a recursive call to mapTree

I would expect to get a proof obligation of In t ts → height t < height (Node x ts).

Is there a way of getting that that does not involve restructuring the function definition? (I know work-arounds that require inlining the definition of map here, for example – I’d like to avoid these.)

Isabelle

To justify that expectation, let me show what happens when I do the same in Isabelle, using the function command, which is (AFAIK) related to Coq’s Function command:

theory Tree imports Main begin

datatype Tree = Node nat "Tree list"

fun height where
  "height (Node _ ts) = Suc (foldr max (map height ts) 0)"

function mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"
by pat_completeness auto

termination
proof (relation "measure (λ(f,t). height t)")
  show "wf (measure (λ(f, t). height t))" by auto
next
  fix f :: "nat ⇒ nat" and x :: nat  and ts :: "Tree list" and t
  assume "t ∈ set ts"
  thus "((f, t), (f, Node x ts))  ∈ measure (λ(f, t). height t)"
    by (induction ts) auto
qed

In the termination proof, I get the assumption t ∈ set ts.

Note that Isabelle does not require a manual termination proof here, and the following definition works just fine:

fun mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"

This works because the map function has a “congruence lemma” of the form

xs = ys ⟹ (⋀x. x ∈ set ys ⟹ f x = g x) ⟹ map f xs = map g ys

that the function command uses to find out that the termination proof only needs to consider t ∈ set ts..

If such a lemma is not available, e.g. because I define

definition "map' = map"

and use that in mapTree, I get the same unprovable proof obligation as in Coq. I can make it work again by declaring a congruence lemma for map', e.g. using

declare map_cong[folded map'_def,fundef_cong]

Solution

In general, it might be advisable to avoid this problem. But if one really wants to obtain the proof obligation that Isabelle gives you, here is a way:

In Isabelle, we can give an external lemma that stats that map applies its arguments only to members of the given list. In Coq, we cannot do this in an external lemma, but we can do it in the type. So instead of the normal type of map

forall A B, (A -> B) -> list A -> list B

we want the type to say “f is only ever applied to elements of the list:

forall A B (xs : list A), (forall x : A, In x xs -> B) -> list B

(It requires reordering the argument so that the type of f can mention xs).

Writing this function is not trivial, and I found it easier to use a proof script:

Definition map {A B} (xs : list A) (f : forall (x:A), In x xs -> B) : list B.
Proof.
  induction xs.
  * exact [].
  * refine (f a _ :: IHxs _).
    - left. reflexivity.
    - intros. eapply f. right. eassumption.
Defined.

But you can also write it “by hand”:

Fixpoint map {A B} (xs : list A) : forall (f : forall (x:A), In x xs -> B), list B :=
  match xs with
   | [] => fun _ => []
   | x :: xs => fun f => f x (or_introl eq_refl) :: map xs (fun y h => f y (or_intror h))
  end.

In either case, the result is nice: I can use this function in mapTree, i.e.

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map ts (fun t _ => mapTree f t))
  end.
Next Obligation.

and I don’t have to do anything with the new argument to f, but it shows up in the the termination proof obligation, as In t ts → height t < height (Node x ts) as desired. So I can prove that and define mapTree:

  simpl.
  apply Lt.le_lt_n_Sm.
  induction ts; inversion_clear H.
  - subst. apply PeanoNat.Nat.le_max_l.
  - rewrite IHts by assumption.
    apply PeanoNat.Nat.le_max_r.
Qed.

It only works with Program Fixpoint, not with Function, unfortunately.