Library Rice
Require Export Scott Acceptability.
Definition self_diverging (s : term) := ~ pi s s.
Definition self_diverging_comb := conj self_diverging closed.
Lemma self_div : ~ lacc self_diverging.
Proof.
intros H.
destruct H as [u [[cls_u lam_u] H]].
unfold self_diverging in H. specialize (H u). intuition.
Qed.
Lemma self_div_comb : ~ lacc self_diverging_comb.
Proof.
intros [u [[cls_u lam_u] H]].
unfold self_diverging_comb in H. unfold conj in H.
specialize (H u). unfold self_diverging in H.
destruct H. firstorder.
Qed.
Lemma Rice1 (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
M (lam Omega) -> ~ lacc M.
Proof with eauto; try now intuition.
intros M_proc M_cl_equiv [t2 [cls_t2 nMt2]] [t1 [cls_t1 nMt1]] MLO [u [[cls_u lam_u] Hu]].
eapply (self_div_comb).
destruct (dec_lacc ldec_closed) as [c [[cls_c lam_c] Hc]].
pose (v := lam ( u (Lam (App (tenc (lam (t2 #1))) (App #0 (Q #0)))))).
pose (v' := acc_conj c v).
exists v'; split; value.
intros s.
pose (vs := lam ((lam (t2 #1)) (s (tenc s)))).
symmetry.
transitivity (pi v s /\ closed s).
{
unfold v'. rewrite acc_conj_correct; value. firstorder intuition.
}
unfold self_diverging_comb, conj.
transitivity (pi u vs /\ closed s).
{
assert (H : u (Lam ((App (tenc (λ t2 #1))) ((App (tenc s)) (Q (tenc s))))) == u (tenc vs))
by now rewrite Q_correct, !App_correct, !Lam_correct.
split; intros [pi_v_s cls_s]; intuition;
unfold pi; revert pi_v_s; eapply converges_proper; rewrite <- H; unfold v; [symmetry | ]; crush.
}
transitivity (M vs /\ closed s).
split; intros [? ?]; intuition; try (now rewrite Hu); firstorder.
{
split.
- intros [Mvs cls_s]; intuition.
intros [w Hw].
assert (forall t, pi vs t <-> pi t2 t). {
intros t. eapply converges_proper; unfold vs; crush.
}
eapply nMt2. eapply M_cl_equiv; eassumption.
- intros [npi_s_s cls_s]; intuition.
assert (forall t, pi (lam Omega) t <-> pi vs t). {
intros t; split; intros H.
- exfalso. destruct H as [w Hw]. eapply Omega_diverges. rewrite <- Hw. symmetry. clear Hw. crush.
- exfalso. eapply npi_s_s.
assert (A: converges ((λ t2 (tenc t)) (s (tenc s)))). revert H. eapply converges_proper. symmetry. unfold vs. crush.
eapply app_converges in A. firstorder.
}
eapply M_cl_equiv; value; eassumption.
}
Qed.
Lemma Rice2 (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
~ M (lam Omega) -> ~ lacc (complement M).
Proof.
intros M_cls M_cl_equiv [t2 [cls_t2 nMt2]] [t1 [cls_t1 nMt1]] nMLO decM.
destruct decM as [u [[cls_u lam_u] Hu]]. unfold complement in Hu.
eapply (self_div_comb).
destruct (dec_lacc ldec_closed) as [c [[cls_c lam_c] Hc]].
pose (v := lam ( u (Lam (App (tenc (lam (t1 #1))) (App #0 (Q #0)))))).
pose (v' := acc_conj c v).
exists v'; split; value.
intros s.
pose (vs := lam ((lam (t1 #1)) (s (tenc s)))).
symmetry.
transitivity (pi v s /\ closed s).
{
unfold v'. rewrite acc_conj_correct; value. firstorder intuition.
}
unfold self_diverging_comb, conj.
transitivity (pi u vs /\ closed s).
{
assert (H : u (Lam ((App (tenc (λ t1 #1))) ((App (tenc s)) (Q (tenc s))))) == u (tenc vs))
by now rewrite Q_correct, !App_correct, !Lam_correct.
split; intros [pi_v_s cls_s]; intuition;
unfold pi; revert pi_v_s; eapply converges_proper; rewrite <- H; unfold v; [symmetry | ]; crush.
}
transitivity (~ M vs /\ closed s).
{
split; intros [? ?]; try (rewrite Hu); intuition; firstorder.
}
{
split.
- intros [Mvs cls_s]; intuition.
intros [w Hw].
assert (forall t, pi t1 t <-> pi vs t). {
intros t. symmetry. eapply converges_proper. unfold vs.
transitivity ((λ t1 (tenc t)) (s (tenc s))). crush. rewrite Hw. crush.
}
eapply Mvs. eapply M_cl_equiv; value; eassumption.
- intros [npi_s_s cls_s]; intuition.
assert (forall t, pi (lam Omega) t <-> pi vs t). {
intros t; split; intros A.
- exfalso. destruct A as [w Hw]. eapply Omega_diverges. rewrite <- Hw. symmetry. clear Hw. crush.
- exfalso. eapply npi_s_s.
assert (B: converges ((λ t1 (tenc t)) (s (tenc s)))). revert A. eapply converges_proper. symmetry. unfold vs. crush.
eapply app_converges in B. firstorder.
}
eapply nMLO.
eapply M_cl_equiv; try (symmetry); eauto.
}
Qed.
Theorem Rice (M : term -> Prop) : (M <=1 proc) ->
(forall (s t : term), proc t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, proc p /\ ~ M p) -> (exists p, proc p /\ M p) ->
~ ldec M.
Proof.
intros. intros A. assert (B : ldec M) by eassumption. destruct A as [u [proc_u Hu]].
destruct (Hu (lam Omega)).
- eapply Rice1; try eassumption. tauto. eapply dec_lacc. exists u; tauto.
- eapply Rice2; try eassumption. tauto. eapply dec_lacc. eapply ldec_complement. exists u; tauto.
Qed.
Lemma lamOmega s : ~ pi (lam Omega) s.
Proof.
intros A. destruct A as [? H]. eapply Omega_diverges. symmetry in H; symmetry; crush.
Qed.
Goal ~ ldec (fun s => proc s /\ forall t, pi s t).
Proof.
eapply Rice.
- firstorder.
- firstorder.
- exists (lam Omega). split; value. intros [_ A]. eapply lamOmega; eauto.
- exists (lam I). repeat split; value. intros t; eexists; crush.
Grab Existential Variables. repeat econstructor.
Qed.
Goal ~ lacc (fun s => proc s /\ exists t, ~ pi s t).
Proof.
eapply Rice1.
- firstorder.
- intros s t cls_t [cls_s [t0 H]] He. split; eauto.
exists t0. rewrite <- He. eassumption.
- exists (lam I). split; value. intros [_ [? H]]. eapply H. eexists; crush.
- exists (lam Omega). repeat split; value. exists I. eapply lamOmega.
- split; value. exists I. eapply lamOmega.
Qed.
Theorem Rice_classical (M : term -> Prop) : (M <=1 closed) ->
(forall (s t : term), closed t -> M s -> (forall u, pi s u <-> pi t u) -> M t) ->
(exists p, closed p /\ ~ M p) -> (exists p, closed p /\ M p) ->
~ ldec M.
Proof.
intros. eapply Scott.
- firstorder.
- intros. eapply H0; try eassumption. intros. unfold pi. now rewrite H5.
- destruct H2; eauto.
- destruct H2; eauto.
Qed.