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.