The Coq mailing list

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

Le Sat, 7 Sep 2013 20:01:24 +0000,
Djamila Baroudi 
<baroudi.d7 AT gmail.com>
 a écrit :

> hello;
> I defines a new type called "event" and I still have to define the
> relationship between these events like the sequence between two
> events, which means that event e2 can not happen unless the event e1
> is checked.
> 
> 
> 
> Inductive event:Type:=send(msg:string)
> | receive(msg:string)
> 
> I try this but it's incorrect:
> 
> Inductive activity:Type:=
> evenement(_:event).
> |sequence (e1 e2 : event) : bool := e1 && e2.
> 
> can you help me please? n
> Thank you.
> 

First of all, I do not advise to start with strings if you are a
beginner, unless you have absolutely no knowledge of the kind of
messages.

For example, you could define:

Inductive from_client :=
  | Connect : from_client
  | Disconnect : from_client
  | Get : url -> from_client (* assuming the url type is defined *)
.

Inductive from_server :=
  | ConnectionAccepted : from_server
  | ConnectionDenied : refusal -> from_server (* assuming refusal is
defined *)
  | Post : data -> from_server (* assuming data is defined *)
  | ConnectionAborted : error_code -> from_server (* assuming
error_code is defined *)
.

About the sequence of events, there is no trick, "e2" MUST know what
occured before, so that you need some trace of previous events (or at
least a state, like in a Moore machine, in which it is assumed that "e1"
occured before).

Require Import List.

Definition trace := list (from_client + from_server).

After that, you have to define what is a good trace, then you can prove
stuff on it (with Moore machines, that would mean that your state must
be accessible from an initial state, still you need to provide the
transition rules).

Inductive GoodRun (t : trace) : Prop :=
  | Abortion : forall (e : error_code), t = (ConnectionAborted e)::nil
->
               GoodRun t
  | Success : t = Disconnect::nil -> GoodRun t
  | Post : forall (a : trace) (d : data), GoodRun a -> t = (Post d)::a
->
           GoodRun t
  | Get : forall (a : trace) (u : url), GoodRun a -> t = (Get u)::a ->
          GoodRun t
.

Inductive GoodTrace (t : trace) : Prop :=
  | EmptyTrace : t = nil -> GoodTrace t
  | Sequence : forall (a b : trace), GoodTrace a -> GoodTrace b ->
               t = a++b -> GoolTrace t
  | QuickEnd : forall (r : refusal),
               t = Connect::(ConnectionDenied r)::nil -> GoodTrace t
  | LongRun : forall (a : trace) : GoodRun a -> t = Connect::a ->
              GoodTrace t
.

Lemma test1 : forall (u : url), GoodTrace (
        Connect::
        ConnectionAccepted::
        (Get u)::
        Disconnect
).
Proof. (* Left as an exercise *)
Qed.

Lemma test2 : forall (u : url), GoodTrace (
        Connect::
        ConnectionAccepted::
        (Get u)::
        Connect
) -> False.
Proof. (* Left as an exercise *)
Qed.