Skip to Content.
Sympa Menu

coq-club - [Coq-Club]Decreasing arguments for fixpoint definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Decreasing arguments for fixpoint definitions


chronological Thread 
  • From: "Adam Koprowski" <adam.koprowski AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]Decreasing arguments for fixpoint definitions
  • Date: Sat, 22 Jul 2006 16:06:02 +0200
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=oGIDA5OMZYceunGVyV0rLpP04ZTCEdChuksudCzlpF/O5t4ivGYqooBdh4BSiVrsq/OhqDzRncdGRrSNiRGbteXi2bVtCTaKagXrWk8/+mXCcjL3cfJG9CAAQ8s9cSw6gjgnOw6eYbJNMYmyZsXz7pz8v/QxYfYuwu2Hi9aZuBQ=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
 
  Dear all,
 I wonder how one can persuade Coq that the Fixpoint definition is well-formed if the decrease of the argument is not completely obvious. For instance how to modify the definition of Vfun in the simple scriplet below to make it acceptable by Coq?
  Thanks in advance for any help,
   Adam


Variable A : Set.

Inductive T : Set :=
| Ts: A -> T
| Tc: T -> T -> T.

Inductive V : Set :=
| Vc: T -> V.

Fixpoint Vfun (v: V) : A :=
match v with
| Vc (Ts a) => a
| Vc (Tc t1 t2) => Vfun (Vc t1)
end.

--
=====================================================
Adam.Koprowski AT gmail.com , ICQ: 3204612
http://www.win.tue.nl/~akoprows
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

Archive powered by MhonArc 2.6.16.

Top of Page