From Undecidability.Shared.Libs.PSL Require Export BasicDefinitions FinTypesDef.
From Undecidability.Shared.Libs.PSL Require Import Bijection.


Definition elem (F: finType) := @enum (type F) (class F).
#[export] Hint Unfold elem : core.
#[export] Hint Unfold class : core.

Lemma elem_spec (X: finType) (x:X) : x (elem X).
Proof.
  apply countIn. pose proof (enum_ok x) as H. unfold elem. .
Qed.


#[export] Hint Resolve elem_spec : core.
#[export] Hint Resolve enum_ok : core.

Lemma allSub (X: finType) (A:list X) : A elem X.
Proof.
  intros x _. apply elem_spec.
Qed.

#[export] Hint Resolve allSub : core.

Theorem Equivalence_property_all (X: finType) (p: X Prop) :
  ( x, p x) x, x (elem X) p x.
Proof.
  split; auto.
Qed.


Theorem Equivalence_property_exists (X: finType) (p:X Prop):
  ( x, p x) x, x (elem X) p x.
Proof.
  split.
  - intros [x P]. eauto.
  - intros [x [E P]]. eauto.
Qed.


#[global]
Instance finType_forall_dec (X: finType) (p: X Prop): ( x, dec (p x)) dec ( x, p x).
Proof.
  intros D. eapply dec_transfer.
  - symmetry. exact (Equivalence_property_all p).
  - auto.
Qed.


#[global]
Instance finType_exists_dec (X:finType) (p: X Prop) : ( x, dec (p x)) dec ( x, p x).
Proof.
  intros D. eapply dec_transfer.
  - symmetry. exact (Equivalence_property_exists p).
  - auto.
Qed.


Definition finType_cc (X: finType) (p: X Prop) (D: x, dec (p x)) : ( x, p x) {x | p x}.
Proof.
  intro H.
  assert( x, x (elem X) p x) as E by firstorder.
  pose proof (list_cc D E) as [x G].
  now exists x.
Defined.


Definition pickx (X: finType): X + (X False).
Proof.
  destruct X as [X [enum ok]]. induction enum.
  - right. intro x. discriminate (ok x).
  - tauto.
Defined.



Lemma DM_notAll (X: finType) (p: X Prop) (D: x, dec (p x)): ( ( x, p x)) x, (p x).
Proof.
  decide ( x, p x); firstorder.
Qed.


Lemma DM_exists (X: finType) (p: X Prop) (D: x, dec (p x)):
  ( x, p x) ~( x, p x).
Proof.
  split.
  - firstorder.
  - decide ( x, p x); firstorder.
Qed.



Fixpoint getPosition {E: eqType} (A: list E) x := match A with
                                                   | nil 0
                                                   | cons x' A' if Dec (x=x') then 0 else 1 + getPosition A' x end.

Lemma getPosition_correct {E: eqType} (x:E) A: if Dec (x A) then z, (nth (getPosition A x) A z) = x else getPosition A x = |A |.
Proof.
  induction A;cbn.
  -repeat destruct Dec;tauto.
  -repeat destruct Dec;intuition; congruence.
Qed.


Lemma getPosition_nth (X:eqType) k (d :X) xs:
  Dupfree.dupfree xs
  k < length xs
  getPosition xs (nth k xs d) = k.
Proof.
  induction xs in k|-*. now cbn.
  intros . inv .
  cbn. destruct k.
  -decide _. all:easy.
  -decide _.
   +subst a. cbn in . edestruct . eapply nth_In. .
   + cbn in . rewrite IHxs. all:try easy;.
Qed.


Definition pos_def (X : eqType) (x : X) A n := match pos x A with None n | Some n n end.

Definition index {F: finType} (x:F) := getPosition (elem F) x.

Lemma index_nth {F : finType} (x:F) y: nth (index x) (elem F) y = x.
Proof.
  unfold index, elem, enum.
  destruct F as [[X E] [A all_A]];cbn.
  pose proof (getPosition_correct x A) as H.
  destruct Dec. auto. apply notInZero in n. now setoid_rewrite all_A in n.
Qed.


Lemma injective_index (A: finType) (x1 x2 : A) : index = index = .
Proof.
  destruct (elem A) eqn:E.
  - hnf. intros. assert ( elem A) by eauto using elem_spec. rewrite E in . auto.
  - clear E. eapply (left_inv_inj (g := ( y nth y (elem A) e))).
    hnf. intros. now rewrite index_nth.
Qed.


Lemma index_le (A:finType) (x:A): index x < length (elem A).
Proof.
  unfold index.
  assert (H:x elem A) by apply elem_spec.
  revert H.
  generalize (elem A). intros l H.
  induction l;cbn;[|decide _].
  -easy.
  -.
  -destruct H. congruence. apply IHl in H. .
Qed.


Lemma index_leq (A:finType) (x:A): index x length (elem A).
Proof.
  eapply Nat.lt_le_incl,index_le.
Qed.