Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Decreasing arguments for fixpoint definitions


chronological Thread 
  • From: David Pichardie <david.pichardie AT irisa.fr>
  • To: "Adam Koprowski" <adam.koprowski AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]Decreasing arguments for fixpoint definitions
  • Date: Sun, 23 Jul 2006 16:19:28 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Adam,

You offer me a good occasion to make some advertisement about the new Coq feature named Function.
In Coq8.1beta, you have now an easy way to define such functions.

You example is particularly easy to define using a measure function. See the coq script below.
Function helps you to make proof too (which is often as hard as programming...).
I you have something to prove on such a function I would be happy to show you how
'function induction' can help you.

Function syntax is given here : http://coq.inria.fr/V8.1beta/refman/Reference-Manual003.html#@command15

Coq script (using Coq 8.1beta http://coq.inria.fr/V8.1beta):

Require Export Omega.
Require Export Recdef.

Variable A : Set.

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

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

(* Measure function to prove termination of Vfun *)
Fixpoint mesT (t:T) : nat :=
  match t with
   Ts a => 0
 | Tc t1 t2 => S (mesT t1 + mesT t2)
 end.

Definition mes (v:V) : nat :=
  let (t) := v in mesT t.

Lemma decrease_Vfun : forall t1 t2,
  mes (Vc t1) < mes (Vc (Tc t1 t2)).
Proof.
  intros; simpl; omega.
Qed.

(* Definition of Vfun *)
Function Vfun (v: V) {measure mes v} : A :=
match v with
| Vc (Ts a) => a
| Vc (Tc t1 t2) => Vfun (Vc t1)
end.
Proof.
  intros; subst; apply decrease_Vfun.
Qed.

(* Two usefull proofs have so been generated *)
Check Vfun_equation.
Check Vfun_ind.




Le 22 juil. 06, à 16:06, Adam Koprowski a écrit :

 
  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)
=====================================================
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
David Pichardie
http://www-sop.inria.fr/everest/personnel/David.Pichardie/
post-doc in the EVEREST team
INRIA Sophia-Antipolis
2004 Route des Lucioles
BP 93, 06902 Sophia Antipolis Cedex
France
Phone: (+33) 4 92 38 71 97
Fax: (+33) 4 92 38 50 29





Archive powered by MhonArc 2.6.16.

Top of Page