The Coq mailing list

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

This is what I have done yet. (Not much because of laziness.)

--------

Require Import ZArith.

Open Scope Z.

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.

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.

Ltac D := unfold tak'; repeat (destruct Z_le_dec; try omega);

 repeat (destruct Z.eq_dec; try omega);

 repeat destruct Zeven_odd_dec; parity_tac; try omega.

Inductive tak : Z -> Z -> Z -> Z -> Prop :=

  | tak_base : forall x y z, x <= y -> tak x y z z

  | tak_call : forall x y z a b c r,

    y < x ->

    tak (x-1) y z a -> 

    tak (y-1) z x b ->

    tak (z-1) x y c ->

    tak a b c r ->

    tak x y z r.

Theorem T_base x y z r: x<=y -> r=z -> tak x y z r.

 intros; D. rewrite H0; apply tak_base; auto.

Qed.

Theorem T0 x y z r: y<x -> z-1<=y<=z+1 -> r=y -> tak x y z r.

intros. assert (r=tak' x y z) by (D; auto). rewrite H2.

 intros. 

  apply Zlt_lower_bound_ind with (z:=y+1)(x:=x); [|omega]; intros.

  apply tak_call with (a:=tak' (x0-1) y z) (b:=tak' (y-1) z x0) (c:=tak' (z-1) x0 y);

   try omega; D; try (apply tak_base; omega); 

   assert (y = tak' (x0-1) y z) by (D; auto); rewrite H6 at -1; apply H3; omega.

Qed.

Theorem T1 x y z r: y=x-1 -> z>=x+1 -> r=x -> tak x y z r.

 intros. rewrite H1.

  apply tak_call with (a:=tak' (x-1) y z)(b:=tak' (y-1) z x)(c:=tak' (z-1) x y);

   try omega; D; try (apply tak_base; omega); apply T0; omega.

Qed.

Lemma Termination1 x y z r: y<x -> r=tak' x y z -> tak x y z r.

 intros. rewrite H0.

 apply Zlt_lower_bound_ind with (z:=y+1)(x:=x). 2: omega. intros.

 apply tak_call with (a:=tak' (x0-1) y z) (b:=tak' (y-1) z x0) (c:=tak' (z-1) x0 y); D;

 try (apply T_base; omega); try (apply T0; omega); try (apply T1; omega).
 (* this can be automatised too *)

  assert (z+1=tak' (x0-1) y z) as X by D; rewrite X; apply H1; omega.

  assert (y=tak' (x0-1) y z) as X by D; rewrite X at -1; apply H1; omega.

  assert (y=tak' (x0-1) y z) as X by D; rewrite X at -1; apply H1; omega.

  assert (y=tak' (x0-1) y z) as X by D; rewrite X at -1; apply H1; omega.

  assert (y=tak' (x0-1) y z) as X by D; rewrite X at -1; apply H1; omega.

  assert (x0-1=tak' (x0-1) y z) as X by D; rewrite X at -1; apply H1; omega.

  assert (y+1=tak' (x0-1) y z) as X by D; rewrite X; apply H1; omega.

(* with 5 cases left *)


In some future I will try to find and use some more useful induction, maybe copying from Wojciech's proof. :)

On Wed, Jan 15, 2014 at 1:22 AM, Wojciech Jedynak <wjedynak AT gmail.com> wrote:

Hello,

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

yes! I actually tried this approach two days ago and succeded, but now
I'm waiting for the proof market to accept solutions again. I'm not so
sure about the simple part, though -- I found a nice measure by
analyzing relation between the depth of the recursion  and the inputs.
I didn't use the _dec functions in the def. of tak0, but instead
relied on e.g. <=?, so that could simplify my proof.

Best,
Wojciech