The Coq mailing list

[roconnor AT theorem.ca]

I was attempting to implement Bird and Paterson's non-uniform parametric
implementation of untyped lambda calculus in Coq.
<http://www.soi.city.ac.uk/~ross/papers/debruijn.html>

The definition of lambda expressions is parameterized over the type of
the free variables:

Inductive Lambda : Type -> Type :=
 | var : forall A:Type, A -> Lambda A
 | app : forall A:Type, Lambda A -> Lambda A -> Lambda A
 | lambda : forall A:Type, Lambda (Maybe A) -> Lambda A.

Here ``Maybe'' is just like ``option'' except on Type instead of Set.

Inductive Maybe (A:Type) : Type :=
 | none : Maybe A
 | just : A -> Maybe A.

I want to defined the _generic fold_ function.  In Haskell
this--total--function can be defined as:

> gfold :: (forall a. m a -> n a) ->
>             (forall a. n a -> n a -> n a) ->
>             (forall a. n (Maybe a) -> n a) ->
>             (forall a. (Maybe (m a)) -> m (Maybe a)) ->
>             Lambda (m a) -> n B
> gfold v a l k (Var x) = v x
> gfold v a l k (App x y) = a (gfold v a l k x) (gfold v a l k y)
> gfold v a l k (Lambda x) = l (gfold v a l k (lift x))

You can see from the last line that this recursion is not structural.  x
is applied to lift before passed to gfold again.  lift is just the obvious
function of type

lift
     : forall A : Type, Lambda A -> forall B : Type, (A -> B) -> Lambda B

I tried to define gfold by recursion on the ``depth'' of lambda
expressions. I created a function

Definition depth2 : (sigT (fun X:Type=>Lambda (m X)))->nat

to compute the depth of a lambda expression.  I evaluate the depth of the
dependent pair (X, t) because my recursion needs lambda expressions of a
given depth over all types to be done before the next depth.

But when I do my induction_ltof1 I get to the following point:

[...]
x : Type
d : Lambda (m x)
______________________________________(1/1)
(forall y : sigT (fun X : Type => Lambda (m X)),
 ltof (sigT (fun X : Type => Lambda (m X))) depth2 y
   (existT (fun X : Type => Lambda (m X)) x d) -> n (projT1 y)) -> n x

Now I want to apply ``dependent inversion d'', but it doesn't work because
dependent inversion d needs to be able to replace d with an arbitrary
Lambda Y, but the existT forces d to be Lambda (m Y).

So I am running low on ideas.  Is it even possible to create these
generalized fold functions in Coq?

Anyone up to the challenge of writing this total function in Coq?

I've attached a Coq file that gets as far as the above.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''(* Author: Russell O'Connor *)
(* This file is Public Domain *)
Require Import WfType_nat.
Require Import Max.

Inductive Maybe (A:Type) : Type :=
 | none : Maybe A
 | just : A -> Maybe A.

Definition liftM (A:Type)(B:Type)(f:A->B)(t:Maybe A) : Maybe B :=
match t with
  none => none B
| just a => just B (f a)
end.

Inductive Lambda : Type -> Type :=
 | var : forall A:Type, A -> Lambda A
 | app : forall A:Type, Lambda A -> Lambda A -> Lambda A
 | lambda : forall A:Type, Lambda (Maybe A) -> Lambda A.

Fixpoint lift (A:Type) (t:Lambda A) {struct t} : forall B:Type, (A->B) -> 
Lambda B :=
match t in (Lambda A) return forall B:Type, (A->B) -> (Lambda B) with
  var A a => fun (B:Type) (f:A->B) => var B (f a)
| app  A r s => fun (B:Type) (f:A->B) => app B (lift A r B f) (lift A s B f )
| lambda A t => fun (B:Type) (f:A->B) => lambda B (lift (Maybe A) t (Maybe B) 
(liftM A B f))
end.

Fixpoint depth (A:Type)(f:Lambda A) {struct f} : nat :=
match f with
 var A a => 0
|app A r s => 1+max (depth _ r) (depth _ s)
|lambda A r => 1+(depth _ r)
end.

Lemma liftDepth (A:Type)(f:Lambda A)(B:Type)(g:A->B) : depth A f = depth B 
(lift A f B g).
Proof.
do 2 intro.
induction f; intros.
reflexivity.
simpl.
rewrite (IHf1 B g).
rewrite (IHf2 B g).
reflexivity.
simpl.
rewrite (IHf (Maybe B) (liftM _ _ g)).
reflexivity.
Qed.

Section gfold.

Variable m:Type->Type.
Variable n:Type->Type.
Variable v:forall a:_,(m a)->n a.
Variable a:forall a:_,(n a)->(n a)->n a.
Variable l:forall a:_,(n (Maybe a))->n a.
Variable k:forall a:_,(Maybe (m a))->m (Maybe a).
Variable B:Type.

Definition depType (X:Type) := Lambda (m X).

Definition depth2 : (sigT depType)->nat.
intros.
destruct X.
eapply depth.
apply d.
Defined.

(*we want the following haskell (total) function

> gfold :: (forall a. m a -> n a) ->
>             (forall a. n a -> n a -> n a) ->
>             (forall a. n (Maybe a) -> n a) ->
>             (forall a. (Maybe (m a)) -> m (Maybe a)) ->
>             Lambda (m a) -> n B
> gfold v a l k (Var x) = v x
> gfold v a l k (App x y) = a (gfold v a l k x) (gfold v a l k y)
> gfold v a l k (ambda x) = l (gfold v a l k (lift x))
*)


Definition gfold (t:(Lambda (m B))) : (n B).
intros.
apply induction_ltof1 with (P:= fun x:(sigT depType) => n (projT1 x)) 
(f:=depth2)(a:=existT depType B t).
clear B t.
intro.
destruct x.
unfold depType in d.
simpl.
unfold depType.
(*dependent inversion cannot work with the d inside the existT expression*)
dependent inversion d.