The Coq mailing list

[David Nowak <david.nowak AT aist.go.jp>]

Hello Rob,

> 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 :-)

It appears that the current version of the experimental command  
"Function" cannot go through the definition of gfoldT.  It returns  
the following error message:

  failure in proveterminate
  User error: find_call_occs : Lambda

See below my code "Example 1" (It needs the development version of  
today -- version 9340).

Also I tried to defined joinT directly (i.e. without using gfoldT).   
See below my code "Example 2".  But then I ran into universe  
inconsistencies!

It is very likely that my direct definition of joinT is wrong.   
However I have the feeling that the lack of universe polymorphism in  
Coq prevent one to formalize properly nested datatypes.

Do you too run into universe inconsistencies?

Best,

David



(******* Example 1 *******)

Require Import Recdef.

Set Implicit Arguments.

Inductive Incr (A:Type) : Type :=
  zero : Incr A
| succ : A->Incr A.

Inductive Trm : Type->Type :=
  var : forall A, A->Trm A
| app : forall A, Trm A->Trm A->Trm A
| lam : forall A, Trm (Incr A) -> Trm A.

Definition mapI (A B:Type)(f:A->B)(x:Incr A) : Incr B :=
  match x with
    zero => zero B
  | succ x' => succ (f x')
  end.

Fixpoint mapT (A B:Type)(f:A->B)(t:Trm A) {struct t} : Trm B :=
  match t in (Trm T) return ((T -> B) -> Trm B) with
    var _ x => fun f' => var (f' x)
  | app _ t1 t2 => fun f' => app (mapT f' t1) (mapT f' t2)
  | lam _ t' => fun f' => lam (mapT (mapI f') t')
  end f.

Fixpoint mesT (A:Type)(t:Trm A) {struct t} : nat :=
  match t with
    var _ _ => 0
  | app _ t1 t2 => mesT t1 + mesT t2
  | lam _ t' => mesT t' + 1
  end.

Function gfoldT
  (A B:Type)(M N:Type->Type)
  (v:forall A, M A->N A)(a:forall A, N A->N A->N A)(l:forall A, N  
(Incr A)->N A)
  (k:forall A, Incr (M A)->M (Incr A))
  (t:Trm A) {measure mesT t} : A=M B -> N B :=
  match t in (Trm T) return (T = M B -> N B) with
    var A0 x =>
      fun H : A0 = M B =>
        v B (eq_rect A0 (fun T : Type => T) x (M B) H)
  | app A0 t1 t2 =>
      fun H : A0 = M B =>
        a B (gfoldT (A:=A0) B M N v a l k t1 H)
            (gfoldT (A:=A0) B M N v a l k t2 H)
  | lam A0 t' =>
      fun H : A0 = M B =>
        l B (gfoldT (A:=(M (Incr B))) (Incr B) M N v a l k
              (mapT
                (k B)
                ((fun t'0 : Trm (Incr (M B)) => t'0)
                 (eq_rect A0 (fun A1 : Type => Trm (Incr A1)) t' (M  
B) H)))
              (refl_equal (M (Incr B))))
         end.



(******* Example 2 *******)

Set Implicit Arguments.

Inductive Incr (A:Type) : Type :=
  zero : Incr A
| succ : A->Incr A.

Inductive Trm : Type->Type :=
  var : forall A, A->Trm A
| app : forall A, Trm A->Trm A->Trm A
| lam : forall A, Trm (Incr A) -> Trm A.

Definition mapI (A B:Type)(f:A->B)(x:Incr A) : Incr B :=
  match x with
    zero => zero B
  | succ x' => succ (f x')
  end.

Fixpoint mapT (A B:Type)(f:A->B)(t:Trm A) {struct t} : Trm B :=
  match t in (Trm T) return ((T -> B) -> Trm B) with
    var _ x => fun f' => var (f' x)
  | app _ t1 t2 => fun f' => app (mapT f' t1) (mapT f' t2)
  | lam _ t' => fun f' => lam (mapT (mapI f') t')
  end f.

Definition distT (A:Type)(x:Incr (Trm A)) : Trm (Incr A) :=
  match x with
    zero => var (zero A)
  | succ x' => mapT (succ (A:=A)) x'
  end.

Definition joinT (A:Type)(t:Trm A)(B:Type)(H:A=Trm B) : A.
Proof.
fix 2.
intros A t.
destruct t as [C x| C t1 t2| C t']; intros B H.
apply x.
rewrite H in |- *.
  apply app.
  eapply joinT.
  rewrite <- H in |- *.
    apply t1.
reflexivity.
eapply joinT.
rewrite <- H in |- *.
   apply t2.
reflexivity.
rewrite H in |- *.
  apply lam.
   eapply joinT.
apply (mapT (distT (A:=B))).
   rewrite <- H in |- *.
   apply t'.
reflexivity.
Defined.

--
David Nowak
http://staff.aist.go.jp/david.nowak/