The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Hi, all,
  we're writing to seek advice on a question which bothers us quite a while. We're using Coq to define the "simulation" relation on two traces, but get stuck when proving the lemma  "SimulationExist":
Lemma SimulationExist : forall st c, exists c', forall a b z, simulation st a b ¡ú
                simulation st (sel c a z) (sel c' b z).
We think it is true:
when "simulation st a b" exists and the function of "sel" in c  is used to construct the interleave of two traces(a and z) , the function of "sel" in c' should construct the interleave of b and z in the same way as the previous one.
We have no idea about how to construct such c' in Coq, any suggestions are appreciated.
   The detail codes are as follows, you can also find them in the attachment. Thanks in advance.
===================
Require Import String List Compare_dec Coq.Unicode.Utf8.
Definition Pset (A:Type) := A ¡ú Prop.
(*A event is defined as a string *)
Definition event:=string.
Inductive id : Type :=
  Id : nat ¡ú id.
Inductive cnd : Type :=
  | BVar: id ¡ú cnd
  | BTrue : cnd
  | BFalse : cnd
  | BImp : cnd ¡ú cnd ¡ú cnd.
(*Inductive type for event with guard(condition)*)
Inductive core:Type:=
|ev: event¡úcore
|cd: cnd¡úcore.
(*A trace is defined as list of core*)
Definition trace := list core.
Definition obligation := Pset trace.
Notation "'¦Å'" := (@nil core).
Notation "x ¡¤ ¦Í" := (@cons core x ¦Í) (at level 60, right associativity).

(*1.the following part is to implement the formal definitions
  of "interleave operator":
Let ¦² be an alphbet. Let x,y ¡Ê ¦² and ¦Ì,v ¡Ê¦²*,
the definition of the interleave operator ¡ì is as follows:
¦Å¡ì¦Ì = ¦Ì¡ì¦Å = ¦Ì
x¦Ì¡ìyv = {x}¡¤(¦Ì¡ìyv) ¡È {y}¡¤(x¦Ì¡ìv)
where ¡¤ is the concatenation operator.
*)
Reserved Notation "x ¡ì y" (at level 5).
Notation "a ¡Ê s" := ((s:Pset _) a) (at level 10).
Notation "[ x | P ]" := (fun x => P).
Inductive interleave : trace ¡ú trace ¡ú obligation :=
| ¦Årule : ¦Å ¡Ê ¦Å ¡ì ¦Å
| lrule : forall x ¦Í ¦Ì ¦Ó, ¦Ó ¡Ê ¦Í ¡ì ¦Ì ¡ú (x¡¤¦Ó) ¡Ê (x¡¤¦Í) ¡ì ¦Ì
| rrule : forall ¦Í y ¦Ì ¦Ó, ¦Ó ¡Ê ¦Í ¡ì ¦Ì ¡ú (y¡¤¦Ó) ¡Ê ¦Í ¡ì (y¡¤¦Ì)
where "x ¡ì y" := (interleave x y).

(*2.the definition of choice:
the function "sel" is used to construct interleave of two traces,
the "spe" is used to restrict the result of "sel"
*)
Record choice := cho
 { sel : trace ¡ú trace ¡ú trace
 ; spe : forall t1 t2, (sel t1 t2) ¡Ê t1¡ìt2
 }.

(*3.the definition of "simulation" relation which is based on "trace"*)
Definition state := id -> bool.
Fixpoint beval (st:state)(c : cnd) : bool :=
  match c with
  | BVar i      => st i
  | BTrue       => true
  | BFalse      => false
  | BImp b1 b2  => orb (negb (beval st b1)) (beval st b2)
    (*translate [P->Q] into [(not P)\/Q]*)
  end.
Inductive simulation(st:state) :trace -> trace ->Prop :=
  |simu_foundation: simulation  st ¦Å ¦Å
  |sim_cnd: forall c c' t t', beval st (BImp c' c)=true ->
             simulation  st t t' ->
             simulation  st ((cd c)¡¤t) ((cd c')¡¤t')
  |sim_ev:  forall t t' e , simulation st t t' ->
             simulation  st ((ev e)¡¤t) ((ev e)¡¤t')
  |sim_add: forall e t t',  simulation st t t' -> 
             simulation  st t ((ev e)¡¤t').

Require Import Relations.
(*
we've proved the following two lemmas, but omitted the proofs for clarity*)
Lemma SimulationReflxive:forall st:state,reflexive _ (simulation st).
Admitted.
Lemma SimulationTransitive: (forall st:state,transitive _ (simulation st)).
Admitted.

Definition trace_dec:forall (a b:trace) ,{a = b} + {a <> b}.
   repeat decide equality.
Defined.

(*4.the properties of "simulation" .
we get stuck in this lemma. We think it is true:
when "simulation st a b" exists and the function of "sel" in c
is used to construct the interleave of two traces(a and z) , the function of "sel"
in c' should construct the interleave of b and z in the same way as the previous one.
We have no idea about how to construct such c' in Coq,
any suggestions are appreciated.
*)
Lemma SimulationExist:forall st c, exists c', forall a b z, simulation st a b ¡ú
                simulation st (sel c a z) (sel c' b z).
Proof.
  intros st c.
 

============
Best regards,
Lisa

Require Import String List Compare_dec Coq.Unicode.Utf8.
Definition Pset (A:Type) := A → Prop.
(*A event is defined as a string *)
Definition event:=string.
Inductive id : Type := 
  Id : nat → id.
Inductive cnd : Type :=
  | BVar: id → cnd
  | BTrue : cnd
  | BFalse : cnd
  | BImp : cnd → cnd → cnd.
(*Inductive type for event with guard(condition)*)
Inductive core:Type:=
|ev: event→core
|cd: cnd→core.
(*A trace is defined as list of core*)
Definition trace := list core.
Definition obligation := Pset trace.
Notation "'ε'" := (@nil core).
Notation "x · ν" := (@cons core x ν) (at level 60, right associativity).

(*1.the following part is to implement the formal definitions
  of "interleave operator":
Let Σ be an alphbet. Let x,y ∈ Σ and μ,v ∈Σ*, 
the definition of the interleave operator § is as follows:
ε§μ = μ§ε = μ
xμ§yv = {x}·(μ§yv) ∪ {y}·(xμ§v)
where · is the concatenation operator.
*)
Reserved Notation "x § y" (at level 5).
Notation "a ∈ s" := ((s:Pset _) a) (at level 10).
Notation "[ x | P ]" := (fun x => P).
Inductive interleave : trace → trace → obligation :=
| εrule : ε ∈ ε § ε
| lrule : forall x ν μ τ, τ ∈ ν § μ → (x·τ) ∈ (x·ν) § μ
| rrule : forall ν y μ τ, τ ∈ ν § μ → (y·τ) ∈ ν § (y·μ)
where "x § y" := (interleave x y).

(*2.the definition of choice:
the function "sel" is used to construct interleave of two traces,
the "spe" is used to restrict the result of "sel"
*)
Record choice := cho
 { sel : trace → trace → trace
 ; spe : forall t1 t2, (sel t1 t2) ∈ t1§t2
 }.


(*3.the definition of "simulation" relation which is based on "trace"*)
Definition state := id -> bool.
Fixpoint beval (st:state)(c : cnd) : bool :=
  match c with 
  | BVar i      => st i
  | BTrue       => true
  | BFalse      => false
  | BImp b1 b2  => orb (negb (beval st b1)) (beval st b2)
    (*translate [P->Q] into [(not P)\/Q]*)
  end.
Inductive simulation(st:state) :trace -> trace ->Prop :=
  |simu_foundation: simulation  st ε ε
  |sim_cnd: forall c c' t t', beval st (BImp c' c)=true -> 
             simulation  st t t' ->
             simulation  st ((cd c)·t) ((cd c')·t')
  |sim_ev:  forall t t' e , simulation st t t' ->
             simulation  st ((ev e)·t) ((ev e)·t')
  |sim_add: forall e t t',  simulation st t t' ->  
             simulation  st t ((ev e)·t').

Require Import Relations.
(*
we've proved the following two lemmas, but omitted the proofs for clarity*)
Lemma SimulationReflxive:forall st:state,reflexive _ (simulation st).
Admitted.
Lemma SimulationTransitive: (forall st:state,transitive _ (simulation st)).
Admitted.

Definition trace_dec:forall (a b:trace) ,{a = b} + {a <> b}.
   repeat decide equality. 
Defined.


(*4.the properties of "simulation" .
we get stuck in this lemma. We think it is true:
when "simulation st a b" exists and the function of "sel" in c 
is used to construct the interleave of two traces(a and z) , the function of 
"sel"
in c' should construct the interleave of b and z in the same way as the 
previous one.
We have no idea about how to construct such c' in Coq,
any suggestions are appreciated.
*)
Lemma SimulationExist:forall st c, exists c', forall a b z, simulation st a b 
→
                simulation st (sel c a z) (sel c' b z).
Proof.
  intros st c.