The Coq mailing list

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

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
>
>
>