The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Paul,

you have nested recursive calls like s0 (s0 y), that is not accepted by 
the Coq guardedness check.

Maybe you can implement you functions in a structurally recursive way.

Cheers,
Andreas

On 16.06.11 6:20 PM, Paul Tarau wrote:
> (* mutually recursive components of s,p *)
> Fixpoint s0 (a:T) :=
> match a with
> | E =>  E
> | (C E y) =>  C (s0 (s0 y)) (s1 (s0 y))
> | (C (C _ _) _) =>  E
> end
> with s1 (a:T) :=
> match a with
> | E =>  E
> | (C E y) =>  s1 y
> | (C (C a b) y) =>  C (p2 a b) y
> end
> with p2 (x:T) (y:T) :=
> match x,y with
> | E,E =>  E
> | E,(C a b) =>  C (C (s0 a) (s1 a)) b
> | (C a b),c =>  C E (p2 (p2 a b) c)
> end.
> (*
> Unfortunately, Coq rejects this with:
>
> Error: Cannot guess decreasing argument of fix.
>
> I think that termination of the mutually recursive Fixpoint
> follows from the fact that at each step in every match
> in every definition at least one argument becomes structurally
> simpler - so every reduction in the mutually recursive
> definition makes progress towards termination.
> *)

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/