The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

As something of a mental exercise, I've been attempting to formalize in Coq 
the nested-datatype formulation of deBruijn lambda notaion from Bird and 
Patterson's paper _de Bruijn Notation as a Nested Datatype_.

So far I've found working with the nested datatype quite awkward, and I'm 
having some difficulty getting some of the function definitions to pass Coq's 
typechecker.  Are there any way to make the following definitions better?  
I'm not 100% sure I understand why 'Term' has to be in sort 'Type'. Is there 
some trick I can use to make the definition of gfoldT typecheck, or do I have 
to do it using well-founded recursion?  Is there any way to eliminate some of 
the mucking about with dependent pattern matching and eq_rect?

Many Thanks,
Rob Dockins

Talk softly and drive a Sherman tank.
Laugh hard, it's a long way to the bank.
       -- TMBG


(*************************************************)

Inductive Incr  (V:Type) : Type :=
  | Zero : Incr V
  | Succ : V -> Incr V.

Inductive  Term : Type -> Type :=
  | Var : forall (V:Type), V -> Term V
  | App : forall (V:Type), Term V -> Term V -> Term V
  | Lam : forall (V:Type), Term (Incr V) -> Term V.

Inductive Closed : Type := .

Definition mapI (A:Type) (B:Type) (f:A->B)
  (x:Incr A) : Incr B :=
  match x with
  | Zero => Zero B
  | Succ a => Succ B (f a)
  end.
Implicit Arguments mapI [A B].

Fixpoint mapT (A:Type) (B:Type) (f:A->B)
  (x:Term A) {struct x} : Term B :=
  (match x in (Term V) return (V->B) -> (Term B) with
  | Var V a   => fun (g:_) => Var B (g a)
  | App V a b => fun (g:_) => App B (mapT V B g a) (mapT V B g b)
  | Lam V a   => fun (g:_) => Lam B (mapT (Incr V) (Incr B) (mapI g) a)
  end) f.
Implicit Arguments mapT [A B].


Definition compose (A:Type) (B:Type) (C:Type) (g:B->C) (f:A->B) (x:A) := g (f 
x).
Implicit Arguments compose [A B C].
Notation "g <.> f" := (compose g f) (at level 90, right associativity).

Definition ext_eq (A:Type) (B:Type) (f:A->B) (g:A->B) := forall (x:A), f x = 
g 
x.
Implicit Arguments ext_eq [A B].
Notation "f <=> g" := (ext_eq f g)  (at level 95, no associativity).

Definition idt := fun x:Type => x.

Definition gfoldT
  (N:Type -> Type)
  (M:Type -> Type)
  (var : forall A:Type, M A -> N A)
  (app : forall A:Type, N A -> N A -> N A)
  (lam : forall A:Type, N (Incr A) -> N A)
  (k   : forall A:Type, Incr (M A) -> M (Incr A))
  : forall B:Type, Term (M B) -> N B :=

  fix f (B:Type) (z:Term (M B)) {struct z} : N B := 
    match z in Term MB return MB = (M B) -> N B with
    | Var MB x   => fun (H:_) => var B (eq_rect (MB) idt x (M B) H)
    | App MB x y => fun (H:_) => app B (f B (eq_rect MB Term x (M B) H))
                                       (f B (eq_rect MB Term y (M B) H))
    | Lam MB x   => fun (H:_) => lam B (f (Incr B) (mapT (k B)
                                       (eq_rect MB (Term <.> Incr) x (M B) 
H)))
    end (refl_equal (M B))
  .

(*
This definition elicits the following error:

Recursive call to f has principal argument equal to
"mapT (k B) (eq_rect MB (Term <.> Incr) x (M B) H)"
instead of x
*)