The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 1 Mar 2006, Brian E. Aydemir wrote:

> 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.
>
> (* ******************** *)
> 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.
> (* ******************** *)

The match clause should read:

   match x in (Phi z) return (Phi (S z)) with

See: <http://cocorico.cs.ru.nl/coqwiki/MatchAsInReturn>

After fixing this you will have more work ahead of you: convering a to a'
and back in your subexpressions.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''