The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

https://proofmarket.org/problem/view/19

In this problem I have found related function in closed form:

Definition tak' x y z :=

 if Z_le_dec x y

  then z

  else if Z_le_dec z x

   then if Zeven_odd_dec (y-x)

    then if Z_le_dec (z+2) y

     then z+1

     else y

    else y

   else if Z.eq_dec y (x-1)

    then x

    else if Z.eq_dec z (x+1)

     then y

     else if Zeven_odd_dec (z-x)

      then x

      else y+1.

Proofs of properties here (lots of time are needed on slow computers, as mine, for example):

Theorem thm1 x y z: x <= y -> tak' x y z = z.

 intros; unfold tak'; destruct Z_le_dec; omega.

Qed.

Ltac parity_tac := match goal with

| x: Zeven _ |- _ => apply Zeven_ex_iff in x; destruct x; parity_tac

| x: Zodd _ |- _ => apply Zodd_ex_iff in x; destruct x; parity_tac

| _ => idtac

end.

Theorem thm2 x y z: y < x -> tak' x y z = tak' (tak' (x-1) y z) (tak' (y-1) z x) (tak' (z-1) x y).

 intros; unfold tak';

 repeat (destruct Z_le_dec; try omega);

 repeat (destruct Z.eq_dec; try omega);

 repeat (destruct Zeven_odd_dec; try omega); parity_tac; omega.

Qed.

Is it possible use this result to prove theorem tak_terminates? In some simple way?

Or more general question? Is it possible to prove termination (similarly to the problem) if I have corresponding function with all required recursive equations proved?