Nested recursion and `Program Fixpoint` or` Function`

Question

I 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 (fx) (map (fun t => mapTree ft) ts) end. Next Obligation. 

Unfortunately, at the moment I have proof of commitment height t < height (Node x ts) , not knowing that t is a member of ts .

Similarly to Function instead of Program Fixpoint , only Function detects a problem and cancels the definition:

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

I would expect to receive an evidentiary obligation In t ts → height t < height (Node x ts) .

Is there a way to get something that is not related to restructuring a function definition? (I know workarounds that require nesting a map definition here, for example, - Id to avoid this.)

Isabelle

To live up to this expectation, let me show you what happens when I do the same in Isabelle using the Function command, which (AFAIK) is associated with the Coqs 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 (fx) (map (λ t. mapTree ft) 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 proof of the end, I get the assumption t ∈ set ts .

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

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

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

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

that the Function command uses to find out that proof of completion only needs to be considered t ∈ set ts ..

If such a lemma is not available, for example, because I define

 definition "map' = map" 

and using this in mapTree , I get the same unforgivable proof as in Coq. I can get it to work again by declaring a congruence lemma for map' , for example. using

 declare map_cong[folded map'_def,fundef_cong] 

Answer 1

In general, it would be advisable to avoid this problem. But if someone really wants to get the proof that Isabelle gives you, here is a way:

In Isabella, we can give an external lemma that describes that map applies its arguments only to members of a given list. In Coq, we cannot do this in an external lemma, but we can do this in type. Therefore, instead of the normal card type

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

we want the type to say: " f applies only to list items:

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

(Requires reordering the argument so that type f can specify xs ).

Writing this function is not trivial, and it was easier for me to use a proof script:

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

But you can also write it "manually":

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

In any case, the result is good: 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 (fx) (map ts (fun t _ => mapTree ft)) end. Next Obligation. 

and I don’t have to do anything with the new argument f , but it appears in the mandatory completion requirement, like In t ts → height t < height (Node x ts) as desired. Therefore, I can prove it 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 Function , unfortunately.

Answer 2

In this case, you do not need a reasonable recursion in its complete generality:

 Require Import Coq.Lists.List. Set Implicit Arguments. Inductive tree := Node : nat -> list tree -> tree. Fixpoint map_tree (f : nat -> nat) (t : tree) : tree := match t with | Node x ts => Node (fx) (map (fun t => map_tree ft) ts) end. 

Coq can independently calculate that map_tree recursive calls map_tree made on strict subtopics. However, it is difficult to prove anything about this function, since the induction principle generated for tree is not useful:

 tree_ind : forall P : tree -> Prop, (forall (n : nat) (l : list tree), P (Node nl)) -> forall t : tree, P t 

This is essentially the same problem you mentioned earlier. Fortunately, we can fix the problem by proving our own principle of induction with proof.

 Require Import Coq.Lists.List. Import ListNotations. Unset Elimination Schemes. Inductive tree := Node : nat -> list tree -> tree. Set Elimination Schemes. Fixpoint tree_ind (P : tree -> Prop) (IH : forall (n : nat) (ts : list tree), fold_right (fun t => and (P t)) True ts -> P (Node n ts)) (t : tree) : P t := match t with | Node n ts => let fix loop ts := match ts return fold_right (fun t' => and (P t')) True ts with | [] => I | t' :: ts' => conj (tree_ind P IH t') (loop ts') end in IH n ts (loop ts) end. Fixpoint map_tree (f : nat -> nat) (t : tree) : tree := match t with | Node x ts => Node (fx) (map (fun t => map_tree ft) ts) end. 

The Unset Elimination Schemes command prevents Coq from generating its default induction principle (and not useful) for tree . The entry of fold_right in the induction hypothesis simply expresses that the predicate P holds for every tree t' appearing in ts .

Here is a statement that you can prove with this induction principle:

 Lemma map_tree_comp fgt : map_tree f (map_tree gt) = map_tree (fun n => f (gn)) t. Proof. induction t as [n ts IH]; simpl; f_equal. induction ts as [|t' ts' IHts]; try easy. simpl in *. destruct IH as [IHt' IHts']. specialize (IHts IHts'). now rewrite IHt', <- IHts. Qed. 

Answer 3

Now you can do this using equations and get the correct elimination principle automatically using structural nested recursion or reasonable recursion