The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Saturday 04 November 2006 08:27, 
roconnor AT theorem.ca
 wrote:
> As I understand, Andre' Hirschowitz and Marco Maggesi use the nested
> data-type for bindings in thier solution to the POPLmark challenge
>
> <http://web.math.unifi.it/users/maggesi/fsub/>
>
> You may wish to see how they define their functions.

Thanks to everyone who replied.  I see that the above POPLmark solution uses 
the development branch of Coq and the new support for these kinds of 
inductive terms as mentioned by Ralph Matthes.  That just gives me another 
reason to anticipate the new release :-)

For anyone who might be curious, I was able to define gfoldT using the 
definitions from my previous email with some additional trickery.  The basic 
idea is to recurse over an auxiliary datatype expressing the shape of the 
term.  Code follows.  In passing, I would say that the difficulty of defining 
this fairily simple function clearly justifies the new extension.

-- 
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 := .

Inductive TermShape : Set :=
  | ShVar : TermShape
  | ShApp : TermShape -> TermShape -> TermShape
  | ShLam : TermShape -> TermShape.
  
Fixpoint termShape (V:Type) (t:Term V) {struct t} : TermShape :=
  match t with
  | Var V2 _   => ShVar
  | App V2 x y => ShApp (termShape V2 x) (termShape V2 y)
  | Lam V2 x   => ShLam (termShape (Incr V2) x)
  end.

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].


Lemma mapT_preservesShape : 
  forall
    (A B:Type)
    (f:A->B)
    (t:Term A)
    (sh:TermShape),

    termShape A t = sh ->
    termShape B (mapT f t) = sh.
    
  intros A B f t.
  generalize B f; clear B f.
  induction t using Term_rect; simpl.
  intros; auto.
  intros; auto.
  rewrite <- H.
  rewrite (IHt1 B f (termShape V t1)); auto.
  rewrite (IHt2 B f (termShape V t2)); auto.

  intros.
  rewrite <- H.
  rewrite (IHt (Incr B) (mapI f) (termShape (Incr V) t)); auto.
  Qed.
  

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 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))
  (B   : Type)
  (a   : Term (M B))
  : N B.
  intros N M var app lam k B a.

  refine (
    (fix f (B:Type) (V:Type) (z:Term V) (sh:TermShape) {struct sh} :
      (V = M B) -> (termShape V z = sh) -> N B :=

      match sh, z in Term MB return 
          (MB = M B) -> (termShape MB z = sh) -> N B with
      | ShVar, Var MB x   => fun (H:_) (H1:_) =>

                var B (eq_rect MB idt x (M B) H)

      | ShApp sx sy, App MB x y => fun (H:_) (H1:_) =>

                app B (f B MB x sx _ _) (f B MB y sy _ _)

      | ShLam sx, Lam MB x   => fun (H:_) (H1:_) =>

             lam B (f (Incr B) (M (Incr B))
               (mapT (fun x0:_ => k B (eq_rect MB Incr x0 (M B) H)) x) sx _ _)

      | _, _  => _ (* impossible cases -- discharge with 'discriminate' *)

      end) B (M B) a
         (termShape (M B) a)
         (refl_equal (M B))
         (refl_equal (termShape (M B) a)));

  simpl; intros; auto; try discriminate.

  simpl in H1; injection H1; auto.
  simpl in H1; injection H1; auto.
  simpl in H1; injection H1.
  intro H2; rewrite <- H2.
  apply mapT_preservesShape; auto.
  Defined.