The Coq mailing list

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

Le Sat, 22 Dec 2012 17:46:46 +0800,
Liang Dou 
<ldou.ecnu AT gmail.com>
 a écrit :

>     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.

Your explanation still lacks some precision.

Here is one of the interpretations I did from your description, but I
bet it is not the one you wish. Maybe you can adapt it to fit your
needs. Coq is for formal systems, you need to be very precise when
defining something in it. If you cannot give some very precise
description of what you want, I think you should not use Coq.

I did not use strings, I gave here some more general framework.
(By the way, I do not really encourage the use of string in Coq, as its
use is rather horrible. I think using a list of elements of a type of
about 4 to 16 values is often a lot more convenient.)

=====================
Require Import List.
Set Implicit Arguments.

Record state_prio : Type :=
  { state : Type
  ; preempts : state -> state -> Prop
  ; preempts_trans : forall s t u,
    preempts s t -> preempts t u -> preempts s u
  ; preempts_strict : forall s, ~ preempts s s
  }.

Record transition (state : Type) (event : Type) : Type :=
  { source : state
  ; trigger : event
  ; target : state
  }.

Record execute_aux (state : Type)
                   (event : Type)
                   (transitions : list (transition state event))
                   (init : state)
                   (events : list event)
                   (fin : state) : Prop :=
  { selected_trigger : event
  ; selected_trigger_spe1 : In {|source:=init
                                ;trigger:=selected_trigger
                                ;target:=fin|} transitions
  ; selected_trigger_spe2 : In selected_trigger events
  }.

Record execute (sttp : state_prio)
               (event : Type)
               (transitions : list (transition (state sttp) event))
               (init : state sttp)
               (events : list event)
               (fin : state sttp) : Prop :=
  { possible_execution : execute_aux transitions init events fin
  ; preempting_execution :
    forall i f, execute_aux transitions i events f ->
    ~ preempts sttp i init
  }.

> 
>      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.