Ssreflect Users Discussion List

[Joshua Gancher <>]

This is a very good idea --  I will check this out, and likely it will work for my purposes. Many thanks!

Joshua

On Wed, Feb 27, 2019 at 1:44 PM georges gonthier <> wrote:

  Dear Joshua,
Your question actually did give me the idea for an improvement to the finfun library.
The root cause of your issue is that the MathComp encoding of tuples fails the positivity criterion, as finfuns are based on tuples.
   There is an alternative definition that does not have this drawback, using an indexed inductive (the `vector` type in the Coq standard library).
However this encoding interfaces poorly with the list/seq library, so we can’t really adopt it.
    Nevertheless as finfuns do not rely heavily on the properties of tuples it is feasible to base them on indexed inductives instead,
and indeed doing so makes it possible to handle dependent functions naturally.
    If you would like to try it out I’ve implemented this in a new dependent-positive-finfun branch in the mathcomp repository.
It is still work in progress as I have stumbled on a serious shortcoming of the Coq engine that impacts the dependent function extension -
so the initial commit on the branch only compiles up to matrix.v (and breaks there), but perhaps this is sufficient for your purposes.
I will work around this issue by shunting some of the dependent support later - I needed to document the impact of the Coq issue first.
   Cheers,
Georges

> Le 21 févr. 2019 à 15:18, Assia Mahboubi <> a écrit :
>
> 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