The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Nov 6, 2006, at 12:53 AM, David Nowak wrote:

> 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?

I did.  Adding the definition of distT to the development I posted in  
my last email gives rise to universe inconsistencies.  I tried a  
number of workarounds, including adding a duplicate definition of  
terms under a different name, but I couldn't get anything to work.

I think you might be right about universe polymorphism.  The goal is  
to define the join operation, which has type:

forall A:Type, Term (Term A) -> Term A

If I understand the situation correctly, there isn't any way at all  
to define a function with this type if Term is in sort Type.   
Actually, you could replace Term with _any_ definition in sort Type  
and this would still be impossible.  It is also my understanding that  
if I could magically make Coq accept the Term definition in sort Set  
that these problems would go away.  Is all that right?

Also, for my edification, are there fundamental issues with universe  
polymorphism in CiC, or is this just a feature that isn't in high  
demand?



> 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/



Rob Dockins

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