proposition: Theorem RiceP (P : input -> Prop) : forall i, P i -> (forall M M' : machine, (forall i, Run (Call M i) true <-> Run (Call M' i) true) -> P (encode_mach M) <-> P (encode_mach M')) -> ~ P [[compile(Ret false)]] -> ~ Decidable P.
proof: Proof. intros i HPi HEquiv Hx (P_impl, P_spec). apply HALT_tm_undecidable. destruct (closure_of (fun p x => let (M, w) := decode_mach_input p in let T := decode_mach i in mlet _ <- Call M w in Call T x )) as (seq, H_seq). apply decidable_def with (p:= fun (p:input) => P_impl [[seq p]] ). apply decides_def. 2: { apply decider_def. intros k. eapply decides_to_halt; eauto. } apply recognizes_def. intros k. unfold HALT_tm. destruct (decode_mach_input k) as (M, w) eqn: r1. rewrite (decides_true_rw P_spec). split; intros Hp. { clear HPi. destruct (halt_or_loop (Call M w)) as [Hm|Hm]; auto. contradict Hx. apply HEquiv with (M:= seq k); auto. intros j. split; intros; run_simpl_all. assert (Hmw : Loop (Call (seq k) j)). { intros. rewrite (closure_of_loop_rw H_seq). rewrite r1. apply loop_seq_l. assumption. } apply run_to_halt in H. run_simpl_all. } apply HEquiv with (M:= decode_mach i). 2: { run_simpl_all. assumption. } intros l. rewrite (closure_of_run_rw H_seq). rewrite r1. rewrite halt_rw in Hp. destruct Hp as (b, Hr). rewrite (run_seq_pre_rw Hr). reflexivity. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed