The Coq mailing list

[Bruno Oliveira <bruno AT ropas.snu.ac.kr>]

Hello,

I have been trying to use Coq to do some programming with indexed types,
but I found that there are some issues with pattern matching. I am hoping
that you could provide some help. I tried to create a minimal version of
the code that illustrates the issues:

Inductive Rep : Type :=
| Plus   : Rep -> Rep -> Rep
| Rec    : Rep
| Const  : Type -> Rep.

Inductive Interpret (r : Rep) : Rep -> Type :=
| inl   : forall a b, Interpret r a -> Interpret r (Plus a b)
| inr   : forall a b, Interpret r b -> Interpret r (Plus a b)
| rec   : Interpret r r -> Interpret r Rec
| const : forall a, a -> Interpret r (Const a).

Inductive T :=
| A : nat -> T
| B : T -> T.

Definition RT := Plus (Const nat) Rec.

My goal is to define a function:

Fixpoint to_T (x : Interpret RT RT) : T := ...

which converts between a structure "Interpret RT RT" and T. I tried many
things, none of which worked. Let me tell you about these:

1) A first attempt is:

Fixpoint to_T (x : Interpret RT RT) : T :=
   match x with
     | inl a b (const _ n) => A n
     | inr a b r => B (to_T r)
     | _ => A 0 (** not needed **)
   end.

However this fails.

2) I then tried to generalize a bit:

Fixpoint to_T (a : Rep) (x : Interpret RT a) : T :=
   match x with
     | inl a b (const _ n) => A  n (* fails here, does not refine the type 
*)
     | inr a b r => B (to_T r)
     | _ => A 0
   end.

This version fails because coq apparently fails to refine the type of
the value |n| to a natural number. Thus I cannot apply the constructor A.

3) Using the proof mode I can get the first case to work:

Definition to_T (a : Rep) (x : Interpret RT a) : (a = RT) -> T.
intros a x.
refine (
   match x with
     | inl a b (const _ n) => _
     | _ => fun p => A 0
   end
). intros. inversion H. subst a0.inversion i.exact (A X).
Defined.

But this is not the function I want.

4) Finally:

Definition to_T (a : Rep) (x : Interpret RT a) : (a = RT) -> T.
refine (fix to_T (a : Rep) (x : Interpret RT a) : (a = RT) -> T :=
   match x with
     | inl a b _ => _
     | inr a b _ => _
     | rec _ => _
     | const a _  => _
   end
); intros; try discriminate.

inversion H. subst a0. inversion i. exact (A X).
inversion H. subst b. inversion i. exact (to_T RT X (refl_equal RT)).
Defined.

In this definition evrything seems to work, but the termination checker
does not like it.

I am running out of ideas now. Any suggestions?

Thanks in advance for any help or suggestions.

Bruno Oliveira