The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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