Library Por
Require Export Eval.
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.