The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

No,

I ask whether it is possible to create a function Change2 that will be
defined as "Change1 (Change1 SomeTuple)" but without the use of induction.
So, the function which will two (or more) times in the same way change the
tuple. So Change1 function must return a result that is the same type as
its argument.
Something like this:

Definition Change2 (TupleB): = Change1 (Change1 TupleA).

Thanks you,

Marko Malikovic

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


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