Ssreflect Users Discussion List

[Allyx FONTAINE <>]

Thanks a lot! Then I'll make a try with the family predicate which seems 
to be very convenient.
Cheers,
Allyx

Le 29/09/2011 11:55, Georges Gonthier a écrit :
>    Finfun doesn't handle dependent function types, so you can't directly 
> express the length constraint in the type. You will either have to build your 
> own version of finfun based on dependently typed lists, or use the family 
> predicate to carve out a subtype, something like this:
>
>   Variables (F : finType) (f : F ->  nat) (R : Type).
>
> Definition nfinfun_fam x := [pred s : seq R | size s == f x].
> Inductive nfinfun := NFinfun ff of ff \in family nfinfun_fam.
>
> Definition nfinfun_val nf := let: NFinfun ff _ := nf in ff.
> Canonical nfinfun_subType := [subType for nfinfun_val by nfinfun_rect].
>
> Definition fun_of_nfinfun (ff : nfinfun) x := Tuple (forallP (valP ff) x).
> Coercion fun_of_nfinfun : nfinfun>->  Funclass.
>
> Lemma nfinfunP (nf1 nf2 : nfinfun) : (forall x, nf1 x = nf2 x)<->  nf1 = nf2.
> Proof. by split=>  [eqf | ->  //]; apply/val_inj/ffunP=>  x; case: (eqf x). 
> Qed.
>
> As with finfun and finset,  you may also want to make the Coercion opaque and 
> have an explicit expansion lemma.
>
>
> -----Original Message-----
> From: Allyx FONTAINE []
> Sent: 28 September 2011 14:34
> To: ssreflect
> Subject: finfun and tuple
>
> Hi all,
>
> Lets consider a finite type F.
> I would like to define the type of finite functions which take in parameter an 
> element of type F (lets call it elt) and returns a sequence of (f elt) nat where 
> (f: F ->  nat) .
>
> I thought about using finfun and tuple, but I did not succeed. So I wonder 
> what are the possible definitions. What do you suggest ?
>
> Thanks for your help,
> Allyx