The Coq mailing list

[jean-francois.monin AT imag.fr]

It is true that type theory prevents us to write
general recursive definitions with "not completely obvious" 
termination. 
For general techniques, see wf recursion or results by
Bertot & Balaa and Bove & Capretta.
That said, IMHO, prefer simple solutions when available,  
e.g. in your case why not just write

Fixpoint Tfun (t:T) : A :=
match t with
| Ts a => a
| Tc t1 t2 => Tfun t1
end.

Definition Vfun (v:V) : A :=
match v with
| Vc t => Tfun t
end.

  JF

Adam Koprowski a ecrit :
 >   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)
 > =====================================================

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 44