The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 21 Sep 2011 09:32:11 +0800 (CST),
左樱 
<phoebezz AT 163.com>
 a écrit :

> Hi guys,
>    
>   We are defined a relationship "simulation" over two traces and try
> to prove the transitive property of it. But we meet some problems
> when proving the sim_tl case. So I wonder whether I give the proper
> definition on "simulation". We define a simulation relation over two
> traces trace1 and trace2 inductively as follow: (1) Let c c’ ∈ cnd, e
> e’ ∈ event,  (ge c e)  (ge c’ e’)∈grdevt(GuardEvent), simulation
> (ge c e)  (ge c’ e’) if bImp c c’ and e = e’ (2)There is a strictly
> increasing function λ:dom(trace1) -> dom(trace2) Such that: Let i,j ∈
> grdevt(GuardEvent), a. Forall  i∈ trace1 , exists j∈ trace2 ,
> simulation i  (λj) b. forall j= (ge c e) ∈ trace1 ,if not (j
> ∈image(trace2)) , exists  k=(ge c’ e’)∈grdevt and j strictly follows
> k in trace1 and c = c’. (The domain of a function f is denoted dom(f)
> and its image image(f) = { f(x) | x ∈ dom(f)}.) 
> 
> Could u please give us some guidence? The related codes are in the
> attachment and i have added comments . Thank you for all the help.

I brought some minor modifications to your development, making it
easier to use:

=> use "String.string_dec" instead of combining "String.prefix and
String.length", it is a lot more convenient.

=> I swaped two constructors somewhere; it is just a hack, to ease
the tactics "constructor" and "econstructor" (but it is just a "hack"
which relies on how constructor works)

=> Your lemma is wrong, I give here a counter example:

============================================

Require Import String Bool List Arith  Ascii.
Open Scope nat_scope.
Open Scope string_scope.
Open Scope list_scope.

(* Identifiers *)
Inductive id : Type := 
  Id : nat -> id.

(** Shorthands for variables: *)
Definition P : id := Id 0.
Definition Q : id := Id 1.
Definition R : id := Id 2.

(** A state represents the current set of values for all the
    variables at some point . *)
Definition state := id -> bool.
Definition empty_state : state := fun _ => true. 

(* The definition specify the syntax of condition*)
Inductive cnd : Type := 
  | BVar: id -> cnd
  | BTrue : cnd
  | BFalse : cnd
  | BNot : cnd -> cnd
  | BAnd : cnd -> cnd -> cnd
  | BOr : cnd -> cnd -> cnd
  | BImp : cnd -> cnd -> cnd .

(*A event is defined as a string *)
Definition event:=string.
(*Inductive type for event with guard(condition)*)
(* I prefer to use records for that *)
Record grdevt:Type:= ge {cond : cnd; ev : event}.
(*A trace is a list of event with guard*)
Definition trace:=list grdevt.

(*Definition string_eq_bool (s1 s2 : string) : bool :=
  andb (prefix s1 s2) 
       (beq_nat (String.length s1) (String.length s2)).*)
(* use rather string_dec *)

Definition beq_event (e1:event)(e2:event):{e1 = e2}+{e1<>e2}:=
   string_dec e1 e2.

(*Evaluating a condition reduces it to bool*)
Fixpoint beval (st:state)(c : cnd) : bool :=
  match c with 
  | BVar i      => st i
  | BTrue       => true
  | BFalse      => false
  | BNot b1     => negb (beval st b1)
  | BAnd b1 b2  => andb (beval st b1) (beval st b2)
  | BOr b1 b2  => orb (beval st b1) (beval st b2)
  | BImp b1 b2  => orb (negb (beval st b1)) (beval st b2)
  (*P->Q ¡Á\u00aa\u00bb\u00bb\u00ce\u00aa not P\/Q*)
  end.

(*A relation simulation defined over two traces*)
Inductive simulation (st:state) :trace -> trace ->Prop :=
|simu_self: forall t, simulation st t t
(* I swapped the two constructors,
   so that "(e)constructor" will treat them in the right order *)
|sim_add: forall g c' e' e'' t t', 
         simulation  st (g::t) ((ge c' e')::t') -> 
              simulation st (g::t) ((ge c' e')::(ge c' e'')::t')
|sim_hd: forall  c c' e e'  t t', 
         beval st (BImp c' c)=true -> simulation st t t' ->
         (* here you can use leibnitz equality and use beq_event to
decide*) e = e' ->
              simulation st ((ge c e)::t) ((ge c' e')::t')
.

(*Test case*)
Definition traceex1 :=
  (ge (BAnd (BVar P) (BVar Q)) "e1Event")::
  (ge (BAnd (BVar P) (BVar Q)) "e2Event")::
  nil.
Definition traceex2 :=
  (ge (BVar P) "e1Event")::
  (ge (BVar Q) "e2Event")::
  (ge (BVar Q) "e2Event")::
  nil.

Example sim1: simulation empty_state traceex1 traceex2.
Proof.
  unfold traceex1. unfold traceex2.
  eapply sim_hd with (st:=empty_state).
  simpl. unfold empty_state. auto.
  eapply sim_add.
  eapply sim_hd with (st:=empty_state).
  simpl. unfold empty_state. auto.
  apply simu_self.
  auto.
  auto.
Qed.

(*The reflexive property of simulation*)
Require Import Relations.
Lemma simlation_refl:forall st:state,reflexive _ (simulation st).
Proof.
  intro st.
  unfold reflexive. apply simu_self.
Qed.

(*Aux Lemma*)
Lemma beval_trans:
forall cnd1 cnd2 cnd3 st,
beval st (BImp cnd1 cnd2) = true ->
beval st (BImp cnd2 cnd3) = true ->
beval st (BImp cnd1 cnd3)=true.
Proof.
 simpl; intros.
 destruct (negb (beval st cnd1)); simpl in *; auto.
 destruct (beval st cnd2); simpl in *; auto.
 discriminate.
Qed.

(* becomes useless:
Lemma beq_event_trans:
forall e1 e2 e3,
beq_event e1 e2 = true ->
beq_event e2 e3 = true ->
beq_event e1 e3 =true.
Proof.
Admitted.
*)

(*The transitive property of simulation*)

Definition kronecker0 := fun i => match i with Id 0 => true | _ =>
false end.

Definition embed id := {|cond := BVar id; ev := ""|}.

Lemma L1: simulation kronecker0 ((embed P)::nil) ((embed P)::(embed
P)::nil). repeat (eauto; econstructor).
Qed.

Lemma L2: simulation kronecker0 ((embed P)::(embed P)::nil) ((embed
P)::(embed Q)::nil). repeat (eauto; econstructor).
Qed.

Lemma L3: simulation kronecker0 ((embed P)::nil) ((embed P)::(embed
Q)::nil) -> False. intros.
 inversion H; clear H; simpl in *; subst.
  discriminate.
 clear - H7.
 inversion H7.
Qed.

Lemma simlation_not_trans:   (forall st:state,transitive _ (simulation
st)) -> False. intros.
 apply L3.
 refine (H _ _ _ _ L1 L2).
Qed.