The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Dear Marko,

Here is a solution using the new Function feature.

I have rewriten your function using eq_nat_dec instead of pattern- 
matching because Function is not very efficient
with too big pattern matching.

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.

Require Import Recdef.
Definition mes (x:nat) : nat := 10-x.
Require Import Arith.
Require Import Omega.

Function problem (x y:nat) {measure mes x} : Prop :=
  if eq_nat_dec (nth y (nth x list_A nil) 0) 5 then
    if eq_nat_dec (nth (y+1) (nth (x+1) list_A nil) 0 ) 1 then True
      else
        if eq_nat_dec (nth (y+1) (nth (x+1) list_A nil) 0 ) 2 then
               if eq_nat_dec x 9 then False
                 else if eq_nat_dec y 9 then False
                   else problem (S x) (S y)
          else False
    else False.
intros; unfold mes; subst.
destruct (le_lt_dec x 9).
  (* case x<= 9 *)
  omega.
  (* case x> 9 : hypothesis anaonymous 1 is absurd *)
  absurd (0=2).
  omega.
  rewrite <- anonymous1.
  rewrite nth_overflow; auto.
  rewrite nth_overflow; simpl; try omega.
Qed.


I use a measure function. I have then to prove that recursive call  
are decresing wrt this measure.
Essentially I must prove this subgoal :
  anonymous1 : nth (y + 1) (nth (x + 1) list_A nil) 0 = 2
  anonymous2 : x <> 9
  ============================
   10 - S x < 10 - x

Hope this helps.

David.

Le 14 sept. 07 à 11:00, Marko Maliković a écrit :

> 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.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club