The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Hi everyone,

I fail to understand why Coq cannot type check a definition involving  
dependent types, so I am hoping that someone here may be able to  
explain what is happening.  I give first a simplified version of my  
code that illustrates the problem.

(* ******************** *)
Require Import Arith.
Lemma le_lt_S : forall (n m : nat), n <= m -> n < S m.
Proof. intros; auto with arith. Qed.

Inductive Phi : nat -> Set :=
  | pfree : forall (n : nat), nat -> Phi n
  | pbound : forall (n m : nat), m < n -> Phi n
  | papp : forall (n : nat), Phi n -> Phi n -> Phi n
  | plam : forall (n : nat), Phi (S n) -> Phi n.

Fixpoint abs
  (m : nat) (n : nat) (wf : n <= m) (a : nat) (x : Phi m) {struct x}
  : Phi (S m)
:=
  match x with
    | pfree _ a' =>
          if eq_nat_dec a a' then pbound _ n (le_lt_S _ _ wf) else  
pfree _ a'
    | papp _ s t =>
          papp _ (abs _ n wf a s) (abs _ n wf a t)
    | _ => pfree _ a
  end.
(* ******************** *)

In the definition of abs, the type checker gives the following error  
for the occurrence of s in the recursive call in the papp case: The  
term "s" has type "Phi n0" while it is expected to have type "Phi  
m".  My guess is that in the pattern "papp _ s t", Coq fills the  
joker in with "n0", and from the definition of papp, that fixes the  
type of s to "Phi n0".  My intuition says that since x has type "Phi  
m", that means if x has the shape "papp n0 s t", then n0 and m ought  
to be convertible for each other and the case should type check.   
Matters do not improve if I fill in the joker myself.

It has been pointed out to me that I can use tactics, in particular  
"refine", to define my function, and the resulting term suggests that  
I should declare my function as

        Fixpoint abs (m : nat) (n : nat) (a : nat) (x : Phi m) {struct x}
        : (n <= m) -> Phi (S m)

While this solves the problem at hand, I'm still not seeing exactly  
why I should expect my original definition to fail.  Is there some  
subtlety about depend types that I have missed?

Any help is appreciated.

Cheers,
Brian

--
Brian E. Aydemir | http://www.cis.upenn.edu/~baydemir/