The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Dimitri Hendriks wrote:

> The system complains that the following definition is not well-formed.
>
> Fixpoint rm_last [A:Set;n:nat]  : (cp A n)->(cp A (pred' n)) :=
> <[n:nat](cp A n)->(cp A (pred' n))>
> Cases n of
> | O    => [u:unit]u
> |(S m) => 
>  <[m:nat](cp A (S m))->(cp A (pred' (S m)))>
>  Cases m of
>  | O => [t:A*unit] let (_,u)=t in u
>  | k => [t:A*(cp A k)] let (a,t')=t in (a,(rm_last A k t'))
>  end
> end.
>
> How to make it work?
>  

Hi Dimitri,

I won't claim this is very elegant, but the following works:

Fixpoint rm_last [A:Set;n:nat]  : (cp A n)->(cp A (pred' n)) :=
<[n:nat](cp A n)->(cp A (pred' n))>
Cases n of
| O    => [u:unit]u
|(S m) =>
 (<[m0:nat]m0=m->(cp A (S m0))->(cp A (pred' (S m0)))>
 Cases m of
 | O => [Heq:O=m][t:A*unit] let (_,u)=t in u
 | k => [Heq:k=m][t:A*(cp A k)] let (a,t')=t in
         (a,(eq_rec ?? [m](cp A (pred' m))
                (rm_last A m (eq_rec ?? [m](cp A m) t' ? Heq))
                ? (sym_equal ??? Heq)))
 end (refl_equal ? m))
end.

The problem comes from the fact that you are doing a dependent 
elimination and thus k must be an alias for (S n0), where n0 is the name 
of the predecessor of m (Coq substitutes pattern (S n0) for k). As a 
consequence, rm_last is applied to (S n0), which is rejected for the 
same as your alternative definition of pred' is rejected.

The funny(?) thing is that in the case of pred', since it is a 
non-dependent elimination, another choice is made for k: k is an alias 
for m.
The trick I propose is to abstract an equality property which allows to 
replace k (that is (S n0)) with m and vice versa. rm_last is applied to 
m (for the guard condition) and t' with its type changed, (cp A m) 
instead of (cp A k). After the recursive call, we must change the type 
the other way round.

I'd say this example raises an interesting question about typing Cases. 
It shows that we may want to have the choice between dependent and 
non-dependent elimination for each branch, and not only for a given Case 
expression...

Cheers,

Bruno Barras.