Computable sets

computable.v

Require Import Coq.Unicode.Utf8.
Require Coq.Program.Basics.

Import IfNotations.

Inductive SET := image (A: Set) (π: A → SET).

Definition index (X: SET) :=
  let '(image A _) := X in A.
Definition π (X: SET): index X → SET  :=
  let '(image _ p) := X in p.

Inductive mem (X: SET): SET → Prop :=
| witness x: mem X (π X x).
Infix "∈" := (Basics.flip mem) (at level 30).

Definition CLASS := SET → Prop.

Definition Decidable (X: SET) := ∀ (x: SET), {x ∈ X} + {¬ (x ∈ X)}.
Existing Class Decidable.

(* Typically computable sets are sets of natural numbers? *)
Inductive Computable {X: SET} :=
| Computable_intro (p: Decidable X) (q: ∀ x, @Computable (π X x)).
Arguments Computable: clear implicits.
Existing Class Computable.

Instance Computable_Complement (X: SET) `{H:Computable X}: Decidable X :=
  let '(Computable_intro P _) := H in P.

Definition Computable_π (X: SET) `{H:Computable X}: ∀ x:index X, Computable (π X x) :=
  let '(Computable_intro _ p) := H in p.
Existing Instance Computable_π.

Definition empty: SET := image Empty_set (λ x, match x with end).
Notation "∅" := empty.

Instance empty_Decidable: Decidable ∅.
Proof.
  right.
  intros [[]].
Defined.

Instance empty_Computable: Computable ∅ :=
  Computable_intro empty_Decidable (λ x, match x with end).

Definition pair (X Y: SET): SET := image bool (λ x, if x then X else Y).

Instance pair_Decidable A B `{Computable A} `{Computable B}: Decidable (pair A B).
Proof.
  intro x.
  admit.
Admitted.