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.