The Coq mailing list

[Marcel Ullrich <s8maullr AT stud.uni-saarland.de>]

Hi Lorenzo,

In principle such things can be solved by our MetaCoq plugin for nested inductive types, but you can also use the principle manually as follows:

We define the functor for easier use:

```
Definition F X := {fmap nat -> X}.
Inductive fmap_tree :=
| fmap_leaf (n : nat)
| fmap_node (n : nat) (branching : F fmap_tree).
```

We then define what is means assumption should
be fulfilled for the nested argument.
Namely, every subterm of type fmap_tree should have a height.

```
Definition FAssumption {X} (P:X->Type) (br:F X) :=
  forall x y, br.[? x]=Some y -> P y.
Definition FProof {X} (P:X->Type) (f:forall x, P x) (br:F X) : FAssumption P br.
  move : br => [? ?] x;case: fndP => ? ?.
  - by injection 1 as <-.
  - congruence.
Defined.
```

These two definitions could be registered and used by the plugin.
Alternatively, we can use them manually to derive the induction principle by hand:
```
Definition fmap_tree_nind
     : forall p : fmap_tree -> Type,
       (forall n : nat, p (fmap_leaf n)) ->
       (forall (n : nat) (branching : F fmap_tree),
       FAssumption p branching ->
       p (fmap_node n branching)) ->
       forall inst : fmap_tree, p inst.
Proof.
  intros p HL HN.
  refine (fix f inst := _).
  destruct inst.
  - apply HL.
  - apply HN,FProof,f.
Defined.
```

Coq accepts the definition of fmap_tree_nind as FProof only applies f to structurally
smaller instances of fmap_tree.

The definition of depth can be adapted to use fmap_tree_nind:
We fold over every number in the domain of br and if the result of
br.[?x] is not None, the recursively determined depth can be used.
```
Definition depth (T : fmap_tree) : nat.
  refine(fmap_tree_nind (fun _ => nat)
    (fun n => 0)
    (fun n br h =>
      (foldr maxn 0 (map (fun x => _
      ) (enum_fset (domf br)))).+1
    ) T).
  destruct (br.[?x]) eqn:H.
  - exact (h x _ H).
  - exact 0.
Defined.
```

Two small testcases:
```
Compute (depth (fmap_leaf 42)). (* 0 *)
Definition t1 := fmap_node 3 fmap0.
Compute (depth t1). (* 1 *)
```

Best,
Marcel

Am 19.02.21 um 14:58 schrieb Lorenzo Gheri:

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