From VLSM.Lib Require Import SsrExport.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Ltac invs h := inversion h; subst => {h}.

Section sec_traces.

Context {A B : Type}.

CoInductive trace : Type :=
| Tnil : A -> trace
| Tcons : A -> B -> trace -> trace.

Definition hd tr :=
match tr with
| Tnil a => a
| Tcons a b tr0 => a
end.

Definition trace_decompose (tr : trace) : trace :=
match tr with
| Tnil a => Tnil a
| Tcons a b tr' => Tcons a b tr'
end.

Lemma trace_destr : forall tr, tr = trace_decompose tr.
A, B: Type
forall tr : trace, tr = trace_decompose tr
Proof.
A, B: Type
forall tr : trace, tr = trace_decompose tr by case. Qed.

CoInductive bisim : trace -> trace -> Prop :=
| bisim_nil : forall a,
   bisim (Tnil a) (Tnil a)
| bisim_cons : forall a b tr tr',
   bisim tr tr' ->
   bisim (Tcons a b tr) (Tcons a b tr').

Lemma bisim_refl : forall tr, bisim tr tr.
A, B: Type
forall tr : trace, bisim tr tr
Proof.
A, B: Type
forall tr : trace, bisim tr tr
cofix CIH.
A, B: Type
CIH: forall tr : trace, bisim tr tr
forall tr : trace, bisim tr tr
case => [a | a b tr]; first exact: bisim_nil.
A, B: Type
CIH: forall tr : trace, bisim tr tr
a: A
b: B
tr: trace
bisim (Tcons a b tr) (Tcons a b tr)
exact/bisim_cons/CIH.
Qed.

Lemma bisim_sym : forall tr1 tr2, bisim tr1 tr2 -> bisim tr2 tr1.
A, B: Type
forall tr1 tr2 : trace, bisim tr1 tr2 -> bisim tr2 tr1
Proof.
A, B: Type
forall tr1 tr2 : trace, bisim tr1 tr2 -> bisim tr2 tr1
cofix CIH.
A, B: Type
CIH: forall tr1 tr2 : trace, bisim tr1 tr2 -> bisim tr2 tr1
forall tr1 tr2 : trace, bisim tr1 tr2 -> bisim tr2 tr1
case => [a | a b tr1] tr2 Hbs; invs Hbs; first exact: bisim_nil.
A, B: Type
CIH: forall tr1 tr2 : trace, bisim tr1 tr2 -> bisim tr2 tr1
a: A
b: B
tr1, tr': trace
H3: bisim tr1 tr'
bisim (Tcons a b tr') (Tcons a b tr1)
exact/bisim_cons/CIH.
Qed.

Lemma bisim_trans : forall tr1 tr2 tr3,
 bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3.
A, B: Type
forall tr1 tr2 tr3 : trace,
bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3
Proof.
A, B: Type
forall tr1 tr2 tr3 : trace,
bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3
cofix CIH.
A, B: Type
CIH: forall tr1 tr2 tr3 : trace, bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3
forall tr1 tr2 tr3 : trace,
bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3
case => [a | a b tr1] tr2 tr0 Hbs Hbs'; invs Hbs; invs Hbs'; first exact: bisim_nil.
A, B: Type
CIH: forall tr1 tr2 tr3 : trace, bisim tr1 tr2 -> bisim tr2 tr3 -> bisim tr1 tr3
a: A
b: B
tr1, tr', tr'0: trace
H3: bisim tr1 tr'
H4: bisim tr' tr'0
bisim (Tcons a b tr1) (Tcons a b tr'0)
exact: (bisim_cons _ _ (CIH _ _ _ H3 H4)).
Qed.

Lemma bisim_hd : forall tr0 tr1, bisim tr0 tr1 -> hd tr0 = hd tr1.
A, B: Type
forall tr0 tr1 : trace,
bisim tr0 tr1 -> hd tr0 = hd tr1
Proof.
A, B: Type
forall tr0 tr1 : trace,
bisim tr0 tr1 -> hd tr0 = hd tr1 by move => tr0 tr1 []. Qed.

CoFixpoint trace_append (tr tr' : trace) : trace :=
match tr with
| Tnil a => tr'
| Tcons a b tr0 => Tcons a b (trace_append tr0 tr')
end.

#[local] Infix "+++" := trace_append (at level 60, right associativity).

Lemma trace_append_nil : forall a tr, (Tnil a) +++ tr = tr.
A, B: Type
forall (a : A) (tr : trace), Tnil a +++ tr = tr
Proof.
A, B: Type
forall (a : A) (tr : trace), Tnil a +++ tr = tr
move => a tr.
A, B: Type
a: A
tr: trace
Tnil a +++ tr = tr
rewrite [Tnil a +++ tr]trace_destr.
A, B: Type
a: A
tr: trace
trace_decompose (Tnil a +++ tr) = tr
by case tr.
Qed.

Lemma trace_append_cons : forall a b tr tr',
 (Tcons a b tr) +++ tr' = Tcons a b (tr +++ tr').
A, B: Type
forall (a : A) (b : B) (tr tr' : trace),
Tcons a b tr +++ tr' = Tcons a b (tr +++ tr')
Proof.
A, B: Type
forall (a : A) (b : B) (tr tr' : trace),
Tcons a b tr +++ tr' = Tcons a b (tr +++ tr')
move => a b tr tr'.
A, B: Type
a: A
b: B
tr, tr': trace
Tcons a b tr +++ tr' = Tcons a b (tr +++ tr')
rewrite [Tcons a b tr +++ tr']trace_destr.
A, B: Type
a: A
b: B
tr, tr': trace
trace_decompose (Tcons a b tr +++ tr') =
Tcons a b (tr +++ tr')
by case tr.
Qed.

Lemma trace_append_bism : forall tr1 tr2 tr3 tr4,
 bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4).
A, B: Type
forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
Proof.
A, B: Type
forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
cofix CIH.
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
move => tr1 tr2 tr3 tr4 [a1 | a1 b1 tr1' tr2' Hbs1'] Hbs2.
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
Hbs2: bisim tr3 tr4
bisim (Tnil a1 +++ tr3) (Tnil a1 +++ tr4)
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 ->
bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 tr1' +++ tr3)
  (Tcons a1 b1 tr2' +++ tr4)
-
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
Hbs2: bisim tr3 tr4
bisim (Tnil a1 +++ tr3) (Tnil a1 +++ tr4)
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 ->
bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 tr1' +++ tr3)
  (Tcons a1 b1 tr2' +++ tr4) rewrite 2!trace_append_nil.
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
Hbs2: bisim tr3 tr4
bisim tr3 tr4
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 ->
bisim tr3 tr4 ->
bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 tr1' +++ tr3)
  (Tcons a1 b1 tr2' +++ tr4) exact: Hbs2.
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 tr1' +++ tr3)
  (Tcons a1 b1 tr2' +++ tr4)
-
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 tr1' +++ tr3)
  (Tcons a1 b1 tr2' +++ tr4) rewrite 2!trace_append_cons.
A, B: Type
CIH: forall tr1 tr2 tr3 tr4 : trace,
bisim tr1 tr2 -> bisim tr3 tr4 -> bisim (tr1 +++ tr3) (tr2 +++ tr4)
tr1, tr2, tr3, tr4: trace
a1: A
b1: B
tr1', tr2': trace
Hbs1': bisim tr1' tr2'
Hbs2: bisim tr3 tr4
bisim (Tcons a1 b1 (tr1' +++ tr3))
  (Tcons a1 b1 (tr2' +++ tr4))
  exact/bisim_cons/CIH.
Qed.

End sec_traces.

Infix "+++" := trace_append (at level 60, right associativity).