proposition: Lemma decidable_to_compl: forall L, Decidable L -> Decidable (compl L).
proof: Proof. intros. destruct H as (p, H). apply decidable_def with (p:=fun i => mlet b <- p i in Ret (negb b)). apply decides_def. - unfold compl. split; intros. { intros N. assert (Run (p i) true) by eauto using decides_in_to_run_true. inversion H0; subst; clear H0. run_simpl_all. } assert (Run (p i) false) by eauto using decides_not_in_to_run_false. eapply run_seq; eauto. constructor. - apply decider_def. intros. assert (Ha: Halt (p i)) by eauto using decides_to_halt. rewrite halt_rw in Ha. destruct Ha as (b, Ha). econstructor; eauto. constructor. Qed.
imports: Turing Coq.Bool.Bool