Coq NP C-3

Variable X:Type. (*Prozesses*)
Variable A:Type. (*Transitions*)

Definition transition := X -> A -> X -> Prop.


Fixpoint tvtrace (f:transition) (p:X) xs tv :=
  match xs with
    nil => forall a, In a tv <-> exists q, f p a q
  | (a::xr) => exists q, f p a q /\ tvtrace f q xr tv
  end.

Definition tveq f p q := forall xs tv, tvtrace f p xs tv <-> tvtrace f q xs tv.

Lemma tvrefl: forall f s, tveq f s s.
Proof.
  intros f s xs tv. tauto.
Qed.

Lemma tvsym: forall f s t, tveq f s t -> tveq f t s.
Proof.
  intros f s t H xs tv.
  specialize (H xs tv).
  tauto.
Qed.

Lemma tvtrans: forall f s t u, tveq f s t -> tveq f t u -> tveq f s u.
Proof.
  intros f s t u H F xs tv.
  specialize (H xs tv).
  specialize (F xs tv).
  tauto.
Qed.

Fixpoint termtrace (f:transition) (p:X) xs :=
  match xs with
    nil => ~ exists a q, f p a q
  | (a::xr) => exists q, f p a q /\ termtrace f q xr
  end.

Definition ttraceeq f p q := forall xs, termtrace f p xs <-> termtrace f q xs.

Lemma tvToTermTrace: forall f s xs, tvtrace f s xs nil <-> termtrace f s xs.
Proof.
  intros f s xs.
  revert s.
  induction xs.
  - intros s. split.
    + intros H. intros (a&q&G).
      apply (H a). exists q. exact G.
    + intros H x.
      split.
      * intros [].
      * intros (q&F).
        apply H. exists x. now exists q.
  - intros s. split.
    + intros (q&H1&H2).
      cbn. exists q. split;trivial.
      now apply IHxs.
    + intros (q&H1&H2).
      exists q. split.
      * exact H1.
      * now apply IHxs.
Qed.


Goal forall f s t, tveq f s t -> ttraceeq f s t.
Proof.
  intros f s t H xs.
  specialize (H xs nil).
  split;intros F;apply tvToTermTrace;apply H;apply tvToTermTrace;exact F.
Qed.

Variable bisim : transition -> X -> X -> Prop.
Variable bisimDef : forall f p q, bisim f p q <->
  (forall a p2, f p a p2 -> exists q2, f q a q2 /\ bisim f p2 q2) /\
  (forall a q2, f q a q2 -> exists p2, f p a p2 /\ bisim f p2 q2).

(* Alternatively, bisim can be defined over bisimulation for a set with this property
and bisimiliarity as existence of the set and (p,q) in the set, this is equivalent
but not as nice for proves *)

Goal forall f p q, bisim f p q -> tveq f p q.
Proof.
  intros f p q H t.
  revert p q H.
  induction t.
  - intros p q H tv.
    split;intros F.
    + apply bisimDef in H as [H1 H2].
      cbn in *.
      intros a.
      split.
      * intros G.
        specialize (F a).
        destruct F as [F1 F2].
        destruct (F1 G) as [p' F].
        destruct (H1 a p' F) as [q' [H _]].
        exists q'. exact H.
      * specialize (F a). destruct F as [F1 F2].
        intros [q2 F]. apply F2.
        destruct (H2 a q2 F) as [p2 [H _]].
        exists p2. exact H.
    + apply bisimDef in H as [H1 H2].
      cbn in *.
      intros a.
      split.
      * intros G.
        specialize (F a).
        destruct F as [F1 F2].
        destruct (F1 G) as [q' F].
        destruct (H2 a q' F) as [p' [H _]].
        exists p'. exact H.
      * specialize (F a). destruct F as [F1 F2].
        intros [p2 F]. apply F2.
        destruct (H1 a p2 F) as [q2 [H _]].
        exists q2. exact H.
  - intros p q H tv. split.
    + intros (p2&F1&F2);cbn.
      apply bisimDef in H as [H1 H2].
      specialize (H1 a p2 F1).
      destruct H1 as (q2&H11&H12).
      exists q2.
      specialize (IHt p2 q2 H12).
      split;try assumption.
      now apply IHt.
    + intros (q2&F1&F2);cbn.
      apply bisimDef in H as [H1 H2].
      specialize (H2 a q2 F1).
      destruct H2 as (p2&H11&H12).
      exists p2.
      specialize (IHt p2 q2 H12).
      split;try assumption.
      now apply IHt.
Qed.






fun bisimulation where
<bisimulation f b = (
        (forall (p,q) : b. forall a p2. f p a p2 --> (exists q2. f q a q2 /\ (p2,q2) : b)) /\
        (forall (p,q) : b. forall a q2. f q a q2 --> (exists p2. f p a p2 /\ (p2,q2) : b)))>

fun bisimilar where
<bisimilar f p q = (exists b. bisimulation f b /\ (p,q) : b)>

fun isTermTrace where
<isTermTrace f p []     = (not (exists a q. f p a q))> |
<isTermTrace f p (a#xr) = (exists q. f p a q /\ isTermTrace f q xr)>

fun termEq where
<termEq f p q = (forall xs. isTermTrace f p xs <--> isTermTrace f q xs)>

fun isTVTrace where
<isTVTrace f p [] tv = (forall a. a : tv <--> (exists q. f p a q))> |
<isTVTrace f p (a#xr) tv = (exists q. f p a q /\ isTVTrace f q xr tv)>

fun tvEq where
<tvEq f p q = (forall xs tv. isTVTrace f p xs tv = isTVTrace f q xs tv)>

lemma tvrefl : <tvEq f s s>
  by simp

lemma tvsym : <tvEq f s t = tvEq f t s>
  by auto

lemma tvtrans : <tvEq f s t /\ tvEq f t u --> tvEq f s u>
  by auto

lemma tvToTerm : <isTVTrace f p xs (set []) <--> isTermTrace f p xs>
  apply (induction xs arbitrary: p)
  by auto

lemma tvTrace : <tvEq f p q --> termEq f p q>
  apply (auto simp add: tvToTerm)
  apply (auto simp flip: tvToTerm)
  done