The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Lorenzo,

  You can define such a function using:

Fixpoint fmap_tree_size (f : fmap_tree) : nat := 
  match f with
  | fmap_leaf n => 0
  | fmap_node n br => foldr maxn 0 (codom (fmap_tree_size \o br)) + 1
  end.

Finite maps are based on finite functions which allow such nested definitions,
You can find an example in the doc:

https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finfun.html#finfun_of_tuple

— Matthieu


> On 19 Feb 2021, at 14:58, Lorenzo Gheri <lor.gheri AT gmail.com> wrote:
> 
> Hi Li-yao and All,
> 
> thank you very much for your answer. That was helpful indeed. However, the 
> main issue there stays: 
> 
> Since `br` is not a partial function, but a fmap, I cannot really do `fun x 
> => depth (br x)`, but I must do `fun x => depth (br.[? x])`, namely what 
> happens is not a simple function application.
> 
> Around fmaps nice results have been developed and that's why I was eager to 
> use this type for finite branching. Has anyone tried something similar, and 
> would be happy to share their experience?
> 
> Best,
> Lorenzo
> 
> 
> 
> 
> On Thu, 18 Feb 2021 at 19:25, Li-yao Xia <lysxia AT gmail.com> wrote:
> 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
> > 
> > 
> >