Require Export picalcth.

Section monotonicity.


Axiom
  proc_mono :
    ∀ (p : name → proc) (x y : name), notin x (p y) → notin x (nu p).


Axiom
  f_act_mono :
    ∀ (a : name → f_act) (x y : name),
    f_act_notin x (a y) → f_act_notin_ho x a.

Axiom
  b_act_mono :
    ∀ (a : name → b_act) (x y : name),
    b_act_notin x (a y) → b_act_notin_ho x a.

End monotonicity.

Section expansions.


Axiom
  ho_proc_exp :
    ∀ (p : name → proc) (x : name),
    ∃ q : name → name → proc,
      notin x (nu (fun y : name ⇒ nu (q y))) ∧ p = q x.

Axiom
  ho2_proc_exp :
    ∀ (p : name → name → proc) (x : name),
    ∃ q : name → name → name → proc,
      notin x (nu (fun y : name ⇒ nu (fun z : name ⇒ nu (q y z)))) ∧
      p = q x.


Lemma proc_exp :
 ∀ (p : proc) (x : name),
 ∃ q : name → proc, notin x (nu q) ∧ p = q x.

Proof.

simple induction p; intros.

∃ (fun _ : name ⇒ nil); split;
 [ apply notin_nu; intros; apply notin_nil | try trivial ].

elim (H x); intros.
∃ (fun n : name ⇒ bang (x0 n)); split.
apply notin_nu; intros.
apply notin_bang; inversion H0.
inversion H2; auto.
inversion H0.
rewrite <- H2; trivial.

elim (H x); intros.
∃ (fun n : name ⇒ tau_pref (x0 n)); split.
apply notin_nu; intros.
apply notin_tau; inversion H0.
inversion H2; auto.
inversion H0.
rewrite <- H2; trivial.

elim (H x); elim (H0 x); intros.
inversion_clear H1; inversion_clear H2.
∃ (fun n : name ⇒ par (x1 n) (x0 n)); split.
apply notin_nu; intros.
apply notin_par; [ inversion H1; auto | inversion H3; auto ].
rewrite <- H4; rewrite <- H5; trivial.

elim (H x); elim (H0 x); intros.
inversion_clear H1; inversion_clear H2.
∃ (fun n : name ⇒ sum (x1 n) (x0 n)); split.
apply notin_nu; intros.
apply notin_sum; [ inversion H1; auto | inversion H3; auto ].
rewrite <- H4; rewrite <- H5; trivial.

elim (ho_proc_exp p0 x); intros.
inversion_clear H0; ∃ (fun n : name ⇒ nu (x0 n)); split;
 [ assumption | rewrite H2; trivial ].

elim (H x); intros.
inversion_clear H0.
elim (LEM_name x n); elim (LEM_name x n0); intros.
rewrite <- H0; rewrite <- H3; ∃ (fun n : name ⇒ match_ n n (x0 n));
 split.
apply notin_nu; intros; inversion H1; apply notin_match; auto.
rewrite H2; trivial.
rewrite <- H3; ∃ (fun n : name ⇒ match_ n n0 (x0 n)); split.
apply notin_nu; intros; inversion H1; apply notin_match; auto.
rewrite H2; trivial.
rewrite <- H0; ∃ (fun n1 : name ⇒ match_ n n1 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_match; auto.
rewrite H2; trivial.
∃ (fun n1 : name ⇒ match_ n n0 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_match; auto.
rewrite H2; trivial.

elim (H x); intros.
inversion_clear H0.
elim (LEM_name x n); elim (LEM_name x n0); intros.
rewrite <- H0; rewrite <- H3;
 ∃ (fun n1 : name ⇒ mismatch n1 n1 (x0 n1));
 split.
apply notin_nu; intros; inversion H1; apply notin_mismatch; auto.
rewrite H2; trivial.
rewrite <- H3; ∃ (fun n1 : name ⇒ mismatch n1 n0 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_mismatch; auto.
rewrite H2; trivial.
rewrite <- H0; ∃ (fun n1 : name ⇒ mismatch n n1 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_mismatch; auto.
rewrite H2; trivial.
∃ (fun n1 : name ⇒ mismatch n n0 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_mismatch; auto.
rewrite H2; trivial.

elim (ho_proc_exp p0 x); intros.
inversion_clear H0; elim (LEM_name x n); intros.
rewrite <- H0; ∃ (fun n0 : name ⇒ in_pref n0 (x0 n0)); split;
 [ apply notin_nu; intros; apply notin_in; intros;
    [ assumption
    | inversion H1; cut (notin x (nu (x0 z))); [ intro | auto ];
       inversion_clear H7; auto ]
 | rewrite H2; trivial ].
∃ (fun n0 : name ⇒ in_pref n (x0 n0)); split;
 [ apply notin_nu; intros; apply notin_in; intros;
    [ auto
    | inversion H1; cut (notin x (nu (x0 z))); [ intro | auto ];
       inversion_clear H7; auto ]
 | rewrite H2; trivial ].

elim (H x); intros.
inversion_clear H0.
elim (LEM_name x n); elim (LEM_name x n0); intros.
rewrite <- H0; rewrite <- H3;
 ∃ (fun n1 : name ⇒ out_pref n1 n1 (x0 n1));
 split.
apply notin_nu; intros; inversion H1; apply notin_out; auto.
rewrite H2; trivial.
rewrite <- H3; ∃ (fun n1 : name ⇒ out_pref n1 n0 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_out; auto.
rewrite H2; trivial.
rewrite <- H0; ∃ (fun n1 : name ⇒ out_pref n n1 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_out; auto.
rewrite H2; trivial.
∃ (fun n1 : name ⇒ out_pref n n0 (x0 n1)); split.
apply notin_nu; intros; inversion H1; apply notin_out; auto.
rewrite H2; trivial.

Qed.


Lemma f_act_exp :
 ∀ (a : f_act) (x : name),
 ∃ b : name → f_act, f_act_notin_ho x b ∧ a = b x.

Proof.

unfold f_act_notin_ho in |- *; simple induction a; intros.

∃ (fun x : name ⇒ tau); split; [ intros | trivial ].
apply f_act_notin_tau.

elim (LEM_name n x); elim (LEM_name n0 x); intros.
∃ (fun x : name ⇒ Out x x); split.
intros; apply f_act_notin_Out; auto.
rewrite H; rewrite H0; try trivial.

∃ (fun x : name ⇒ Out x n0); split.
intros; apply f_act_notin_Out; auto.
rewrite H0; try trivial.

∃ (fun x : name ⇒ Out n x); split.
intros; apply f_act_notin_Out; auto.
rewrite H; try trivial.

∃ (fun x : name ⇒ Out n n0); split;
 [ intros; apply f_act_notin_Out; auto | trivial ].

Qed.


Lemma b_act_exp :
 ∀ (a : b_act) (x : name),
 ∃ b : name → b_act, b_act_notin_ho x b ∧ a = b x.

Proof.

unfold b_act_notin_ho in |- *; simple induction a; intros.

elim (LEM_name n x); intros.
∃ (fun x : name ⇒ In x); split.
intros; apply b_act_notin_In; auto.
rewrite H; try trivial.

∃ (fun x : name ⇒ In n); split.
intros; apply b_act_notin_In; auto.
trivial.

elim (LEM_name n x); intros.
∃ (fun x : name ⇒ bOut x); split.
intros; apply b_act_notin_bOut; auto.
rewrite H; try trivial.

∃ (fun x : name ⇒ bOut n); split.
intros; apply b_act_notin_bOut; auto.
trivial.

Qed.

End expansions.


Section eq_congr.

Variable x y : name.

Axiom
  ho_proc_ext :
    ∀ (p q : name → name → proc) (x : name),
    notin x (nu (fun y : name ⇒ nu (p y))) →
    notin x (nu (fun y : name ⇒ nu (q y))) → p x = q x → p = q.

Axiom
  proc_ext :
    ∀ (p q : name → proc) (x : name),
    notin x (nu p) → notin x (nu q) → p x = q x → p = q.

Lemma proc_spec :
 ∀ p q : name → proc, p = q → ∀ x : name, p x = q x.

Proof.

intros; rewrite H; trivial.

Qed.

Lemma proc_sub_congr :
 ∀ p q : name → proc,
 notin x (nu p) → notin x (nu q) → p x = q x → p y = q y.

Proof.

intros; apply proc_spec; apply proc_ext with x; auto.

Qed.

Lemma ho_proc_sub_congr :
 ∀ p q : name → name → proc,
 notin x (nu (fun z : name ⇒ nu (p z))) →
 notin x (nu (fun z : name ⇒ nu (q z))) → p x = q x → p y = q y.

Proof.

intros;
 elim
  (unsat
     (par (nu (fun z : name ⇒ nu (p z))) (nu (fun z : name ⇒ nu (q z))))
     (cons x (cons y empty))); intros.
inversion_clear H; inversion_clear H0; inversion_clear H2; inversion_clear H0;
 inversion_clear H4; inversion_clear H2; inversion_clear H5;
 inversion_clear H6; clear H7.

apply proc_ext with x0; auto.

change ((fun n : name ⇒ p n x0) y = (fun n : name ⇒ q n x0) y) in |- *;
 apply proc_sub_congr; try apply notin_nu; intros;
 [ cut (notin x (nu (p z))) | cut (notin x (nu (q z))) | apply proc_spec ];
 auto; intro; inversion_clear H7; auto.

Qed.

Axiom
  f_act_ext :
    ∀ (a b : name → f_act) (x : name),
    f_act_notin_ho x a → f_act_notin_ho x b → a x = b x → a = b.

Lemma f_act_spec :
 ∀ a b : name → f_act, a = b → ∀ x : name, a x = b x.

Proof.

intros; rewrite H; trivial.

Qed.

Lemma f_act_sub_congr :
 ∀ a b : name → f_act,
 f_act_notin_ho x a → f_act_notin_ho x b → a x = b x → a y = b y.

Proof.

intros; apply f_act_spec; apply f_act_ext with x; auto.

Qed.

Axiom
  b_act_ext :
    ∀ (a b : name → b_act) (x : name),
    b_act_notin_ho x a → b_act_notin_ho x b → a x = b x → a = b.

Lemma b_act_spec :
 ∀ a b : name → b_act, a = b → ∀ x : name, a x = b x.

Proof.

intros; rewrite H; trivial.

Qed.

Lemma b_act_sub_congr :
 ∀ a b : name → b_act,
 b_act_notin_ho x a → b_act_notin_ho x b → a x = b x → a y = b y.

Proof.

intros; apply b_act_spec; apply b_act_ext with x; auto.

Qed.

End eq_congr.

Section eta.


Lemma PRE_ETA_EQ :
 ∀ (q : proc) (x : name) (p : name → proc),
 notin x (nu p) → q = p x → nu p = nu (fun x : name ⇒ p x).

Proof.

intro; case q; intros.

cut (p = (fun _ : name ⇒ nil)); [ intro | apply proc_ext with x; auto ].
rewrite H1; trivial.
apply notin_nu; intros; apply notin_nil.

elim (proc_exp p x); intros.
inversion_clear H1.
rewrite H3 in H0; cut (p0 = (fun n : name ⇒ bang (x0 n)));
 [ intro | apply proc_ext with x; auto ].
rewrite H1; trivial.
apply notin_nu; intros; apply notin_bang; inversion_clear H2; auto.

elim (proc_exp p x); intros.
inversion_clear H1.
rewrite H3 in H0; cut (p0 = (fun n : name ⇒ tau_pref (x0 n)));
 [ intro | apply proc_ext with x; auto ].
rewrite H1; trivial.
apply notin_nu; intros; apply notin_tau; inversion_clear H2; auto.

elim (proc_exp p x); elim (proc_exp p0 x); intros.
inversion_clear H1; inversion_clear H2.
rewrite H4 in H0; rewrite H5 in H0;
 cut (p1 = (fun n : name ⇒ par (x1 n) (x0 n)));
 [ intro | apply proc_ext with x; auto ].
rewrite H2; trivial.
apply notin_nu; intros; apply notin_par;
 [ inversion_clear H1 | inversion_clear H3 ]; auto.

elim (proc_exp p x); elim (proc_exp p0 x); intros.
inversion_clear H1; inversion_clear H2.
rewrite H4 in H0; rewrite H5 in H0;
 cut (p1 = (fun n : name ⇒ sum (x1 n) (x0 n)));
 [ intro | apply proc_ext with x; auto ].
rewrite H2; trivial.
apply notin_nu; intros; apply notin_sum;
 [ inversion_clear H1 | inversion_clear H3 ]; auto.

elim (ho_proc_exp p x); intros.
inversion_clear H1.
rewrite H3 in H0; cut (p0 = (fun n : name ⇒ nu (x0 n)));
 [ intro | apply proc_ext with x; auto ].
rewrite H1; trivial.

elim (LEM_name x n); elim (LEM_name x n0); intros.

rewrite <- H1 in H0; rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ match_ n1 n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_match; auto.

rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ match_ n1 n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_match; auto.

rewrite <- H1 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ match_ n n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_match; auto.

elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ match_ n n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_match; auto.

elim (LEM_name x n); elim (LEM_name x n0); intros.

rewrite <- H1 in H0; rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ mismatch n1 n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_mismatch; auto.

rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ mismatch n1 n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_mismatch; auto.

rewrite <- H1 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ mismatch n n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_mismatch; auto.

elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ mismatch n n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_mismatch; auto.

elim (LEM_name x n); intro.

rewrite <- H1 in H0; elim (ho_proc_exp p x); intros.
inversion_clear H2.
rewrite H4 in H0; cut (p0 = (fun n1 : name ⇒ in_pref n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H2; trivial.
apply notin_nu; intros; apply notin_in; intros; inversion_clear H3; auto.
cut (notin x (nu (x0 z))); [ intro | auto ].
inversion_clear H3; auto.

elim (ho_proc_exp p x); intros.
inversion_clear H2.
rewrite H4 in H0; cut (p0 = (fun n1 : name ⇒ in_pref n (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H2; trivial.
apply notin_nu; intros; apply notin_in; intros; inversion_clear H3; auto.
cut (notin x (nu (x0 z))); [ intro | auto ].
inversion_clear H3; auto.

elim (LEM_name x n); elim (LEM_name x n0); intros.

rewrite <- H1 in H0; rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ out_pref n1 n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_out; auto.

rewrite <- H2 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ out_pref n1 n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_out; auto.

rewrite <- H1 in H0; elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ out_pref n n1 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_out; auto.

elim (proc_exp p x); intros.
inversion_clear H3.
rewrite H5 in H0; cut (p0 = (fun n1 : name ⇒ out_pref n n0 (x0 n1)));
 [ intro | apply proc_ext with x; auto ].
rewrite H3; trivial.
apply notin_nu; intros; inversion_clear H4; apply notin_out; auto.

Qed.

Lemma ETA_EQ : ∀ p : name → proc, nu p = nu (fun x : name ⇒ p x).

Proof.

intro; elim (unsat (nu p) empty); intros.
inversion_clear H; clear H1.
apply PRE_ETA_EQ with (p x) x; auto.

Qed.


Lemma ETA_EQ2 :
 ∀ p : name → name → proc,
 nu (fun x : name ⇒ nu (p x)) =
 nu (fun x : name ⇒ nu (fun y : name ⇒ p x y)).

Proof.

intro;
 cut
  ((fun x : name ⇒ nu (p x)) = (fun x : name ⇒ nu (fun y : name ⇒ p x y)));
 [ intro; rewrite H; trivial | idtac ].
elim (unsat (nu (fun x : name ⇒ nu (p x))) empty); intros; inversion_clear H;
 clear H1.
apply proc_ext with x; auto.

Qed.

End eta.