The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Why do you return tuples?
Is the following not possible in your case?

(*...*)
Parameter T2S : nat -> nat -> nat -> nat -> State.
Definition Change1 (S : State) := T2S (Y S + 1) (X S + 2) (W S + 3) (Z S + 4).

Then Change2 would be
Definition Change2 := Change1 o Change1.
(*I'm not sure about the o operator, I have no coq installed*)

If you have to work with tuple types, do something like this (again, I
have no coq here so it will be nonsense syntactically):
(* .... *)
Coercion FourTuple : State >-> nat * nat * nat * nat.
Definition Change1 (S : nat * nat * nat * nat) := match S with (x, y,
z, w) => (y + 1, x + 1, w + 3, z + 4) end.
Definition Change2 := Change1 o Change1.

2012/3/3 Marko Malikoviæ 
<marko AT ffri.hr>:
> Greetings,
>
> Please help me in the problem that I noted bellow.
>
> Firstly, for some reason I should not have any inductive definitions in
> the system! (No Record, no Inductive, etc).
>
> So, it looks like this:
>
> 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.
> Is this even possible to do without any induction?
>
> Thanks in advance and best regards,
>
> Marko Malikoviæ
>
> -----------------------
> Doc. Dr. Sc. Marko Malikoviæ
> Filozofski fakultet
> Sveuèili¹te u Rijeci
> ---------------------
> Ph.D. Marko Malikoviæ
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
>Â marko AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------
>