The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Marko Malikoviæ wrote:
> Parameter State : Set.
> Parameter X Y Z W : State ->  nat.
> Definition FourTuple (S : State) := (X S, Y S, Z S, W S).
>
> Function that change (and rotate) the elements of the tuple is (for example):
>
> Definition Change1 (S : State) := (Y S + 1, X S + 2, W S + 3, Z S + 4).
>
> And now I have no idea how to define function Change2 which have to be
> Change1 of Change1. The reason is clear: Change1 takes an argument of type
> State, and returns the result of type tuple.
>    

Are you just asking how to write a tuple type in Coq?  If so, that 
should certainly be covered in any standard introduction to Coq.