coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive function with increasing arguments

From: Venanzio Capretta <venanzio_logic AT yahoo.it>
To: Marko Malikovi� <marko AT ffri.hr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Recursive function with increasing arguments
Date: Fri, 14 Sep 2007 12:06:03 +0200 (CEST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.it; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=jA6G4zhAwI7ubhG9+dJ25HZgRtzihIo+jLFzvBuE7SINkR0kXRYArDzQURluSv24snv28LHSMXBLk7jk9iwnKf7f+mX1mUdgoGsaz2da+6mu6wD3VPAgxP1qQgOmK6UM6jTZbfwwI8PFtdpLTVUaWqjj5l2XFFJBNkPBRgxnuPY=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Here is a solution to your problem that uses "Bove/Capretta" method.
See:
Bove & Capretta
  "Nested General Recursion and Partiality in Type Theory" (TPHOLs 2001)
  "Recursive Functions with Higher Order Domains" (TLCA 2005)
  "Modelling general recursion in type theory" (MSCS 15:4, 2005)
I leave the proof of Dtotal to you, but it should be easy.

Venanzio

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.

Definition prob_call (x y:nat): nat*nat+bool :=
match nth y (nth x list_A nil) 0 with
    5 => match nth (y+1) (nth (x+1) list_A nil) 0 with
             1 => (inr _ true)
           | 2 => match x+2 with
                      S x' => match y+2 with
                                  S y' => match x' with
                                              10 => (inr _ false)
                                            | _ => match y' with
                                                       10 => (inr _ false)
                                                     | _ => inl _ (x',y')
                                                   end
                                          end
                                | _ => (inr _ false)
                              end
                    | _ => (inr _ false)
                  end
           | _ => (inr _ false)
         end
  | _ => (inr _ false)
end.

Inductive D: (nat*nat+bool) -> Set :=
  dtrue:  D (inr _ true)
| dfalse: D (inr _ false)
| dstep: forall x y, D (prob_call x y) -> D (inl _ (x,y)).

Fixpoint prob_aux (u:nat*nat+bool)(h:D u){struct h}: Prop :=
match h with
  dtrue => True
| dfalse => False
| dstep x y h' => prob_aux (prob_call x y) h'
end.

Lemma Dtotal: forall u, D u.
Proof.
Admitted.

Definition problem (x y:nat): Prop :=
  prob_aux (inl _ (x,y)) (Dtotal (inl _ (x,y))).

      Make free worldwide PC-to-PC calls. Try the new Yahoo! Canada Messenger
at http://ca.messenger.yahoo.com/

[Coq-Club] Recursive function with increasing arguments, Marko Malikovi�
- Re: [Coq-Club] Recursive function with increasing arguments, David Pichardie
- <Possible follow-ups>
- Re: [Coq-Club] Recursive function with increasing arguments, Venanzio Capretta