The Coq mailing list

[roconnor AT theorem.ca]

With Milad Niqui's help I managed to create the function.
For those interested, I've attached the solution.

The key seems to be to write the following trivial lemma.

Lemma elimLambdaM (B:Set) :
forall (P:(Lambda (m B)->Set)) (t:Lambda (m B)),
(forall a:(m B),P (var (m B) a)) ->
(forall (p:(Lambda (m B)))(q:(Lambda (m B))), P (app (m B) p q)) ->
(forall p:(Lambda (Maybe (m B))),P (lambda (m B) p)) ->
P t.
intros.
destruct t; auto.
Qed.

As you can see, all it does is run destruct; however, despite my best
efforts, I cannot create this function without using this lemma.  I've
tried to replace my use of elimLambdaM with destruct, case, and inversion
tactics but I always just get ``cannot solve second order unification''.

Well, at least I have a solution.

I had to use -impredicative-set in order to define the join function for
my monad.

-- 
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:Set) : Set :=
 | none : Maybe A
 | just : A -> Maybe A.

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

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

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

Fixpoint depth (A:Set)(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:Set)(f:Lambda A)(B:Set)(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:Set->Set.
Variable n:Set->Set.
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).

Inductive D_gfold :forall (T:Set), (Lambda (m T)) -> Set := D_gfold_var
: forall (T: Set) (x:m T), D_gfold T (var (m T) x)
                                           | D_gfold_app : forall (T:
Set) (x y:Lambda (m T)), D_gfold T x -> D_gfold T y -> D_gfold T (app (m
T) x y)
                                           | D_gfold_abs : forall (T:
Set) (x:Lambda (Maybe (m T))), D_gfold (Maybe T)
                                              (lift (Maybe (m T)) x (m
(Maybe T)) (k T))-> D_gfold T (lambda (m T) x ).

Fixpoint gfoldHelp (T : Set) (t : Lambda (m T)) (Ht : D_gfold T t) {struct
Ht} : n T :=
  match Ht in (D_gfold T0 l) return (n T0) with
  | D_gfold_var T0 x => v T0 x
  | D_gfold_app T0 x y Hx Hy => a T0 (gfoldHelp T0 x Hx) (gfoldHelp T0 y Hy)
  | D_gfold_abs T0 x Hx => l T0 (gfoldHelp (Maybe T0) (lift (Maybe (m T0)) x
(m (Maybe T0)) (k T0)) Hx)
end.

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

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

Lemma elimLambdaM (B:Set) : forall (P:(Lambda (m B)->Set))
(t:Lambda (m B)),
(forall a:(m B),P (var (m B) a)) ->
(forall (p:(Lambda (m B)))(q:(Lambda (m B))),
  P (app (m B) p q)) ->
(forall p:(Lambda (Maybe (m B))),
P (lambda (m B) p)) -> P t.
intros.
destruct t; auto.
Qed.

Lemma total (B:Set) : forall t:(Lambda (m B)),(D_gfold B t).
intros.
apply induction_ltof1 with (P:= fun x:(sigT depType) =>
 D_gfold (projT1 x) (projT2 x))(f:=depth2)(a:=existT depType B t).
clear B t.
intro.
destruct x.
simpl.
unfold depType in d.
unfold depType.
intros.
cut (d=d).
apply elimLambdaM with (P:=(fun y:_ => d=y->D_gfold x y)).
intros.
constructor.
intros.
constructor.
apply (H (existT depType x p)).
rewrite H0.
unfold ltof.
simpl.
apply Lt.le_lt_n_Sm.
apply le_max_l.
apply (H (existT depType x q)).
rewrite H0.
unfold ltof.
simpl.
apply Lt.le_lt_n_Sm.
apply le_max_r.
intros.
constructor.
apply (H (existT depType (Maybe x)
(lift (Maybe (m x)) p (m (Maybe x)) (k x)))).
unfold ltof.
simpl.
rewrite <- liftDepth.
rewrite H0.
simpl.
apply Lt.lt_n_Sn.
reflexivity.
Qed.

Definition gfold (T : Set) (t : Lambda (m T)) : n T :=
gfoldHelp T t (total T t).

End gfold.

Definition join : forall (T:Set)(l:Lambda (Lambda T)),(Lambda T) :=
gfold Lambda Lambda
(fun (a:Set)(l:_) => l)
(fun (a:Set)=> (app a))
(fun (a:Set)=>(lambda a))
(fun (a:Set)(m:_)=>
 match m with 
 | none => var _ (none _)
 | just x => lift _ x _ (just _)
 end).

Definition sub (A B:Set) (l:Lambda A) (m:A->Lambda B) : Lambda B :=
join _ (lift _ l _ m).