The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 12/17/2012 10:12 PM, Liang Dou wrote:
> 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?
>    

I assume it's clear that your definition is not even positive, let alone 
strictly positive.  There is a good chance that admitting your 
definition would create a logical inconsistency, though I haven't 
verified it for sure.

For more information on why Coq needs to enforce this restriction, see 
Section 3.6 of CPDT <http://adam.chlipala.net/cpdt/>.

As Cedric wrote, it is not obvious that there is a trivial restatement 
of your definition that will be legal.  One has to know more context for 
such things.  One promising albeit inconvenient option might be to 
define a [notExecute] mutual inductive that covers all the ways that 
[execute] might fail.