# Library Por

Require Export Eval.

# Definition of parallel or

Definition Por' := R (.\ "p", "n", "s", "t";
!Eva "n" "s" !(lam(lam(true)))
(!Eva "n" "t" !(lam(lam(false))) (.\"x"; ("p" (!Succ "n") "s" "t"))) !I).

Definition Por'2 := R (lam (lam (lam (lam (
Eva #2 #1 (lam(lam(true)))
(Eva #2 #0 (lam(lam(false))) (lam (#4 (Succ #3) #2 #1))) I ))))).

Hint Unfold Por'.

Lemma Por'_rec n s t: Por' (enc n) (tenc s) (tenc t) ==
Eva (enc n) (tenc s) (lam(lam(true)))
(Eva (enc n) (tenc t) (lam(lam(false))) (lam ((lam(Por'#0)) (Succ (enc n)) (tenc s) (tenc t)))) I.

Proof.

crush.

Qed.

Definition Por := Por' (enc 0).

Lemma Por'_n_Sn n s t : converges (Por' (enc n) (tenc s) (tenc t)) <-> converges ( Por' (enc (S n)) (tenc s) (tenc t)).

Proof.

destruct (eva n s) eqn:Hs.

- rewrite !Por'_rec, !Eva_correct, Hs, (eva_n_Sn Hs); split; destruct (eva (S n) t), (eva n t); eexists; crush.

- destruct (eva n t) eqn: Ht.

+ rewrite !Por'_rec, !Eva_correct, Hs, Ht, (eva_n_Sn Ht).
split; destruct (eva (S n) s); eexists; crush.
+ assert (Por' (enc n) (tenc s) (tenc t) ==Por' (enc (S n)) (tenc s) (tenc t)).

rewrite Por'_rec, !Eva_correct, Hs, Ht.
crush. now rewrite H.
Qed.

Lemma Por'_n_conv n s t: converges (Por' (enc 0) (tenc s) (tenc t)) <-> converges ( Por' (enc n) (tenc s) (tenc t)).

Proof.

induction n.

- reflexivity.

- rewrite IHn.
eapply Por'_n_Sn.
Qed.

Lemma Por_correct_1a s t : converges s -> converges (Por (tenc s) (tenc t)).

Proof.

intros [s' Hs].
unfold Por.
destruct (equiv_eva Hs) as [n H].

rewrite (Por'_n_conv n).
exists (lam #1). rewrite Por'_rec, Eva_correct, H, Eva_correct.
destruct (eva n t); crush.

Qed.

Hint Unfold converges.

Lemma Por_correct_1b s t : converges t -> converges( Por (tenc s) (tenc t)).

Proof.

intros [t' Ht].

destruct (equiv_eva Ht) as [n H].
unfold Por.
rewrite (Por'_n_conv n).
destruct (eva n s) eqn:Hs';
[exists (lam #1) | exists I ]; rewrite Por'_rec, Eva_correct, Eva_correct, H, Hs'; crush.

Qed.

Lemma Por_correct_1 s t : converges s \/ converges t -> converges (Por (tenc s) (tenc t)).

Proof.

intros [convs | convt]; eauto using Por_correct_1a, Por_correct_1b.

Qed.

Lemma Por_correct_2' s t n : converges (Por' (enc n) (tenc s) (tenc t)) -> Por' (enc n) (tenc s) (tenc t) == true /\ converges s \/ Por' (enc n) (tenc s) (tenc t) == false /\ converges t.

Proof with eauto.

intros H.
destruct H as [u H].
eapply equiv_lambda, star_pow in H.
destruct H as [m H].
revert n H.

eapply complete_induction with (x := m).
clear m; intros m IHm n H'.
destruct (eva n s) eqn:Hs, (eva n t) eqn:Ht.

- left.
rewrite Por'_rec, Eva_correct, Hs, Eva_correct, Ht. split. crush.
destruct (eva_lam Hs); subst.
exists x. eapply eva_equiv. eassumption.
- left.
rewrite Por'_rec, Eva_correct, Hs, Eva_correct, Ht. split. crush.
destruct (eva_lam Hs); subst.
exists x. eapply eva_equiv. eassumption.
- right.
rewrite Por'_rec, Eva_correct, Hs, Eva_correct, Ht. split. crush.
destruct (eva_lam Ht); subst.
exists x. eapply eva_equiv. eassumption.
- assert (Por' (enc n) (tenc s) (tenc t) == Por' (enc (S n)) (tenc s) (tenc t)).

rewrite Por'_rec, Eva_correct, Hs, Eva_correct, Ht.

transitivity ((((lam (Por' #0)) (Succ (enc n))) (tenc s)) (tenc t)).
crush.
rewrite Succ_correct.
crush.
assert (A : exists k, pow step (S k) (((Por' (enc n)) (tenc s)) (tenc t)) (((Por' (enc (S n))) (tenc s)) (tenc t))). {

eapply powSk.
unfold Por'. reduce.
transitivity ( Eva (enc n) (tenc s) (lam(lam(true)))
(Eva (enc n) (tenc t) (lam(lam(false))) (lam ((lam (Por' #0)) (Succ (enc n)) (tenc s) (tenc t)))) I ).
simpl. crush.
transitivity (I (Eva (enc n) (tenc t) (Î» (Î» false))
(Î» (Î» Por' #0) (Succ (enc n)) (tenc s) (tenc t))) I).

assert( A: Eva (enc n) (tenc s) >* none).
eapply equiv_lambda. rewrite Eva_correct, Hs. reflexivity. eapply star_trans. do 3 eapply star_trans_l. eassumption.
crush.

eapply star_trans.

assert( B: Eva (enc n) (tenc t) >* none).
eapply equiv_lambda. rewrite Eva_correct, Ht. reflexivity.
eapply star_trans.
eapply star_trans_l. eapply star_trans_r. do 2 eapply star_trans_l. eassumption. crush.
transitivity ((Î» Por' #0) (Succ (enc n)) (tenc s) (tenc t)).
crush.
crush.

}
destruct A as [k A].

destruct (pow_trans_lam H' A) as [l [l_lt_m B]].

rewrite H.
eapply IHm...
Qed.

Lemma Por_correct_2 s t : converges (Por (tenc s) (tenc t)) ->
Por (tenc s) (tenc t) == true /\ converges s \/ Por (tenc s) (tenc t) == false /\ converges t.

Proof.

eapply Por_correct_2'.

Qed.

Lemma Por_correct_true s t : Por (tenc s) (tenc t) == true -> converges s.

Proof.

intros H.

assert (A : converges (Por(tenc s) (tenc t))) by ( rewrite H; eexists; crush ).

destruct (Por_correct_2 A) as [ | B].

- intuition.

- exfalso.
rewrite H in B. eapply true_equiv_false. intuition.
Qed.

Lemma Por_correct_false s t : Por (tenc s) (tenc t) == false -> converges t.

Proof.

intros H.

assert (A : converges (Por(tenc s) (tenc t))) by ( rewrite H; eexists; crush ).

destruct (Por_correct_2 A) as [B | B].

- exfalso.
rewrite H in B. eapply true_equiv_false. intuition.
- intuition.

Qed.