The Coq mailing list

[Dimitri Hendriks <Dimitri.Hendriks AT phil.uu.nl>]

Dear all,

Does anyone know how to solve the following easy-to-formulate-problem.

I want to define a function which removes the last element of a tuple. 
Tuples are defined as generalized pairs; a tuple of n A-elements is of 
type (cp A n), the cartesian product of n copies of set A and the unit set, 
defined by:

Fixpoint cp [A:Set;n:nat] : Set :=
Cases n of
| O    => unit
|(S m) => A*(cp A m)
end.

In order to compute the type of the tuple obtained by the removal of 
its last element, I need the function pred', which (in contrast to pred)
removes the innermost S of a natural number:

Fixpoint pred' [n:nat] : nat :=
Cases n of
| O => O
|(S m) => 
  Cases m of
  | O => O
  | k => (S (pred' k))
  end
end.

Note that the following alternative definition is not accepted,
because the system doesn't recognize that the recursive argument
is decreased.

Fixpoint pred'_alt [n:nat] : nat :=
Cases n of
| O       => O
|(S m) => 
  Cases m of
  | O    => O
  |(S p) => (S (pred'_alt (S p)))
  end
end.

Ofcourse we have that:

Remark predpred' : (n:nat)(pred n)=(pred' n).
Proof.
Induction n.
Reflexivity.
Intro m; Case m.
Intro; Reflexivity.
Intros k IH.
Change (pred (S (S k)))=(S (pred' (S k))) .
Rewrite <- IH; Reflexivity.
Qed.

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?

Thank in advance,
Dimitri