The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

Satrajit Roy wrote:

> Hi guys!!!!
> I have been grappling with polymorphism in Coq for a while. So thought 
> a concrete example might make it easier for people to answer.
>
> Let's say I have:
>
> Inductive policy_kind:Set :=
>     policy_a | policy_b.
>
> Record policy_A:Set := A {a_def : bool; a_cur:bool}.
> Record policy_B:Set := B {b_def: nat; b_max:nat; b_cur:nat}.
I have corrected some typos in the record declaration.

> What should be the correct definition for 'policy' if I want to do 
> something like the following:
>
> Definition policy (k:policy_kind) (data:list <?>) : <?> :=
>     match k with
>        | policy_a => A (nth 0 data) (nth 1 data) (*nth must return a 
> bool*)
>        | policy_b => B (nth 0 data) (nth 1 data) (nth 2 data) (*nth 
> must return a nat*)
> end.
>
> I know I can do it differently, but I want to do it this way so that 
> the accessor functions are auto generated.
Here is one solution :
 Definition elem_of_pol k := match k with policy_a => bool  | policy_b 
=> nat  end.
 Definition type_of_pol k := match k with policy_a => policy_A | 
policy_b => policy_B end.

Require Import List.
(* The first arguments of nth is implicite, the last is a default value
    (if the list contain less than n elements,
    where n is the  the second argument of nth) *)

Definition policy (k:policy_kind) (data : list (elem_of_pol k)) : 
type_of_pol k :=
 match k return list (elem_of_pol k) -> type_of_pol k with
 | policy_a => fun (lb:list bool) =>  A (nth 0 lb true) (nth 1 lb true)
 | policy_b => fun (ln:list nat) => B (nth 0 ln 0) (nth 1 ln 0) (nth 2 
ln 0)
 end data.

Benjamin

> There may be syntax errors in the above, but, basically I need to 
> figure out what would the terms be that should replace the '?" in the 
> above definition.
>
> Thanks in anticipation.