The Coq mailing list

[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
-------------------------