From Undecidability.Synthetic Require Import DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts MoreEnumerabilityFacts.
Require Import List.
Import ListNotations.
From Undecidability.Shared Require Import Dec.
Set Implicit Arguments.
Set Default Proof Using "Type".
Section Properties.
Variables (X : Type) (P : X -> Prop)
(Y : Type) (Q : Y -> Prop)
(Z : Type) (R : Z -> Prop).
Fact reduces_reflexive : P ⪯ P.
Proof. exists (fun x => x); red; tauto. Qed.
Fact reduces_transitive : P ⪯ Q -> Q ⪯ R -> P ⪯ R.
Proof.
unfold reduces, reduction.
intros (f & Hf) (g & Hg).
exists (fun x => g (f x)).
intro; rewrite Hf, Hg; tauto.
Qed.
Fact reduces_dependent :
P ⪯ Q <-> inhabited (forall x, { y | P x <-> Q y }).
Proof.
constructor.
- intros [f Hf]. constructor. intros x. now exists (f x).
- intros [f]. exists (fun x => proj1_sig (f x)).
intros x. exact (proj2_sig (f x)).
Qed.
Fact reduces_complement : P ⪯ Q -> complement P ⪯ complement Q.
Proof.
intros [f Hf].
exists f. intros x. specialize (Hf x). split.
all: intros H Hc; apply H, Hf, Hc.
Qed.
End Properties.
Module ReductionChainNotations.
Ltac redchain2Prop_rec xs :=
lazymatch xs with
| pair ?x (pair ?y ?xs) =>
let z := redchain2Prop_rec (pair y xs) in
constr:(x ⪯ y /\ z)
| pair ?x ?y => constr:(x ⪯ y)
end.
Ltac redchain2Prop xs :=
let z := redchain2Prop_rec xs
in exact z.
Declare Scope reduction_chain.
Delimit Scope reduction_chain with redchain_scope.
Notation "x '⪯ₘ' y" := (pair x y) (at level 80, right associativity, only parsing) : reduction_chain.
Notation "'⎩' xs '⎭'" := (ltac:(redchain2Prop (xs % redchain_scope))) (only parsing).
End ReductionChainNotations.
Lemma dec_red X (p : X -> Prop) Y (q : Y -> Prop) :
p ⪯ q -> decidable q -> decidable p.
Proof.
unfold decidable, decider, reduces, reduction, reflects.
intros [f] [d]. exists (fun x => d (f x)). intros x. rewrite H. eapply H0.
Qed.
Lemma red_comp X (p : X -> Prop) Y (q : Y -> Prop) :
p ⪯ q -> (fun x => ~ p x) ⪯ (fun y => ~ q y).
Proof.
intros [f]. exists f. intros x. red in H. now rewrite H.
Qed.
Section enum_red.
Variables (X Y : Type) (p : X -> Prop) (q : Y -> Prop).
Variables (f : X -> Y) (Hf : forall x, p x <-> q (f x)).
Variables (Lq : _) (qe : list_enumerator Lq q).
Variables (x0 : X).
Variables (d : eq_dec Y).
Local Fixpoint L L' n :=
match n with
| 0 => []
| S n => L L' n ++ (filter (fun x => Dec (In (f x) (cumul Lq n))) (cumul L' n))
end.
Local Lemma enum_red L' :
list_enumerator__T L' X ->
list_enumerator (L L') p.
Proof using qe Hf.
intros HL'.
split.
+ intros H.
eapply Hf in H. eapply (cumul_spec qe) in H as [m1]. destruct (cumul_spec__T HL' x) as [m2 ?].
exists (1 + m1 + m2). cbn. apply in_app_iff. right.
apply filter_In. split.
* eapply cum_ge'; eauto; lia.
* eapply Dec_auto. eapply cum_ge'; eauto; lia.
+ intros [m H]. induction m.
* inversion H.
* cbn in H. apply in_app_or in H. destruct H; [now auto|].
apply filter_In in H. destruct H as [_ H].
destruct (Dec _) in H; [|easy].
eapply Hf. eauto.
Qed.
End enum_red.
Lemma enumerable_red X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> discrete Y -> enumerable q -> enumerable p.
Proof.
intros [f] [] % enum_enumT [] % discrete_iff [L] % enumerable_enum.
eapply list_enumerable_enumerable.
eexists. eapply enum_red; eauto.
Qed.
Lemma semi_decidable_red (X Y : Type) (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> semi_decidable q -> semi_decidable p.
Proof.
intros [f Hf] [g Hg]. exists (fun x n => g (f x) n).
firstorder.
Qed.
Theorem not_decidable X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) ->
~ decidable q /\ ~ decidable (complement q).
Proof.
intros. split; intros ?.
- eapply H1. eapply dec_red in H2; eauto.
eapply dec_compl in H2. eapply dec_count_enum; eauto.
- eapply H1. eapply dec_red in H2; eauto.
eapply dec_count_enum; eauto. now eapply red_comp.
Qed.
Theorem not_coenumerable X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) -> discrete Y ->
~ enumerable (complement q).
Proof.
intros. intros ?. eapply H1. eapply enumerable_red in H3; eauto.
now eapply red_comp.
Qed.
Require Import List.
Import ListNotations.
From Undecidability.Shared Require Import Dec.
Set Implicit Arguments.
Set Default Proof Using "Type".
Section Properties.
Variables (X : Type) (P : X -> Prop)
(Y : Type) (Q : Y -> Prop)
(Z : Type) (R : Z -> Prop).
Fact reduces_reflexive : P ⪯ P.
Proof. exists (fun x => x); red; tauto. Qed.
Fact reduces_transitive : P ⪯ Q -> Q ⪯ R -> P ⪯ R.
Proof.
unfold reduces, reduction.
intros (f & Hf) (g & Hg).
exists (fun x => g (f x)).
intro; rewrite Hf, Hg; tauto.
Qed.
Fact reduces_dependent :
P ⪯ Q <-> inhabited (forall x, { y | P x <-> Q y }).
Proof.
constructor.
- intros [f Hf]. constructor. intros x. now exists (f x).
- intros [f]. exists (fun x => proj1_sig (f x)).
intros x. exact (proj2_sig (f x)).
Qed.
Fact reduces_complement : P ⪯ Q -> complement P ⪯ complement Q.
Proof.
intros [f Hf].
exists f. intros x. specialize (Hf x). split.
all: intros H Hc; apply H, Hf, Hc.
Qed.
End Properties.
Module ReductionChainNotations.
Ltac redchain2Prop_rec xs :=
lazymatch xs with
| pair ?x (pair ?y ?xs) =>
let z := redchain2Prop_rec (pair y xs) in
constr:(x ⪯ y /\ z)
| pair ?x ?y => constr:(x ⪯ y)
end.
Ltac redchain2Prop xs :=
let z := redchain2Prop_rec xs
in exact z.
Declare Scope reduction_chain.
Delimit Scope reduction_chain with redchain_scope.
Notation "x '⪯ₘ' y" := (pair x y) (at level 80, right associativity, only parsing) : reduction_chain.
Notation "'⎩' xs '⎭'" := (ltac:(redchain2Prop (xs % redchain_scope))) (only parsing).
End ReductionChainNotations.
Lemma dec_red X (p : X -> Prop) Y (q : Y -> Prop) :
p ⪯ q -> decidable q -> decidable p.
Proof.
unfold decidable, decider, reduces, reduction, reflects.
intros [f] [d]. exists (fun x => d (f x)). intros x. rewrite H. eapply H0.
Qed.
Lemma red_comp X (p : X -> Prop) Y (q : Y -> Prop) :
p ⪯ q -> (fun x => ~ p x) ⪯ (fun y => ~ q y).
Proof.
intros [f]. exists f. intros x. red in H. now rewrite H.
Qed.
Section enum_red.
Variables (X Y : Type) (p : X -> Prop) (q : Y -> Prop).
Variables (f : X -> Y) (Hf : forall x, p x <-> q (f x)).
Variables (Lq : _) (qe : list_enumerator Lq q).
Variables (x0 : X).
Variables (d : eq_dec Y).
Local Fixpoint L L' n :=
match n with
| 0 => []
| S n => L L' n ++ (filter (fun x => Dec (In (f x) (cumul Lq n))) (cumul L' n))
end.
Local Lemma enum_red L' :
list_enumerator__T L' X ->
list_enumerator (L L') p.
Proof using qe Hf.
intros HL'.
split.
+ intros H.
eapply Hf in H. eapply (cumul_spec qe) in H as [m1]. destruct (cumul_spec__T HL' x) as [m2 ?].
exists (1 + m1 + m2). cbn. apply in_app_iff. right.
apply filter_In. split.
* eapply cum_ge'; eauto; lia.
* eapply Dec_auto. eapply cum_ge'; eauto; lia.
+ intros [m H]. induction m.
* inversion H.
* cbn in H. apply in_app_or in H. destruct H; [now auto|].
apply filter_In in H. destruct H as [_ H].
destruct (Dec _) in H; [|easy].
eapply Hf. eauto.
Qed.
End enum_red.
Lemma enumerable_red X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> discrete Y -> enumerable q -> enumerable p.
Proof.
intros [f] [] % enum_enumT [] % discrete_iff [L] % enumerable_enum.
eapply list_enumerable_enumerable.
eexists. eapply enum_red; eauto.
Qed.
Lemma semi_decidable_red (X Y : Type) (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> semi_decidable q -> semi_decidable p.
Proof.
intros [f Hf] [g Hg]. exists (fun x n => g (f x) n).
firstorder.
Qed.
Theorem not_decidable X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) ->
~ decidable q /\ ~ decidable (complement q).
Proof.
intros. split; intros ?.
- eapply H1. eapply dec_red in H2; eauto.
eapply dec_compl in H2. eapply dec_count_enum; eauto.
- eapply H1. eapply dec_red in H2; eauto.
eapply dec_count_enum; eauto. now eapply red_comp.
Qed.
Theorem not_coenumerable X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) -> discrete Y ->
~ enumerable (complement q).
Proof.
intros. intros ?. eapply H1. eapply enumerable_red in H3; eauto.
now eapply red_comp.
Qed.