The Coq mailing list

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

(*
Hello,

I'm trying to model the behavior of a very simple system. Consider the
following
*)

Section Generalization.
Variable message : Type.
Variable state : Type.
Variable send_request : message -> state -> state.
Variable send_reply : message -> state -> state.
Variable p : message -> state -> Prop.
Variable q : message -> state -> Prop.

(*
» first hint
»   <it may not hold in your real implementation, though>
»   : select what will be parameters and what will be
»     indices
»
»Putting all as indice will always work,
»but may be rather annoying at some times.
»That is you will often have to rely on the inversion tactic,
»if you do not want to work it manually, where case/destruct
»is often a lot more convenient and will perfectly work with
»parameters.
»
»So use indice only when required.
»In fact, I think indice are never necessary when
»if you allow yourself to use equalities
»(equalities have indices, but you can restrict yourself to
»this sole case, except maybe in JMeq or very similar and
»not very common cases).
»
»Note that in your case, you use equality on s',
»so I guess you should not use indices.
*)

Inductive system_exec (m : message) (s s' : state) : Prop :=
  | Request: q m s
          -> s' = send_request m s
          -> system_exec m s s'

  | Reply: p m s
        -> s' = send_reply m s
        -> system_exec m s s'
.

(*
» This is the version in which you do not want to allow yourself
» using equalities, and were indices become mandatory.
»
»Inductive system_exec (m : message) (s : state) : state -> Prop :=
»  | Request: q m s
»          -> system_exec m s (send_request m s)
»
»  | Reply: p m s
»        -> system_exec m s (send_reply m s)
».
»
»As you may need to use some inversion tactic,
»I consider the uncommented »form more convenient.
*)

(*p and q are just predicates included here for the sake of clarity..*)

(*
where state is a structure along the lines of an automaton.

The idea is that I want to model a (possibly infinite) execution,
meaning an infinite number of messages sent, making it go from state s
to state s'...

If following the standard approach used for operational semantics, I
would use a (possibly refl.) transitive closure of system_exec, but I
cannot use this in this case as I'm not going from elements of the same
type. I mean its not like I can do (message * state) -> (message *
state) as the message on the 'target' state is senseless for my
modeling...

» Note that (possibly refl.) transitive closure of system_exec won't
» allow infinite execution, but only finite. You need more than
» transitivity. I think in this case we could speak of 'completion of
» the transitive closure' to allow the limits (I am all but sure of
» this terminology).

Also, usually one uses this approach to model the fact of program
'reduction', until we cannot progress anymore (e.g. SKIP - well if you
define your relation reflexive you can still progress, but lets ignore
that...), which is not exactly what I want here.

» I think it has nothing to do with a reflexive relation.
» Reflexivity does not allow you to keep progressing.

So, how would you go about modeling a system that would just allow a
possibly infinite exchange of messages in a operational semantics
fashion?

» What about coinduction?
*)

CoInductive TransitiveClosureCompletion
 (X:Type) (R:X->X->Prop) (x : X) (y : X) : Prop
:= Term : R x y -> TransitiveClosureCompletion X R x y
 | Step : forall z t, TransitiveClosureCompletion X R x z ->
                      TransitiveClosureCompletion X R t y ->
             R z t -> TransitiveClosureCompletion X R x y.
(*
» Well, there is an equivalent and simpler version where the second
» constructor does not have 'z', 'z' is replaced by 'x',
» and "TransitiveClosureCompletion X R x x" is removed.
» Always put a "R ?a ?b" in the constructors to have some "resistor"
» without it, you will be able to prove
» "∀ x y, TransitiveClosureCompletion x y"
» which is not what you want.
*)

CoInductive ReflexiveTransitiveClosureCompletion
 (X:Type) (R:X->X->Prop) (x : X) (y : X) : Prop
:= Term2 : x = y -> ReflexiveTransitiveClosureCompletion X R x y
 | Step2 : forall z, R x z -> ReflexiveTransitiveClosureCompletion X R
z y -> ReflexiveTransitiveClosureCompletion X R x y.
(*
» Here is an example dealing with reflexivity
*)

(*
One possible idea would be defining my relation from (stream message *
state) to (stream message * state). Then, my Request constructor would
take the head of the stream to know the message to send, and would go
to a state s' with the effect of that emission. As for the Reply
constructor, it would just check if there is some message to reply to,
affect the state and leave the stream of messages unaffected I guess..

Well, I still need some thinking on this, but anyway, do you think the
above would be a good approach? How would you do it? :D
*)

(*
» If I well remember, CompCert uses a convergent and a divergent
» semantics. Maybe you could be interested in such a thing.
*)

Definition Terminal (s : state) : Prop
:= forall m s', ~ system_exec m s s'.
(*
» Or possibly a more subtle relation…
*)

Inductive ConvergentExecution (s s' : state) : Prop :=
| Termination : s = s' -> Terminal s -> ConvergentExecution s s'
| Converging : forall m t, system_exec m s t ->
               ConvergentExecution t s' -> ConvergentExecution s s'.

CoInductive DivergentExecution (s : state) : Prop :=
| Diverging : forall m t, system_exec m s t -> DivergentExecution t ->
              DivergentExecution s.

(*
Thank you, and an Happy New Year to all of you who just got back to the
office today!

» I also wish that for all of us

Cheers.

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible
life choice.
*)
End Generalization.