The Coq mailing list

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

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

--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/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