The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.jussieu.fr>]

Hi,
The advise is : { z | P z } is an inductive type, (exist _ z (_ : P  
Z)) is the constructor of type {z | P z}

-8<------
Definition ZHs_of_Zs(zs:list Z)(*H:forall z, In z zs -> (0<=z<Max) 
%Z*) :list ZH.
refine ((fix f (zs:list Z)(*_:f z, In z zs -> (0<=z<Max)%Z*):list ZH :=
 match zs return (list ZH) with
 | nil => nil
 | cons z zs' => cons (exist _ z  _) (f zs')
 end) zs).
-8<------
will be better :-)

Pierre Boutillier

Le 7 janv. 12 à 10:26, Takashi MIYAMOTO a écrit :

> Dear all,
>
> I am trying to write a mapping function from a list of Z to a list  
> of subset type ZH.
> The definition of function ZHs_of_Zs fails. It seems that my usage  
> of refine tactic is wrong.
> Could you give an advice how to write functions like this?
>
> ---
>
> Require Import ZArith.
> Parameter Max:Z.
> Parameter HMax:(Max >= 2)%Z.
> Definition ZH := {z:Z | (0<=z<Max)%Z}.
>
> Definition ZHs_of_Zs(zs:list Z)(H:forall z, In z zs -> (0<=z<Max) 
> %Z) :list ZH.
> refine (fix f (zs:list Z)(_:forall z, In z zs -> (0<=z<Max)%Z):list  
> ZH :=
>  match zs return (list ZH) with
>  | nil => nil
>  | z::zs' => {z|_} :: (f zs' _)
>  end).
>
> ---
>
> Thank you in advance.
>
> ===================================
> Takashi Miyamoto

Pierre Boutillier
pierre.boutillier AT pps.jussieu.fr