The Coq mailing list

[Nicolas Osborne <nicolas.osborne.etu AT univ-lille.fr>]

Thanks for the answer Sylvain.

I played a little with your proposition. The problem is that when I want to 
use one
of the primitives of M.t, I have to open the tree, rebuild an M.t, use the 
primitive and
rebuild the tree.

As I don’t have a lot of experience with Records and dependent types in 
general, this 
should prove to be difficult to implement in the current project.

Nicolas

> Le 10 avr. 2019 à 14:03, Sylvain Boulmé 
> <Sylvain.Boulme AT univ-grenoble-alpes.fr>
>  a écrit :
> 
> 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