Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Dear Georges and Joshua,

FWIW I had encountered a similar need (dependently-typed finfuns), for
a different aim: I needed to put a canonical structure of finType over
the dependent product of finTypes to formalize the product
distribution for the dependent product of finite probability spaces,
using the infotheo [1] library.

I ended up developing a small theory [2] where dependent finfuns are
defined in terms of non-dependent finfuns with the following encoding:

Section Finite_product_structure.
  Variables (I : finType) (T_ : I -> finType).
  Record fprod : predArgType :=
    { fprod_fun : {ffun I -> {i : I & T_ i}} ;
      fprod_prop : [forall i : I, tag (fprod_fun i) == i] }.
  
  Notation fprod_type := (forall i : I, T_ i) (only parsing).
  Program Definition fprod_type_of_fprod : fprod -> fprod_type.
  Program Definition fprod_of_fprod_type : fprod_type -> fprod.
  Coercion fprod_type_of_fprod : fprod >-> Funclass.
…
End Finite_product_structure.
…
Notation "[ 'fprod' i : I => F ]" := (fprod_of_fprod_type (fun i : I => F))
  (at level 0, i ident, only parsing) : fun_scope.

[1]<https://github.com/affeldt-aist/infotheo/>
[2]<https://github.com/erikmd/coq-bool-games/blob/master/src/fprod.v>

Even if that encoding wouldn't address Joshua's question (as it's just
another layer on the existing definition of finfuns) I'd be interested
to discuss whether some bits of that approach could be useful to
generalize finfuns in math-comp… and have native support for
dependently-typed finfuns with relevant canonical structures.

Kind regards,

Erik

Le mercredi 27 février 2019 à 19:44 +0100, georges gonthier a écrit :
>   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

-- 
Érik Martin-Dorel, PhD
Maître de Conférences, Lab. IRIT, Univ. Toulouse 3


https://www.irit.fr/~Erik.Martin-Dorel