Require Export Undecidability.Synthetic.Definitions Lia.
Require Import Undecidability.Shared.Dec.
Require Import Setoid Morphisms.

Definition discrete X := decidable ( '(x,y) x = y :> X).


Lemma reflects_not b P :
  reflects b P reflects (negb b) (P).
Proof.
  unfold reflects.
  destruct b; cbn; intuition congruence.
Qed.


Lemma reflects_conj {b1 b2 P1 P2} :
  reflects reflects reflects ( && ) ( ).
Proof.
  unfold reflects.
  destruct , ; cbn; firstorder congruence.
Qed.


Lemma reflects_disj {b1 b2 P1 P2} :
  reflects reflects reflects ( || ) ( ).
Proof.
  unfold reflects.
  destruct , ; cbn; firstorder congruence.
Qed.


Lemma reflects_prv b (P : Prop) : (b = true P) (b = false P) reflects b P.
Proof.
  intros .
  destruct b; cbn; firstorder.
Qed.



Lemma dec_decidable' X p :
  ( x : X, dec (p x)) { f : _ | x, p x f x = true}.
Proof.
  intros d. exists ( x if d x then true else false). intros x. destruct (d x); firstorder congruence.
Qed.


Lemma decidable_iff X p :
  decidable p inhabited ( x : X, dec (p x)).
Proof.
  split.
  - intros [f H]. econstructor. intros x. specialize (H x). destruct (f x); firstorder congruence.
  - intros [d]. eapply dec_decidable' in d as [f]. now exists f.
Qed.



Lemma discrete_iff X :
  discrete X inhabited (eq_dec X).
Proof.
  split.
  - intros [D] % decidable_iff. econstructor. intros x y; destruct (D (x,y)); firstorder.
  - intros [d]. eapply decidable_iff. econstructor. intros (x,y). eapply d.
Qed.


Lemma dec_compl X p :
  decidable p decidable ( x : X p x).
Proof.
  intros [f H]. exists ( x negb (f x)).
  intros x. eapply reflects_not, H.
Qed.


Lemma dec_conj X p q :
  decidable p decidable q decidable ( x : X p x q x).
Proof.
  intros [f] [g]. exists ( x andb (f x) (g x)).
  intros x. eapply reflects_conj; eauto.
Qed.


Lemma dec_disj X p q :
  decidable p decidable q decidable ( x : X p x q x).
Proof.
  intros [f] [g]. exists ( x orb (f x) (g x)).
  intros x. eapply reflects_disj; eauto.
Qed.



Instance Proper_decides {X} :
  Proper (pointwise_relation X (@eq bool) pointwise_relation X iff iff ) (@decider X).
Proof.
  intros f g p q . red in , .
  unfold decider, reflects.
  split; intros H x.
  - now rewrite , H, .
  - now rewrite , H, .
Qed.


Instance Proper_decidable {X} :
  Proper (pointwise_relation X iff iff) (@decidable X).
Proof.
  intros p q .
  split; intros [f H]; exists f.
  - now rewrite .
  - now rewrite .
Qed.



Lemma discrete_bool : discrete bool.
Proof.
  eapply discrete_iff. econstructor. exact _.
Qed.


Lemma discrete_nat : discrete .
Proof.
  eapply discrete_iff. econstructor. exact _.
Qed.


Lemma discrete_nat_nat : discrete ( * ).
Proof.
  eapply discrete_iff. econstructor. exact _.
Qed.


Lemma discrete_prod X Y : discrete X discrete Y discrete (X * Y).
Proof.
  intros [] % discrete_iff [] % discrete_iff.
  eapply discrete_iff. econstructor. exact _.
Qed.


Lemma discrete_sum X Y : discrete X discrete Y discrete (X + Y).
Proof.
  intros [] % discrete_iff [] % discrete_iff.
  eapply discrete_iff. econstructor. exact _.
Qed.


Lemma discrete_option X : discrete X discrete (option X).
Proof.
  intros [] % discrete_iff. eapply discrete_iff.
  econstructor. exact _.
Qed.


Lemma discrete_list X : discrete X discrete (list X).
Proof.
  intros [] % discrete_iff. eapply discrete_iff.
  econstructor. exact _.
Qed.