The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Alternatively, if you don't want to change the definition of [tree], you can make your fixpoint recursive on the tree type rather than the list type:

Require Import Coq.Lists.List.
Import ListNotations.
Open Scope list_scope.
Inductive tree :=
| node (data : bool) (children : list tree).

(* put this in a section so the guard checker can see through through the fixpoint by inlining [f] into the body before doing guard checking *)

Section flat_map_with_tl.
  Context {A B : Type} (f : A -> list A -> list B).
  Fixpoint flat_map_with_tl (l : list A) : list B
    := match l with
       | [] => []
       | x :: t => f x t ++ flat_map_with_tl t
       end.
End flat_map_with_tl.

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

On Mon, Oct 26, 2020 at 8:17 PM Jason Gross <jasongross9 AT gmail.com> wrote:

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/