Require Import ssreflect.
Require Export ZArith.
Require Export List.
Require Import Language.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Ltac foo h := inversion h; subst => {h}.
(* This must be found in the library ... *)
Lemma Empty_set_elim: forall (T: Type), Empty_set -> T.
Proof. move => T h0. pose f := fun e: Empty_set => T.
have := Empty_set_rect f h0. move => h1. rewrite /f in h1.
by apply h1. Qed.
CoInductive res: Set :=
| ret: state -> res
| output: val -> res -> res
| input: (val -> res) -> res
| delay: res -> res.
CoFixpoint bot := delay bot.
Lemma io_destr: forall r, r = match r with
| ret st => ret st
| output v r' => output v r'
| input f => input f
| delay r' => delay r'
end.
Proof. by case; simpl => //. Qed.
Axiom extensionality: forall (f g: val -> res),
(forall v, f v = g v) -> f = g.
(* strong bisimilarity *)
CoInductive bism: res -> res -> Prop :=
| bism_ret: forall st,
bism (ret st) (ret st)
| bism_input: forall f0 f1,
(forall v, bism (f0 v) (f1 v)) ->
bism (input f0) (input f1)
| bism_output: forall r0 r1 v,
bism r0 r1 ->
bism (output v r0) (output v r1)
| bism_delay: forall r0 r1,
bism r0 r1 ->
bism (delay r0) (delay r1).
Lemma bism_refl: forall r, bism r r.
Proof. cofix COINDHYP. case.
- move => st. by apply bism_ret.
- move => v r. apply bism_output. apply COINDHYP.
- move => i. apply bism_input. move => v. apply COINDHYP.
- move => i. apply bism_delay. apply COINDHYP.
Qed.
Lemma bism_sym: forall r0 r1, bism r0 r1 -> bism r1 r0.
Proof.
cofix COINDHYP. move => r0 r1 h0. foo h0.
- apply bism_ret.
- apply bism_input. move => v. have := COINDHYP _ _ (H v). apply.
- apply bism_output. have := COINDHYP _ _ H; apply.
- have := bism_delay (COINDHYP _ _ H); apply.
Qed.
Lemma bism_trans: forall r0 r1 r2, bism r0 r1 -> bism r1 r2 -> bism r0 r2.
Proof.
cofix COINDHYP.
move => r0 r1 r2 h0. foo h0.
- move => h0. foo h0. apply bism_ret.
- move => h0. foo h0. apply bism_input. move => v.
have := COINDHYP _ _ _ (H v) (H1 v). apply.
- move => h0. foo h0. apply bism_output. have := COINDHYP _ _ _ H H3; apply.
- move => h0. foo h0. have := bism_delay (COINDHYP _ _ _ H H1). apply.
Qed.
Definition setoid (P: res -> Prop) :=
forall r0, P r0 -> forall r1, bism r0 r1 -> P r1.
Definition setoid2 (P: res -> res -> Prop) :=
forall r0 r1, P r0 r1 -> forall r2, bism r0 r2 -> forall r3, bism r1 r3 ->
P r2 r3.
(* head convergence *)
Inductive red: res -> res -> Prop :=
| red_ret: forall st, red (ret st) (ret st)
| red_delay: forall r0 r1, red r0 r1 -> red (delay r0) r1
| red_output: forall r0 r1 v,
bism r0 r1 -> red (output v r0) (output v r1)
| red_input: forall f g,
(forall x, bism (f x) (g x)) -> red (input f) (input g).
(* convergence is setoid *)
Lemma red_setoid: setoid2 red.
Proof. rewrite /setoid2. induction 1.
- move => r0 h0 r1 h1. foo h0. foo h1. by apply red_ret.
- move => r2 h0 r3 h1. foo h0. have := red_delay (IHred _ H1 _ h1).
by apply.
- move => r2 h0 r3 h1. foo h0. foo h1.
have := red_output _ (bism_trans (bism_trans (bism_sym H3) H) H4).
by apply.
- move => r0 h0 r1 h1. foo h0. foo h1.
have := red_input (fun v => (bism_trans (bism_trans (bism_sym (H1 v)) (H v)) (H2 v))).
by apply. Qed.
Lemma red_deterministic: forall r0 r1, red r0 r1 ->
forall r2, red r0 r2 -> bism r1 r2.
Proof. induction 1.
- move => r0 h0. foo h0. by apply bism_refl.
- move => r2 h0. foo h0. have := IHred _ H1; by apply.
- move => r2 h0. foo h0.
have := bism_output _ (bism_trans (bism_sym H) H3). by apply.
- move => r2 h0. foo h0.
have := bism_input (fun v => (bism_trans (bism_sym (H v)) (H1 v))).
by apply. Qed.
(* divergence *)
CoInductive div: res -> Prop :=
| div_delay: forall r, div r -> div (delay r).
Lemma div_setoid: setoid div.
Proof. cofix hcoind. move => r0 h0 r1 h1. foo h0. foo h1.
have := div_delay (hcoind _ H _ H1). by apply. Qed.
Lemma nonred_div: forall r, ~(exists r0, red r r0) -> div r.
Proof.
cofix COINDHYP. case.
- move => st0 h0. absurd False => //. apply h0. exists (ret st0). apply red_ret.
- move => v r h0. absurd False => //. apply h0. exists (output v r).
apply red_output. apply bism_refl.
- move => f h0. absurd False => //. apply h0. exists (input f).
apply red_input. move => v. apply bism_refl.
- move => r h0. have := div_delay (COINDHYP _ _). apply. move => [r0 h1].
apply h0. exists r0. have := red_delay h1. apply.
Qed.
(* weak bisimilarity via the head convergence *)
CoInductive wbism: res -> res -> Prop :=
| wbism_ret: forall r0 r1 st,
red r0 (ret st) -> red r1 (ret st) -> wbism r0 r1
| wbism_output: forall v r0 r0' r1 r1',
red r0 (output v r0') -> red r1 (output v r1') -> wbism r0' r1' ->
wbism r0 r1
| wbism_input: forall r0 r1 f0 f1,
red r0 (input f0) -> red r1 (input f1) -> (forall v, wbism (f0 v) (f1 v)) ->
wbism r0 r1
| wbism_delay: forall r0 r1,
wbism r0 r1 -> wbism (delay r0) (delay r1).
Lemma wbism_setoid: setoid2 wbism.
Proof.
cofix hcoind. move => r0 r1 h0 r2 h1 r3 h2. foo h0.
- have := wbism_ret (red_setoid H h1 (bism_refl _))
(red_setoid H0 h2 (bism_refl _)). by apply.
- have := wbism_output (red_setoid H h1 (bism_refl _))
(red_setoid H0 h2 (bism_refl _)) H1. by apply.
- have := wbism_input (red_setoid H h1 (bism_refl _))
(red_setoid H0 h2 (bism_refl _)) H1. by apply.
- foo h2. foo h1. have := wbism_delay (hcoind _ _ H _ H2 _ H1).
by apply.
Qed.
Lemma bism_wbism: forall r0 r1, bism r0 r1 -> wbism r0 r1.
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have := wbism_ret (red_ret _) (red_ret _). by apply.
- have := wbism_input (red_input (fun v => bism_refl _))
(red_input (fun v => bism_refl _)). apply. move => v.
apply hcoind. by apply H.
- have := wbism_output (red_output _ (bism_refl _))
(red_output _ (bism_refl _)). apply. have := hcoind _ _ H. by apply.
- apply wbism_delay. have := hcoind _ _ H. by apply.
Qed.
(* reflexivity *)
Lemma wbism_refl: forall r, wbism r r.
Proof.
move => r. have := bism_wbism (bism_refl r). by apply.
Qed.
(* symmetry *)
Lemma wbism_sym: forall r0 r1, wbism r0 r1 -> wbism r1 r0.
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have := wbism_ret H0 H. by apply.
- have := wbism_output H0 H (hcoind _ _ H1). by apply.
- have := wbism_input H0 H (fun v => hcoind _ _ (H1 v)). by apply.
- have := wbism_delay (hcoind _ _ H). by apply.
Qed.
Lemma wbism_delay_R: forall r0 r1, wbism r0 r1 -> wbism r0 (delay r1).
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have h0 := red_delay H0 => {H0}. have := wbism_ret H h0. by apply.
- have h0 := red_delay H0 => {H0}. have := wbism_output H h0 H1. by apply.
- have h0 := red_delay H0 => {H0}. have := wbism_input H h0 H1. by apply.
- have := wbism_delay (hcoind _ _ H). by apply.
Qed.
Lemma wbism_neg_delay_L: forall r0 r1, wbism (delay r0) r1 ->
wbism r0 r1.
Proof.
move => r0 r1 h0. foo h0.
- foo H. have := wbism_ret H2 H0. apply.
- foo H. have := wbism_output H3 H0 H1. by apply.
- foo H. have := wbism_input H3 H0 H1. by apply.
- have := wbism_delay_R H0. by apply.
Qed.
Lemma red_ret_wbism: forall r0 st0,
red r0 (ret st0) -> forall r1, wbism r0 r1 ->
red r1 (ret st0).
Proof.
have: forall r0 r2,
red r0 r2 ->
forall st0, bism r2 (ret st0) -> forall r1, wbism r0 r1 ->
red r1 (ret st0).
* induction 1.
- move => st0 h0 r1 h1. foo h0. foo h1. foo H. by apply H0.
foo H. foo H.
- move => st0 h0 r2 h1.
have := IHred _ h0 _ (wbism_neg_delay_L h1). by apply.
move => st0 h0. foo h0. move => st0 h0. foo h0.
move => h r0 st0 h0 r1 h1. have := h _ _ h0 _ (bism_refl _) _ h1.
by apply.
Qed.
Lemma red_output_wbism: forall r0 v0 r1, red r0 (output v0 r1) ->
forall r2, wbism r0 r2 -> exists r3, red r2 (output v0 r3) /\ wbism r1 r3.
Proof.
have: forall r0 r4, red r0 r4 ->
forall v0 r1, bism (output v0 r1) r4 ->
forall r2, wbism r0 r2 -> exists r3, red r2 (output v0 r3) /\ wbism r1 r3.
* induction 1.
- move => v0 r0 h0. foo h0.
- move => v0 r2 h0 r3 h1.
have := IHred _ _ h0 _ (wbism_neg_delay_L h1). apply.
- move => v0 r2 h0 r3 h1. foo h0. foo h1. foo H0. foo H0.
exists r1'. split; first done.
have := wbism_setoid H3 (bism_trans (bism_trans (bism_sym H5) H)
(bism_sym H1)) (bism_refl _). by apply. foo H0.
- move => v0 r0 h0. foo h0.
move => h r0 v0 r1 h0 r2 h1. have := h _ _ h0 _ _ (bism_refl _) _ h1.
by apply.
Qed.
Lemma red_input_wbism: forall r0 f0, red r0 (input f0) ->
forall r2, wbism r0 r2 ->
exists f1, red r2 (input f1) /\ (forall v, wbism (f0 v) (f1 v)).
Proof.
have: forall r0 r1, red r0 r1 ->
forall f0, bism (input f0) r1 ->
forall r2, wbism r0 r2 ->
exists f1, red r2 (input f1) /\ (forall v, wbism (f0 v) (f1 v)).
* induction 1.
- move => f0 h0. foo h0.
- move => f0 h0 r2 h1. have := IHred _ h0 _ (wbism_neg_delay_L h1).
by apply.
- move => f0 h0. foo h0.
- move => f0 h0 r0 h1. foo h0. foo h1. foo H0. foo H0.
foo H0. exists f2. split; first done. move => v.
have := wbism_setoid (H3 v) (bism_trans (bism_trans (bism_sym (H6 v))
(H v)) (bism_sym (H2 v))) (bism_refl _). by apply.
move => h r0 f0 h0 r2 h1. have := h _ _ h0 _ (bism_refl _) _ h1.
by apply.
Qed.
(* transitivity *)
Lemma wbism_trans: forall r0 r1 r2, wbism r0 r1 -> wbism r1 r2 ->
wbism r0 r2.
Proof.
cofix hcoind. move => r0 r1 r2 h0 h1; foo h0; foo h1.
- have h0 := red_deterministic H0 H1. foo h0.
have := wbism_ret H H2. by apply.
- have h0 := red_deterministic H0 H1. foo h0.
- have h0 := red_deterministic H0 H1. foo h0.
- foo H0. have h0 := red_ret_wbism H3 H1.
have := wbism_ret H (red_delay h0). by apply.
- have h0 := red_deterministic H0 H2. foo h0.
- have h0 := red_deterministic H0 H2. foo h0.
- have := wbism_output H H3 (hcoind _ _ _ H1
(wbism_setoid H4 (bism_sym H6) (bism_refl _))). by apply.
- have h0 := red_deterministic H0 H2. foo h0.
- foo H0. have [r1 [h0 h1]] := red_output_wbism H4 H2.
have := wbism_output H (red_delay h0) (hcoind _ _ _ H1 h1).
by apply.
- have h0 := red_deterministic H0 H2. foo h0.
- have h0 := red_deterministic H0 H2. foo h0.
- have h0 := red_deterministic H0 H2. foo h0.
have := wbism_input H H3 (fun v => hcoind _ _ _ (wbism_setoid (H1 v)
(bism_refl _) (H7 v)) (H4 v)). by apply.
- foo H0. have [f2 [h0 h1]] := red_input_wbism H4 H2.
have := wbism_input H (red_delay h0) (fun v => hcoind _ _ _
(H1 v) (h1 v)). by apply.
- foo H0. have h0 := red_ret_wbism H3 (wbism_sym H).
have := wbism_ret (red_delay h0) H1. by apply.
- foo H0. have [r0 [h0 h1]] := red_output_wbism H4 (wbism_sym H).
have := wbism_output (red_delay h0) H1 (hcoind _ _ _ (wbism_sym h1) H2).
by apply.
- foo H0. have [f2 [h0 h1]] := red_input_wbism H4 (wbism_sym H).
have := wbism_input (red_delay h0) H1 (fun v => hcoind _ _ _
(wbism_sym (h1 v)) (H2 v)). by apply.
- have := wbism_delay (hcoind _ _ _ H H1). by apply.
Qed.
(* weak bisimilarity via nested induction-coinduction *)
Inductive wbismi (X: res -> res -> Prop) : res -> res -> Prop :=
| wbismi_delay_L: forall r0 r1,
wbismi X r0 r1 -> wbismi X (delay r0) r1
| wbismi_delay_R: forall r0 r1,
wbismi X r0 r1 -> wbismi X r0 (delay r1)
| wbismi_ret: forall st, wbismi X (ret st) (ret st)
| wbismi_input: forall f0 f1,
(forall v, X (f0 v) (f1 v)) ->
wbismi X (input f0) (input f1)
| wbismi_output: forall v r0 r1,
X r0 r1 -> wbismi X (output v r0) (output v r1).
CoInductive wbismc: res -> res -> Prop :=
| wbismc_intro: forall (X: res -> res -> Prop) r0 r1,
(setoid2 X) ->
(forall r0 r1, X r0 r1 -> wbismc r0 r1) ->
wbismi X r0 r1 -> wbismc r0 r1
| wbismc_delay: forall r0 r1, wbismc r0 r1 -> wbismc (delay r0) (delay r1).
Lemma wbismi_monotone: forall (X Y: res -> res -> Prop),
(forall x y, X x y -> Y x y) ->
forall r0 r1, wbismi X r0 r1 -> wbismi Y r0 r1.
Proof.
move => X Y hXY. induction 1.
- have := wbismi_delay_L IHwbismi. by apply.
- have := wbismi_delay_R IHwbismi. by apply.
- by apply wbismi_ret.
- apply wbismi_input. move => v. apply hXY. done.
- apply wbismi_output. have := hXY _ _ H. by apply.
Qed.
Lemma wbismi_setoid: forall X, setoid2 X ->
setoid2 (wbismi X).
Proof.
move => X hsetoid. rewrite /setoid2. induction 1.
- move => r2 h0 r3 h1. foo h0. have h0 := IHwbismi _ H1 _ h1.
have := wbismi_delay_L h0. by apply.
- move => r2 h0 r3 h1. foo h1.
have := wbismi_delay_R (IHwbismi _ h0 _ H1). by apply.
- move => r2 h0 r3 h1. foo h0. foo h1. by apply wbismi_ret.
- move => r2 h0 r3 h1. foo h0. foo h1. apply wbismi_input.
move => v. have := hsetoid _ _ (H v) _ (H1 v) _ (H2 v). by apply.
- move => r2 h0 r3 h1. foo h0. foo h1. apply wbismi_output.
have := hsetoid _ _ H _ H3 _ H4. by apply.
Qed.
Lemma wbismc_setoid: setoid2 wbismc.
Proof.
rewrite /setoid2. cofix hcoind. move => r0 r1 h0. foo h0.
- move => r2 h0 r3 h1. have := wbismc_intro H H0. apply.
have := wbismi_setoid H H1 h0 h1. by apply.
- move => r0 h0 r1 h1. foo h0. foo h1.
have := wbismc_delay (hcoind _ _ H _ H1 _ H2). by apply.
Qed.
Lemma bism_setoid: setoid2 bism.
Proof.
rewrite /setoid2. move => r0 r1 h0 r2 h2 r3 h3.
have := (bism_trans (bism_trans (bism_sym h2) h0) h3). by apply.
Qed.
Lemma bism_wbismc: forall r0 r1, bism r0 r1 -> wbismc r0 r1.
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have := wbismc_intro bism_setoid. apply. apply hcoind.
by apply wbismi_ret.
- have := wbismc_intro bism_setoid. apply. apply hcoind.
by apply wbismi_input.
- have := wbismc_intro bism_setoid. apply. apply hcoind.
by apply wbismi_output.
- have := wbismc_delay (hcoind _ _ H). by apply.
Qed.
(* wbismc is reflexive *)
Lemma wbismc_refl: forall r, wbismc r r.
Proof.
move => r. have := bism_wbismc (bism_refl _). by apply.
Qed.
(* wbismc is symmetric *)
Lemma wbismc_sym: forall r0 r1, wbismc r0 r1 -> wbismc r1 r0.
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have h: setoid2 (fun r0 => fun r1 => wbismc r1 r0).
* rewrite /setoid2. move => r2 r3 h0 r4 h1 r5 h2.
have := wbismc_setoid h0 h2 h1. by apply.
have := wbismc_intro h. apply. move => r2 r3 h0.
have := hcoind _ _ h0. by apply. have h0 := wbismi_monotone H0 H1.
clear H0 H1 H h. move: r0 r1 h0. induction 1.
- have := wbismi_delay_R IHh0. by apply.
- have := wbismi_delay_L IHh0. by apply.
- apply wbismi_ret.
- by apply wbismi_input.
- by apply wbismi_output.
- have := wbismc_delay (hcoind _ _ H). by apply.
Qed.
Definition comp (X Y: res -> res -> Prop) (r0 r1: res) :=
exists r2, X r0 r2 /\ Y r2 r1.
Lemma comp_setoid: forall (X Y: res -> res -> Prop),
(setoid2 X) -> (setoid2 Y) -> (setoid2 (comp X Y)).
Proof.
move => X Y hX hY r0 r1 [r4 [h1 h2]] r2 h3 r3 h4. exists r4. split.
have := hX _ _ h1 _ h3 _ (bism_refl _). done.
have := hY _ _ h2 _ (bism_refl _) _ h4. done.
Qed.
Lemma wbismi_comp: forall (X Y: res -> res -> Prop),
(setoid2 X) -> (setoid2 Y) ->
forall r0 r1, wbismi X r0 r1 -> forall r2 r3, wbismi Y r2 r3 -> bism r1 r2 ->
wbismi (comp X Y) r0 r3.
Proof.
move => X Y hX hY. induction 1; induction 1; move => h0; foo h0.
- have := wbismi_delay_L (IHwbismi _ _ (wbismi_delay_L H0)
(bism_delay H3)). by apply.
- have := wbismi_delay_R (IHwbismi0 (bism_refl _)). by apply.
- have := wbismi_delay_R (IHwbismi0 (bism_input H1)). by apply.
- have := wbismi_delay_R (IHwbismi0 (bism_output _ H1)). by apply.
- have := wbismi_delay_R (IHwbismi0 (bism_delay H1)). by apply.
- have := wbismi_delay_L (IHwbismi _ _ (wbismi_ret _ _) (bism_refl _)).
by apply.
- have := wbismi_delay_L (IHwbismi _ _ (wbismi_input H0) (bism_input H3)).
by apply.
- have := wbismi_delay_L (IHwbismi _ _ (wbismi_output _ H0) (bism_output _ H3)).
by apply.
- have := IHwbismi _ _ H0 H3. by apply.
- have := wbismi_delay_R (IHwbismi0 (bism_delay H2)). by apply.
- have := wbismi_delay_R (IHwbismi (bism_refl _)). by apply.
- by apply wbismi_ret.
- have := wbismi_delay_R (IHwbismi (bism_input H2)). by apply.
- apply wbismi_input. move => v. exists (f1 v). split.
have := H v; by apply. have := hY _ _ (H0 _) _ (bism_sym (H3 _)) _ (bism_refl _).
by apply.
- have := wbismi_delay_R (IHwbismi (bism_output _ H4)). by apply.
- apply wbismi_output. exists r1. split => //.
have := hY _ _ H0 _ (bism_sym H2) _ (bism_refl _). by apply.
Qed.
Lemma wbismi_neg_delay_R: forall X,
setoid2 X ->
forall r0 r1, wbismi X r0 (delay r1) -> wbismi X r0 r1.
Proof.
move => X hsetoid.
have h: forall r0 r1, wbismi X r0 r1 -> forall r2, bism r1 (delay r2) ->
wbismi X r0 r2.
* induction 1.
- move => r2 h0. have := wbismi_delay_L (IHwbismi _ h0). by apply.
- move => r2 h0. foo h0. have := wbismi_setoid hsetoid H (bism_refl _)
H2. by apply.
- move => r0 h0. foo h0.
- move => r2 h0. foo h0.
- move => r2 h0. foo h0.
move => r0 r1 h0. have := h _ _ h0 _ (bism_refl _). by apply.
Qed.
Lemma wbismi_neg_delay_L: forall X,
setoid2 X ->
forall r0 r1, wbismi X (delay r0) r1-> wbismi X r0 r1.
Proof.
move => X hsetoid.
have h: forall r0 r1, wbismi X r0 r1 -> forall r2, bism r0 (delay r2) ->
wbismi X r2 r1.
* induction 1.
- move => r2 h0. foo h0. have := wbismi_setoid hsetoid H H2 (bism_refl _).
by apply.
- move => r2 h0. have := wbismi_delay_R (IHwbismi _ h0). by apply.
- move => r0 h0. foo h0.
- move => r2 h0. foo h0.
- move => r2 h0. foo h0.
move => r0 r1 h0. have := h _ _ h0 _ (bism_refl _). by apply.
Qed.
Lemma wbismc_delay_R: forall r0 r1, wbismc r0 r1 -> wbismc r0 (delay r1).
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have := wbismc_intro H H0. apply. have := wbismi_delay_R H1. by apply.
- have := wbismc_delay (hcoind _ _ H) . by apply.
Qed.
Lemma wbismc_delay_L: forall r0 r1, wbismc r0 r1 -> wbismc (delay r0) r1.
Proof.
cofix hcoind. move => r0 r1 h0. foo h0.
- have := wbismc_intro H H0. apply. have := wbismi_delay_L H1. by apply.
- have := wbismc_delay (hcoind _ _ H) . by apply.
Qed.
Lemma wbismc_neg_delay_L: forall r0 r1, wbismc (delay r0) r1 ->
wbismc r0 r1.
Proof.
move => r0 r1 h0. foo h0.
- have := wbismc_intro H H0. apply. have := wbismi_neg_delay_L H H1.
by apply.
- have := wbismc_delay_R H0. by apply.
Qed.
Lemma wbismc_neg_delay_R: forall r0 r1, wbismc r0 (delay r1) ->
wbismc r0 r1.
Proof.
move => r0 r1 h0. foo h0.
- have := wbismc_intro H H0. apply. have := wbismi_neg_delay_R H H1.
by apply.
- have := wbismc_delay_L H1. by apply.
Qed.
(* wbismc is transitive *)
Lemma wbismc_trans: forall r0 r1 r2, wbismc r0 r1 -> wbismc r1 r2 ->
wbismc r0 r2.
Proof.
cofix hcoind. move => r0 r1 r2 h0. foo h0; move => h0; foo h0.
- have := wbismc_intro (comp_setoid H H2). apply.
* move => r3 r4 h0. destruct h0 as [r5 [h0 h1]].
have := hcoind _ _ _ (H0 _ _ h0) (H3 _ _ h1). by apply.
* have := wbismi_comp H H2 H1 H4 (bism_refl _). by apply.
- have h := wbismi_neg_delay_R H H1.
have := wbismc_intro (comp_setoid H wbismc_setoid). apply.
* move => r1 r2 [r5 [h0 h1]]. have := hcoind _ _ _ (H0 _ _ h0) h1.
by apply.
* apply wbismi_delay_R. clear H1. move: r0 r3 h r4 H2. induction 1.
- move => r2 h0. have := wbismi_delay_L (IHh _ h0). by apply.
- move => r2 h0. have := IHh _ (wbismc_neg_delay_L h0). by apply.
- move => r2 h0. foo h0. move h: (ret st) => r0. rewrite h in H3.
move: r0 r2 H3 h. induction 1.
- move => h0. foo h0.
- move => h0. have := wbismi_delay_R (IHwbismi h0). by apply.
- move => h0. apply wbismi_ret.
- move => h0. foo h0.
- move => h0. foo h0.
- move => r2 h0. foo h0. move h: (input f1) => r0. rewrite h in H4.
move: r0 r2 H4 h. induction 1.
- move => h0. foo h0.
- move => h0. have := wbismi_delay_R (IHwbismi h0). by apply.
- move => h0. foo h0.
- move => h0. foo h0. apply wbismi_input. move => v. exists (f2 v).
split =>//. have := H3 _ _ (H4 _). by apply.
- move => h0. foo h0.
- move => r2 h0. foo h0. move h: (output v r1) => r3. rewrite h in H4.
move: r3 r2 H4 h. induction 1.
- move => h0. foo h0.
- move => h0. have := wbismi_delay_R (IHwbismi h0). by apply.
- move => h0. foo h0.
- move => h0. foo h0.
- move => h0. foo h0. apply wbismi_output. exists r2.
split =>//. have := H3 _ _ H4. by apply.
- have h := wbismi_neg_delay_L H0 H2. clear H2.
have := wbismc_intro (comp_setoid wbismc_setoid H0). apply.
* move => r0 r1 [r5 [h0 h1]]. have := hcoind _ _ _ h0 (H1 _ _ h1).
by apply.
* apply wbismi_delay_L. move: r4 r2 h r3 H. induction 1.
- move => r2 h0. have := IHh _ (wbismc_neg_delay_R h0). by apply.
- move => r2 h0. have := wbismi_delay_R (IHh _ h0). by apply.
- move => r2 h0. foo h0. move h: (ret st) => r0. rewrite h in H3.
move: r0 r2 H3 h. induction 1.
- move => h0. have := wbismi_delay_L (IHwbismi h0). by apply.
- move => h0. foo h0.
- move => h0. apply wbismi_ret.
- move => h0. foo h0.
- move => h0. foo h0.
- move => r2 h0. foo h0. move h: (input f0) => r0. rewrite h in H4.
move: r0 r2 H4 h. induction 1.
- move => h0. have := wbismi_delay_L (IHwbismi h0). by apply.
- move => h0. foo h0.
- move => h0. foo h0.
- move => h0. foo h0. apply wbismi_input. move => v. exists (f3 v).
split =>//. have := H3 _ _ (H4 _). by apply.
- move => h0. foo h0.
- move => r2 h0. foo h0. move h: (output v r0) => r3. rewrite h in H4.
move: r3 r2 H4 h. induction 1.
- move => h0. have := wbismi_delay_L (IHwbismi h0). by apply.
- move => h0. foo h0.
- move => h0. foo h0.
- move => h0. foo h0.
- move => h0. foo h0. apply wbismi_output. exists r3.
split =>//. have := H3 _ _ H4. by apply.
- have := wbismc_delay (hcoind _ _ _ H H1). by apply.
Qed.
(* the rest proves equivalence of the two definitions of *)
(* weak bisimilarity *)
Lemma red_wbismi_ret: forall tr0 tr1 st0,
red tr0 (ret st0) -> red tr1 (ret st0) ->
wbismi wbism tr0 tr1.
Proof.
have h: forall tr0 tr1, red tr0 tr1 ->
forall tr2 tr3, red tr2 tr3 ->
forall st0, bism tr1 (ret st0) -> bism tr3 (ret st0) ->
wbismi wbism tr0 tr2.
induction 1; induction 1.
- move => st1 h0 h1. foo h0. foo h1. apply wbismi_ret.
- move => st0 h0 h1. have := wbismi_delay_R (IHred _ h0 h1). by apply.
- move => st0 h0 h1. foo h1.
- move => st0 h0 h1. foo h1.
- move => st0 h1 h2. have := wbismi_delay_L (IHred _ _ _ _ h1 h2). apply.
by apply red_ret.
- move => st0 h0 h1. have := wbismi_delay_R (IHred0 _ h0 h1). by apply.
- move => st0 h0 h1. foo h1.
- move => st0 h0 h1. foo h1.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
- move => st0 h0. foo h0.
* move => tr0 tr1 st0 h0 h1. have := h _ _ h0 _ _ h1 _ _ _. apply.
apply bism_ret. apply bism_ret.
Qed.
Lemma red_wbismi_output: forall v r0 r1 r2 r3,
red r0 (output v r1) -> red r2 (output v r3) ->
wbism r1 r3 -> wbismi wbism r0 r2.
Proof.
have h: forall r0 r1, red r0 r1 ->
forall r2 r3, red r2 r3 ->
forall v r1', bism r1 (output v r1') ->
forall r3', bism r3 (output v r3') ->
wbism r1' r3' -> wbismi wbism r0 r2.
induction 1; induction 1.
- move => v0 r0 h0. foo h0.
- move => v0 r2 h0. foo h0.
- move => v0 r2 h0. foo h0.
- move => v0 r2 h0. foo h0.
- move => v0 r2 h0 r3 h1 h2. foo h1.
- move => v0 r4 h0 r5 h1 h2.
have := wbismi_delay_R (IHred0 _ _ h0 _ h1 h2). by apply.
- move => v0 r4 h0 r5 h1 h2.
have := wbismi_delay_L (IHred _ _ (red_output _ H0) _ _ h0 _ h1 h2).
by apply.
- move => v0 r2 h0 r3 h1. foo h1.
- move => v0 r2 h0 r3 h1. foo h1.
- move => v0 r4 h0 r5 h1 h2.
have := wbismi_delay_R (IHred _ _ h0 _ h1 h2). by apply.
- move => v1 r4 h0 r5 h1 h2. foo h0. foo h1. apply wbismi_output.
have := wbism_setoid _ (bism_sym (bism_trans H H2))
(bism_sym (bism_trans H0 H3)). apply. by apply h2.
- move => v1 r2 h0 r3 h1. foo h1.
- move => v0 r0 h0. foo h0.
- move => v0 r2 h0. foo h0.
- move => v0 r2 h0. foo h0.
- move => v0 r0 h0. foo h0.
move => v r0 r1 r2 r3 h0 h1 h2.
have := h _ _ h0 _ _ h1 _ _ (bism_refl _) _ (bism_refl _) h2. by apply.
Qed.
Lemma red_wbismi_input: forall r0 r1 f0 f1,
red r0 (input f0) -> red r1 (input f1) ->
(forall v, wbism (f0 v) (f1 v))-> wbismi wbism r0 r1.
Proof.
have h: forall r0 r1, red r0 r1 -> forall r2 r3, red r2 r3 ->
forall f0, bism r1 (input f0) -> forall f1, bism r3 (input f1) ->
(forall v, wbism (f0 v) (f1 v)) ->
wbismi wbism r0 r2.
* induction 1; induction 1.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0 f1 h1. foo h1.
- move => f0 h0 f1 h1 h2.
have := wbismi_delay_R (IHred0 _ h0 _ h1 h2). by apply.
- move => f0 h0 f1 h1. foo h1.
- move => f0 h0 f1 h1 h2.
have := wbismi_delay_L (IHred _ _ (red_input H0)
_ h0 _ h1 h2). by apply.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0. foo h0.
- move => f0 h0 f1 h1. foo h1.
- move => f0 h0 f1 h1 h2.
have := wbismi_delay_R (IHred _ h0 _ h1 h2). by apply.
- move => f0 h0 f1 h1. foo h1.
- move => f2 h0 f1 h1 h2. apply wbismi_input. move => v.
foo h1. foo h0.
have := wbism_setoid (h2 v) (bism_sym (bism_trans (H v) (H4 v)))
(bism_sym (bism_trans (H0 v) (H3 v))). by apply.
move => r0 r1 f0 f1 h0 h1 h2.
have := h _ _ h0 _ _ h1 _ (bism_refl _) _ (bism_refl _) h2. by apply.
Qed.
Lemma wbism_wbismc:
forall tr0 tr1, wbism tr0 tr1 -> wbismc tr0 tr1.
Proof.
cofix hcoind. move => tr0 tr1 h0. foo h0.
- have := wbismc_intro _ hcoind (red_wbismi_ret H H0). apply.
apply wbism_setoid.
- have := wbismc_intro wbism_setoid hcoind (red_wbismi_output H H0 H1). by apply.
- have := wbismc_intro wbism_setoid hcoind (red_wbismi_input H H0 H1). by apply.
- have := wbismc_delay (hcoind _ _ H). apply.
Qed.
Lemma wbismi_red: forall X r0 r1, wbismi X r0 r1 ->
(exists st0, red r0 (ret st0) /\ red r1 (ret st0))
\/ (exists f0, exists f1, red r0 (input f0) /\ red r1 (input f1)
/\ (forall v, X (f0 v) (f1 v)))
\/ (exists v0, exists r2, exists r3, red r0 (output v0 r2) /\ red r1 (output v0 r3)
/\ X r2 r3).
Proof.
induction 1.
- move: IHwbismi => [h0 | [h0 | h0]].
- move: h0 => [st0 [h0 h1]].
left. exists st0. split. have := red_delay h0. by apply. by apply h1.
- move: h0 => [f0 [f1 [h0 [h1 h2]]]]. right. left. exists f0. exists f1.
split; last split => //. have := red_delay h0. by apply.
- move: h0 => [v0 [r2 [r3 [h0 [h1 h2]]]]]. right; right. exists v0.
exists r2. exists r3. split; last split => //. have := red_delay h0; by apply.
- move: IHwbismi => [h0 | [h0 | h0]].
- move: h0 => [st0 [h0 h1]].
left. exists st0. split => //. have := red_delay h1. by apply.
- move: h0 => [f0 [f1 [h0 [h1 h2]]]]. right. left. exists f0. exists f1.
split; last split => //. apply h0. have := red_delay h1. by apply.
- move: h0 => [v0 [r2 [r3 [h0 [h1 h2]]]]]. right; right. exists v0.
exists r2. exists r3. split; last split => //. apply h0.
have := red_delay h1; by apply.
- left. exists st. split; by apply red_ret.
- right; left. exists f0. exists f1. split; last split => //.
apply red_input. move => v. apply bism_refl.
apply red_input. move => v. apply bism_refl.
- right; right. exists v. exists r0. exists r1. split; last split => //.
apply red_output. apply bism_refl.
apply red_output. apply bism_refl.
Qed.
Lemma wbismc_wbism: forall tr0 tr1,
wbismc tr0 tr1 -> wbism tr0 tr1.
Proof.
cofix hcoind. move => tr0 tr1 h0. foo h0.
- have [h0 | [h0 | h0]] := wbismi_red H1.
- move: h0 => [st0 [h0 h1]]. have := wbism_ret h0 h1. by apply.
- move: h0 => [f0 [f1 [h0 [h1 h2]]]].
have := wbism_input h0 h1 (fun v => hcoind _ _ (H0 _ _ (h2 v))). by apply.
- move: h0 => [v0 [r2 [r3 [h0 [h1 h2]]]]].
have := wbism_output h0 h1 (hcoind _ _ (H0 _ _ h2)). by apply.
- have := wbism_delay (hcoind _ _ H). by apply.
Qed.