The Coq mailing list

[Liang Dou <ldou.ecnu AT gmail.com>]

    Actually, we are trying to define a state automata with priority.
Suppose that if the name of state s1 is the prefix of state s2, then
s1 has the higher priority. All the transition with higher priority
states will be executed first.

    For example,there are two states with names "s1" and "s11".
Obviously, the priority of "s1" is higher than "s11" .  When we have
two transitions to execute:t1 =( "s1","a","s2") and
t2=("s11","a","s3") and  an event 'a' fires, t1 should execute first
due to the priority rule.
    The inductive type 'execute' is defined to describe the above
execution rule. But we get the error from Coq.

     Thanks agin for your help.
===================================

Definition event:=string.
Definition state:=string.
Definition action:=list event.
Definition trigger:= event.
Definition transition:= state * trigger * state.
Definition s1:="s1".
Definition s11:="s11".
Definition s2:="s2".
Definition s3:="s3".
Definition t1:=(s1,"a",s2).
Definition t2:=(s11,"a",s3).
Definition ev:="a"::nil. (*The evironment of automata, which contains
all enable events to fire*)
Definition T:= t1::t2::nil.  (*The transition set,which contains all
the possible transitions can be executed*)
Inductive execute: state -> action -> state  ->Prop :=
|OR1: forall  (s s' l l' : state) ( a : event),
      (exists t, In t T /\ In (snd (fst t)) ev /\ (fst (fst t)) = l )->
      (forall s', ~ (execute s (a::nil) s')) ->
      prefix s l = true ->
      execute l (a::nil) l' .

2012/12/18 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.