proposition: Theorem Rice (P : input -> Prop) (nt: Nontrivial P): (forall M M', (forall i, Run (Call M i) true <-> Run (Call M' i) true) -> P (encode_mach M) <-> P (encode_mach M')) -> ~ Decidable P.
proof: Proof. intros HEquiv Hp. inversion nt as [i j Hpi Hpj]. assert (Hx: P [[compile (Ret false)]] \/ ~P [[compile (Ret false)]]). { destruct Hp. eapply decides_or; eauto. } destruct Hx as [Hx|Hx]. 2: { contradict Hp. eapply RiceP; eauto. } assert (H: ~ Decidable (compl P)). { apply RiceP with j. - unfold compl. assumption. - intros; unfold compl. split; intros. + intros N. contradict H0. apply HEquiv with (M:= M'); auto. intros x. rewrite H; reflexivity. + contradict H0. apply HEquiv with (M:= M). * intros x. rewrite H; reflexivity. * assumption. - intros N. contradiction. } apply decidable_to_compl in Hp. contradiction. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed