coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]Decreasing arguments for fixpoint definitions, Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, Sébastien Hinderer
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, jean-francois . monin
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, David Pichardie
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions,
Adam Koprowski
- Re: [Coq-Club]Decreasing arguments for fixpoint definitions, David Pichardie
Archive powered by MhonArc 2.6.16.