The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello Nicolas,

The error is induced by the "NoDup" field of M.t.

One workaround could be to split the inductive definition in two parts:

    Inductive raw_tree: Type :=
     mkRawTree: T -> M.Raw.t raw_tree -> raw_tree.

    Import M.

    Inductive wf_tree: raw_tree -> Prop :=
     mkRawTree_wf (x:T) (l: M.t raw_tree):
       (forall p, List.In p l.(this) -> wf_tree (snd p))
       -> wf_tree (mkRawTree x l.(this)).

    Record tree : Type := { raw: raw_tree; wf: wf_tree raw }.


But, I do not know if such an approach works well in practice...

S.


Le 10/04/2019 à 11:23, Nicolas Osborne a écrit :
> Dear Coq-Club,
>
> I need to define a rose tree with a map instead of a list. As I don’t 
> have any reason to care about efficiency in this context, I use 
> FMapWeakList from the Standard Library and declare the following:
>
>     Require Import Coq.Structures.DecidableTypeEx.
>     Require Import Coq.FSets.FMapWeakList.
>
>     Variable T:Type.
>     Module M := FMapWeakList.Make(Nat_as_DT).
>
>     Inductive tree: Type := mkTree: T -> M.t tree -> tree.
>
> Then, Coq greets me with the following error message:
>
>        Error: Non strictly positive occurrence of "tree" in "nat -> M.t 
> tree -> tree".
>
> As I understand it, this means that "tree" occurs at the left of an 
> arrow in one of the argument of the constructor (namely "M.t tree"), 
> which is forbidden for consistency reasons.
>
> Is there any way around ?
>
> My first guess would be to use a list of products in the tree:
> Inductive tree’: Type := mkTree’: T -> list (nat * tree’) -> tree’.
>
> and then make sure that this list behaves like a map when writing the 
> functions handling the modifications of the tree.
>
> But if there is a way to use directly a map in the tree, that would be a 
> relief.
>
> Thanks,
> Nicolas Osborne