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.