coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robert Dockins <robdockins AT fastmail.fm>
- To: David Nowak <david.nowak AT aist.go.jp>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club]Nested datatypes in Coq
- Date: Mon, 6 Nov 2006 09:11:21 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club]Nested datatypes in Coq, Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq,
roconnor
- Re: [Coq-Club]Nested datatypes in Coq,
Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq,
David Nowak
- Re: [Coq-Club]Nested datatypes in Coq, Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq,
jean-francois . monin
- Re: [Coq-Club]Nested datatypes in Coq, Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq, Adam Chlipala
- Re: [Coq-Club]Nested datatypes in Coq, roconnor
- Re: [Coq-Club]Nested datatypes in Coq,
jean-francois . monin
- Re: [Coq-Club]Nested datatypes in Coq, Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq,
David Nowak
- Re: [Coq-Club]Nested datatypes in Coq,
Robert Dockins
- Re: [Coq-Club]Nested datatypes in Coq, Stefan Monnier
- Re: [Coq-Club]Nested datatypes in Coq,
roconnor
Archive powered by MhonArc 2.6.16.