The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

To answer your practical question, this works:

Require Import Coq.Lists.List.
Import ListNotations.
Open Scope list_scope.
Inductive tree :=
| node (data : bool) (children : list_tree)
with list_tree :=
| nil
| cons (x : tree) (xs : list_tree).

Fixpoint nodesWithCont (nodes : list_tree): list (tree * list_tree)
  := match nodes with
     | nil => []
     | cons (node d children) tl
       => [(node d children, tl)] ++ nodesWithCont children ++ nodesWithCont tl
     end.

(Presumably you can use notations or coercions to make this not too unpleasant.)

As far as your theoretical question, I'm not aware of any such issues; I'd suggest opening a feature request and seeing what the devs say.

On Mon, Oct 26, 2020 at 7:19 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

It is surprising to me that in the fixpoint below, Coq cannot figure out that `children` is

a subterm of nodes. Theoretically, it seems that as long as a term is produced by peeling off one or more constructors (and doing nothing else), it should be considered a subterm. Are there some soundness or practicality issues in supporting such fixpoints?

Meanwhile, is there a way to write the fixpoint below without complicating the definition too much?

Require Import Coq.Lists.List.
Import ListNotations.

Inductive tree :=
| node (data: bool) (children: list tree).

Fixpoint nodesWithCont (nodes: list tree): list (tree* list tree) :=
   match nodes with
   | [] => []
   | (node d children)::tl =>  [(node d children, tl)] ++ (nodesWithCont children)++
                                                       nodesWithCont tl
   end.

Error: Recursive call to nodesWithCont has principal argument equal to "children" instead of

"tl".

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/