Definitions

Reductions and Undecidability

Require Import Single_TM Prelim.

Definition red (X Y:Type) (p: X -> Prop) (q: Y -> Prop) :=
  exists (f: X -> Y ), (forall x:X, p x <-> q (f x)).

Lemma red_trans (X Y Z: Type) (p: X -> Prop) (q: Y -> Prop) (r: Z -> Prop) :
  red p q -> red q r -> red p r.
Proof.
  intros [f HF] [g HG]. exists (fun x => g (f x)). intros x. split.
  intros PH. now apply HG, HF. intros HR. now apply HF, (HG (f x)).
Qed.

Definition undecidable (Z:Type) (Q: Z -> Prop) : Prop := red HaltD Q.