The Coq mailing list

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

Dear Coq developers and users,

Have somebody idea how to build recursive function when all arguments are
increasing, but without using CoInductive types (just inductive)?

For example, on the bottom of this mail is recursive definition of
function "problem". Normally, it is ill-formed because x and y are
increasing (don't look too much in data's of example because this example
is fanciful).
Anyway, this function will always stop because of:

match x' with
 10 => False

match y' with
 10 => False

But Coq don't know that function will always stop.

One way is to embed some decreasing argument i and use {struct i} but then
I must to have i like argument in "problem x y i" and it is not so nice
(although I can ignore this argument i).

My second idea was to use "pred" (predecessor) but it is a function and it
is not well formed constructor.

Some ideas (I repeat: without CoInductive types).

Thank you very much,

Marko Malikoviæ

Here is example:

Require Import List.

Definition list_A :=
(2 :: 2 :: 3 :: 3 :: nil) ::
(4 :: 4 :: 2 :: 1 :: nil) ::
(1 :: 1 :: 1 :: 2 :: nil) ::
(3 :: 2 :: 4 :: 5 :: nil) ::
(5 :: 5 :: 4 :: 1 :: nil) ::
nil.

Fixpoint problem (x y:nat) {struct x} : Prop :=
match nth y (nth x list_A nil) 0 with
    5 => match nth (y+1) (nth (x+1) list_A nil) 0 with
             1 => True
           | 2 => match x+2 with
                      S x' => match y+2 with
                                  S y' => match x' with
                                              10 => False
                                            | _ => match y' with
                                                       10 => False
                                                     | _ => problem x' y'
                                                   end
                                          end
                                | _ => False
                              end
                    | _ => False
                  end
           | _ => False
         end
  | _ => False
end.