The Coq mailing list

[Lorenzo Gheri <lor.gheri AT gmail.com>]

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