From Undecidability.Synthetic Require Import InformativeDefinitions DecidabilityFacts.
Set Implicit Arguments.
(* ** Pre-order properties *)
Section Properties.
Variables (X : Type) (P : X -> Prop)
(Y : Type) (Q : Y -> Prop)
(Z : Type) (R : Z -> Prop).
Fact ireduces_reflexive : P ⪯ᵢ P.
Proof. exists (fun x => x); red; tauto. Qed.
Fact ireduces_transitive : P ⪯ᵢ Q -> Q ⪯ᵢ R -> P ⪯ᵢ R.
Proof.
unfold inf_reduces, reduction.
intros (f & Hf) (g & Hg).
exists (fun x => g (f x)).
intro; rewrite Hf, Hg; tauto.
Qed.
Fact ireduces_reduces : P ⪯ᵢ Q -> P ⪯ Q.
Proof. intros (f & ?); exists f; auto. Qed.
Fact reduces_ireduces : P ⪯ Q -> inhabited (P ⪯ᵢ Q).
Proof. intros (f & ?); exists; exists f; auto. Qed.
Fact reduces_ireduces_iff : P ⪯ Q <-> inhabited (P ⪯ᵢ Q).
Proof.
split.
+ apply reduces_ireduces.
+ intros []; apply ireduces_reduces; auto.
Qed.
(* ** An equivalent dependent definition *)
Fact ireduces_dependent :
(P ⪯ᵢ Q -> forall x, { y | P x <-> Q y })
* ((forall x, { y | P x <-> Q y }) -> P ⪯ᵢ Q).
Proof.
unfold inf_reduces, reduction.
split.
+ intros (f & Hf).
intros x; exists (f x); auto.
+ intros f.
exists (fun x => proj1_sig (f x)).
intros; apply (proj2_sig (f x)).
Qed.
End Properties.
Set Implicit Arguments.
(* ** Pre-order properties *)
Section Properties.
Variables (X : Type) (P : X -> Prop)
(Y : Type) (Q : Y -> Prop)
(Z : Type) (R : Z -> Prop).
Fact ireduces_reflexive : P ⪯ᵢ P.
Proof. exists (fun x => x); red; tauto. Qed.
Fact ireduces_transitive : P ⪯ᵢ Q -> Q ⪯ᵢ R -> P ⪯ᵢ R.
Proof.
unfold inf_reduces, reduction.
intros (f & Hf) (g & Hg).
exists (fun x => g (f x)).
intro; rewrite Hf, Hg; tauto.
Qed.
Fact ireduces_reduces : P ⪯ᵢ Q -> P ⪯ Q.
Proof. intros (f & ?); exists f; auto. Qed.
Fact reduces_ireduces : P ⪯ Q -> inhabited (P ⪯ᵢ Q).
Proof. intros (f & ?); exists; exists f; auto. Qed.
Fact reduces_ireduces_iff : P ⪯ Q <-> inhabited (P ⪯ᵢ Q).
Proof.
split.
+ apply reduces_ireduces.
+ intros []; apply ireduces_reduces; auto.
Qed.
(* ** An equivalent dependent definition *)
Fact ireduces_dependent :
(P ⪯ᵢ Q -> forall x, { y | P x <-> Q y })
* ((forall x, { y | P x <-> Q y }) -> P ⪯ᵢ Q).
Proof.
unfold inf_reduces, reduction.
split.
+ intros (f & Hf).
intros x; exists (f x); auto.
+ intros f.
exists (fun x => proj1_sig (f x)).
intros; apply (proj2_sig (f x)).
Qed.
End Properties.