Require Export PCF2.external.Synthetic.Definitions.
Require Import PCF2.external.Synthetic.DecidabilityFacts.
Require Import PCF2.external.Synthetic.ReducibilityFacts.
Require Import PCF2.external.TM.SBTM.

Definition undecidable {X} (p : X -> Prop) :=
  decidable p -> enumerable (complement SBTM_HALT).

Lemma undecidability_from_reducibility {X} {p : X -> Prop} {Y} {q : Y -> Prop} :
  undecidable p -> p ⪯ q -> undecidable q.
Proof.
  unfold undecidable, decidable, decider, reduces, reduction, reflects.
  intros H [f Hf] [d Hd]. eapply H. exists (fun x => d (f x)). intros x. rewrite Hf. eapply Hd.
Qed.

Lemma undecidability_from_complement {X} {p : X -> Prop} :
  undecidable (complement p) -> undecidable p.
Proof.
  intros H Hp. now apply H, dec_compl.
Qed.

Lemma undecidability_to_complement {X} {p : X -> Prop} :
  undecidable (complement p) -> undecidable (complement (complement p)).
Proof.
  intros H Hp. now apply H, dec_compl'.
Qed.

Module undecidabilityNotations.
Import ReductionChainNotations.

Tactic Notation "undec" "from" constr(H) :=
  apply (undecidability_from_reducibility H).

Tactic Notation "undec" "from" constr(U) "using" "chain" constr(C) :=
  undec from U; reduce with chain C.

End undecidabilityNotations.