The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  You can try to define a binary relation between two events, then consider
a predicate on finite traces (finite lists of events).
  I have attached a small example, but I'm not sure that it is  
exactly what you need.
 In particular it doesn't take into account repetitions of the same  
event, but it should be easy to fix that.
  Extending these definitions to  infinite traces is possible in Coq,  
using co-inductive types.

The best,

Pierre





Quoting Djamila Baroudi 
<baroudi.d7 AT gmail.com>:

> 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.
>
> --
>
> *Mlle Djamila Baroudi**                            *
>
> *Faculté des Sciences Exactes et Informatique,         *
>
>  *Université de Mostaganem,*
>
>  *27000 Mostaganem, Algérie.                   *
>
> *
> *


Require Import String.

Inductive event:Type:=
| send(msg:string)
| receive(msg:string).

Inductive must_precede : event -> event -> Prop :=
| must_precede_intro : forall msg, must_precede (send msg) (receive msg).

Goal must_precede (send "foo") (receive "foo").
Proof. split. Qed.

Goal ~ must_precede (send "foo") (receive "bar").
Proof. red;inversion_clear 1. Qed.

Goal forall m, ~ must_precede (receive m) (send m).
Proof. red;inversion_clear 1.
Qed.

Definition must_precede_dec : forall e e', {must_precede e e'}+{~ must_precede e e'}.
destruct e, e'; [right; red;inversion 1 
                | destruct (string_dec msg msg0)
                | right; red;inversion 1 
                | right; red;inversion 1].
left;subst msg0;constructor.
right;red; inversion 1; destruct n;auto.
Qed.


Require Import List.


(** tr doesn't contain any element that should occur before e *)
Definition ok (e:event) (tr: list event) :  Prop :=
forall e', In e' tr -> ~ must_precede e' e.

Goal ~ ok (receive "foo") ((send "bar")::(send "foo")::nil).
Proof. intro H; generalize (H (send "foo")); intro H'; apply H'.
 right;now left.   
 constructor.
Qed.

Inductive well_formed : list event -> Prop :=
| wf_nil : well_formed nil
| wf_cons : forall e tr, well_formed tr -> ok e tr -> well_formed (e::tr).