# Library Decidability

Require Export Encoding.

# Definition of L-decidability

Definition ldec (P : term -> Prop) :=
exists u : term, proc u /\ forall s, (P s /\ u (tenc s) == true) \/ (~ P s /\ u (tenc s) == false).

# Complement, conj and disj of predicates

Definition complement (P : term -> Prop) := fun t => ~ P t.

Definition conj (P : term -> Prop) (Q : term -> Prop) := fun t => P t /\ Q t.

Definition disj (P : term -> Prop) (Q : term -> Prop) := fun t => P t \/ Q t.

Hint Unfold complement conj disj.

# Deciders for complement, conj and disj of ldec predicates

Definition tcompl (u : term) : term := .\"x"; !Not (!u "x").

Definition tconj u v : term := .\"x"; !Andalso (!u "x") (!v "x").

Definition tdisj u v : term := .\"x"; !Orelse (!u "x") (!v "x").

Hint Unfold tcompl tconj tdisj : cbv.

# L-decidable predicates are closed under complement, conj and disj

Lemma ldec_complement P : ldec P -> ldec (complement P).

Proof.

intros [u [[cls_u lam_u] H]].

exists (tcompl u).

split; value.

intros s.
destruct (H s) as [[Ps A] | [nPs A]];
[right | left]; intuition; crush.

Qed.

Lemma ldec_conj P Q : ldec P -> ldec Q -> ldec (conj P Q).

Proof.

intros [u [[cls_u lam_u] decP]] [v [[cls_v lam_v] decQ]].

exists (tconj u v).
split; value.
intros s.

destruct (decP s) as [[Ps Hu ] | [nPs Hu]], (decQ s) as [[Qs Hv] | [nQs Hv]]; [left| right..]; firstorder; crush.

Qed.

Lemma ldec_disj P Q : ldec P -> ldec Q -> ldec (disj P Q).

Proof.

intros [u [[cls_u lam_u] Hu]] [v [[cls_v lam_v] Hv]].

exists (tdisj u v).
split; value.
intros s.
destruct (Hu s) as [[A B] | [A B]], (Hv s) as [[C D] | [C D]]; [left .. | right]; firstorder; crush.
Qed.