Ssreflect Users Discussion List

[Assia Mahboubi <>]

Dear Joshua,

I am afraid I do not have a satisfactory answer to provide...

With your first version

> Inductive TstF :=
>   | TBase : nat -> TstF
>   | TF : (T -> TstF) -> TstF.

there is indeed little hope to obtain an eqType up to extensionality in
CIC without extra axiom, due to the arrow type in the argument of the TF
constructor.

It is certainly a pity that Coq is not able to detect that a definition
 like:

> Inductive TstF' :=
>   | TBase' : nat -> TstF'
>   | TF' : {ffun T -> TstF'} -> TstF'.

is harmless. But I am afraid that a discussion on a the possible
improvements of the (so-called positivity) condition for the
well-formedness of inductive types would be more appropriate elsewhere,
e.g. on the CoqClub mailing list.

Here is the only thing I could come up with: working with the less
specific type

Inductive TstF_aux :=
| TBase_aux : nat -> TstF_aux
| TF_aux : seq TstF_aux -> TstF_aux.


and recover the corresponding function TF : T -> TstF attached to an
inner node using something like:

TF (s : seq TstF) : T -> TstF := fun t => nth (TBase 0) s (enum_rank t).

Type TstF_aux can be easily endowed with eq/choice/countType structures
using for instance an encoding to GenTree.tree (as indicted in the
header of the choice.v library).

A predicate discriminating well-formed trees (with sequences of the
appropriate size) might be necessary. In which case, a subType could be
used to transport again the eq/choice/countType structructures.

Best wishes,

assia


Le 15/02/2019 à 20:00, Joshua Gancher a écrit :
> Hi all,
> 
> Consider the below datatype, where T is a finType:
> 
> Inductive TstF :=
>   | TBase : nat -> TstF
>   | TF : (T -> TstF) -> TstF.
> 
> I would like to leverage the finType structure of T in order to give a
> choiceType structure to TstF (up to extensionality of the function in
> TF). Thus I want to do something like: 
> 
> Inductive TstF' :=
>   | TBase' : nat -> TstF'
>   | TF' : {ffun T -> TstF'} -> TstF'.
> 
> However, the above does not go through, since it violates the strict
> positivity requirement in Coq. (Indeed, replacing {ffun T -> TstF'} with
> something like {xs : list TstF' | P xs} where P is a pred also violates
> the same requirement.)
> 
> Has anybody thought of a workaround for this issue? 
> 
> Thanks,
> Joshua Gancher