The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 18 Dec 2012 11:12:19 +0800,
Liang Dou 
<ldou.ecnu AT gmail.com>
 a écrit :

> Hi , all
>    We have an inductive definition "execute" and we get the error for
> coq:
> 
> Non strictly positive occurrence of "execute" in
>  "forall s : state,
>   state ->
>   forall (l l' : state) (a : event),
>   (forall s'0 : state, ~ execute s (a :: nil) s'0) ->
>   prefix s l = true -> execute l (a :: nil) l'".
> 
> =======================================
> Definition event:=string.
> Definition state:=string.
> Definition action:=list event.
> 
> Inductive execute: state -> action -> state  ->Prop :=
> |OR1: forall  (s s' l l' : state) ( a : event),
>       (forall s', ~ (execute s (a::nil) s')) ->
>       prefix s l = true ->
>       execute l (a::nil) l' .
> 
> 
> could someone tell ue how to fix it?
> 
> 
> 3X~~!!

I know not all cases are indicated here, but I really find your case of
execute suspicious. With no more information, we cannot tell a way to
effectively fix it (or at least I can't). You can still try to define
mutually recursive case, such as:

Inductive execute …
with no_execution …
.

And then prove that "no_execution … ⇒ ~ execute …", but I think a
complete rethinking of your type would be better.
For instance, your s' (in "forall (s s' …") is orphan, and the pattern
of your type seems really unfamiliar to me. With a little more
explanation and context, I think I would be more helpful.