The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Lorenzo,

For fixpoints on nested inductive types, you must make sure to apply 
your function to a subterm. In your case, that means `depth` must end up 
applied to `br x` for any `x`.


>    Fixpoint depth (T : fmap_tree) : nat :=
>      match T with
>      | fmap_leaf n => 0
>      | fmap_node n br  => (maxn_f_codom id (fun x => depth (br x))).+1
>      end.


Now it is clear that the only location where `depth` is called 
recursively is in fact good. The exact rules are a little looser than 
that, but then you have to be aware of those rules and of the precise 
definition of every function that separates `depth` from `br`; it's not 
sufficient to understand what those functions do extensionally.

Cheers,
Li-yao

On 2/18/2021 1:32 PM, Lorenzo Gheri wrote:
> Hi All,
>
> I have defined the following datatype:
>
>    From mathcomp.ssreflect Require Import all_ssreflect.
>    From mathcomp Require Import finmap.
>    Open Scope fset.
>    Open Scope fmap.
>
>    Inductive fmap_tree :=
>    | fmap_leaf (n : nat)
>    | fmap_node (n : nat) (branching : {fmap nat -> fmap_tree}).
>
> I would really like to keep this definition, namely to use finite maps 
> (fmap from the math-comp libraries) instead of lists. I however run into 
> problems when defining depth:
>
>    Definition maxn_f_codom {A:Type} (f: A -> nat) (br: {fmap nat -> A}):=
>      foldr maxn 0 (map (fun x=> match (br.[?x]) with
>                                  | None => 0
>                                  | Some T' => f T'
>                                  end)
>             (enum_fset (domf br)) ).
>
>
>    Fixpoint depth (T : fmap_tree) : nat :=
>      match T with
>      | fmap_leaf n => 0
>      | fmap_node n br  => (maxn_f_codom depth br).+1
>      end.
>
> In particular the definition of maxn_f_codom above---which could as well 
> be inlined in the depth definition---is accepted by Coq with no issues, 
> but the Fixpoint for depth is ill-formed. I thought I could easily use 
> enum_fset for turning the finite domain of the fmap into a list and then 
> termination would have been guaranteed. I was being too naif! :)
>
> Before I give up altogether and go back to branching with lists, is 
> there any way for me to convince Coq that fmaps are OK as well?
>
> Many thanks,
> Lorenzo