The Coq mailing list

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

You're not wrong - this is what I need.

Marko Malikovic

> Le Sat, 3 Mar 2012 19:39:07 +0100 (CET),
> Marko Maliković 
>Â <marko AT ffri.hr>
>  a écrit :
>
>> It is no longer important. I just forgot about the composition of
>> functions. Thanx to Jonas Oberhauser. He understood what I need.
>
> I guess that what was proposed was to have a function from states to
> tuples:
>
> Definition tupleOfState (S : State) := (X S, Y S, Z S, T S).
>
> And then have regular functions on tuples:
>
> Definition change1 (t : nat*nat*nat*nat) : nat*nat*nat*nat :=
>  let (a,b,c,d) := t in (a+1,b+2,c+3,d+4).
>
> So that you could define:
>
> Definition Change1 s := change1 (tupleOfState s).
> Definition Change2 s := change1 (change1 (tupleOfState s)).
>
> Am I wrong?
>
>>
>> Greetings,
>>
>> Marko Malikovic
>> > Marko Maliković wrote:
>> >> 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).
>> >>
>> >
>> > I'm still having trouble identifying some non-trivial issue in your
>> > question.  Are you asking how to write a recursive function in
>> > Coq?  Or when you write "induction" do you mean "recursion," such
>> > that you are looking for a way to implement an iterated
>> > self-composition function without explicit recursion?
>>
>>
>
>


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