The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Conor McBride wrote:

> Will the attached do?

That'll do. I translated it in Coq and it works almost as nicely as your  
Epigram version.

Venanzio

(* Translation of Conor McBride's Epigram formalization *)

Set Implicit Arguments.

Inductive Vec (X:Set): nat -> Set :=
  vnil : Vec X 0
| vcons : forall (n:nat)(x:X), Vec X n -> Vec X (S n).

Implicit Arguments vnil [X].

Definition match_vcons:
  forall (X:Set)(P:nat->Set)(n:nat), Vec X (S n) ->
  (X -> Vec X n -> P (S n)) -> P (S n).
Proof.
intros X P n v f; inversion_clear v as [|H x v'].
apply f; [exact x | exact v'].
Defined.

Implicit Arguments match_vcons [X P n].

Lemma match_vcons_reduction:
  forall (X:Set)(P:nat->Set)(n:nat)(f:X->Vec X n->P (S n))(x:X)(v:Vec X n),
    match_vcons (vcons x v) f = f x v.
Proof.
auto.
Qed.

Fixpoint vec (X:Set)(n:nat)(x:X){struct n}: Vec X n :=
match n return Vec X n with
  O => vnil
| (S n) => vcons x (vec n x)
end.

Require Import List.

Fixpoint vapp (X Y:Set)(n:nat)(fs: Vec (X->Y) n){struct fs}:
  Vec X n -> Vec Y n:=
match fs in Vec _ n return Vec X n -> Vec Y n with
  vnil => fun _ => vnil
| vcons n f fs => fun ss =>
                  match_vcons ss (fun s ss => vcons (f s) (vapp fs ss))
end.

Definition vbo (X:Set)(f:X->X->X)(n:nat): Vec X n -> Vec X n -> Vec X n :=
fun xs ys => vapp (vapp (vec n f) xs) ys.

Fixpoint vtrans (X:Set)(m n:nat)(xss: Vec (Vec X n) m){struct xss}:
  Vec (Vec X m) n:=
match xss in Vec _ m return Vec (Vec X m) n with
  vnil => vec n vnil
| vcons m xs xss => vapp (vapp (vec n (vcons (n:=m)))
                               (xs))
                         (vtrans xss)
end.

Fixpoint Arity (X:Set)(n:nat)(Y:Set){struct n}: Set :=
match n with
  O => Y
| (S n) => X -> (Arity X n Y)
end.

Fixpoint vapps (m n:nat)(X Y:Set){struct n}:
  Vec (Arity X n Y) m -> Arity (Vec X m) n (Vec Y m) :=
match n return Vec (Arity X n Y) m -> Arity (Vec X m) n (Vec Y m) with
  O => fun fs => fs
| (S n) => fun fs ss => vapps n X Y (vapp fs ss)
end.

Definition vmaps:
  forall (m n:nat)(X Y:Set), Arity X n Y -> Arity (Vec X m) n (Vec Y m) :=
fun m n X Y f => vapps n X Y (vec m f).