(* Set Implicit Arguments. *)
Require Import BA.External.
Require Import Seqs.
Require Import BasicDefs.
Require Import BA.FinTypes.

Section FirstKFinType.

  Definition le_k k := fun n => n <= k.
  Instance dec_le_k k n : dec ( le_k k n). Proof. auto. Defined.

  Definition Le_K k := {n | (pure (le_k k)) n}.

  Fixpoint all_le_k k : list nat := match k with
    | 0 => [0]
    | S k => (S k) :: (all_le_k k) end.

  Instance dec_pure_le_k k n : dec (pure (le_k k) n).
  Proof.
   decide (le_k k n) as[D|D].
   - left. now apply pure_equiv.
   - right. intros L. apply D. now apply pure_equiv in L.
  Defined.

  Hint Resolve dec_pure_le_k.

  Lemma pure_le_k_if k n : n <= k -> pure (le_k k) n.
  Proof.
    intros L.
    now rewrite <-pure_equiv.
  Qed.

  Definition all_Le_K k n := (fix f (L: list nat) := match L with
      | [] => []
      | n::L => match (decision (pure (le_k k) n)) with
                 | left D => (exist (pure (le_k k)) n D) :: f L
                 | right D => f L
                   end end) (all_le_k n).

  Lemma in_all_le_k_iff k n: n<= k <-> n el all_le_k k.
  Proof.
   induction k.
   - split.
     + intros L. simpl. left. omega.
     + intros [E|E]. omega. contradiction E.
   - split.
     + intros L. decide (n = S k).
       * rewrite e. simpl. now left.
       * simpl. right. apply IHk. omega.
     + intros E. decide (n = S k).
       * omega.
       * enough (n <= k). omega.
         apply IHk. destruct E as [E|E].
         -- apply IHk. omega.
         -- assumption.
  Qed.

  Lemma dup_free_all_le_k k: dupfree (all_le_k k).
  Proof.
    induction k.
    - simpl. constructor.
      + auto.
      + constructor.
    - simpl. constructor.
      + intros E. apply in_all_le_k_iff in E. omega.
      + assumption.
  Qed.

  Lemma in_all_Le_K_if k (x : Le_K k): x el all_Le_K k k.
  Proof.
    unfold all_Le_K.
    destruct x as [n L].
    pose (L' := L).
    rewrite <-pure_equiv in L'.
    pose (Q:= in_all_le_k_iff k n).
    destruct Q. specialize (H L').
    induction (all_le_k k).
    - contradiction H.
    - destruct H.
      + rewrite H.
        decide (pure (le_k k) n).
        * simpl. left.
           f_equal. apply pure_eq.
        * exfalso. apply n0. now apply pure_le_k_if.
      + decide (pure (le_k k) a).
        * simpl. right. apply IHl; auto.
        * apply IHl; auto.
  Qed.

  Lemma in_all_Le_K_if2 k x : x el all_Le_K k k -> match x with exist _ x L => x <= k end.
  Proof.
    destruct x. intros _. change ((le_k k) x). rewrite pure_equiv. apply p.
  Qed.

  Lemma in_all_Le_K_ifLess k k' x :k <= k'-> x el all_Le_K k' k -> match x with exist _ x _ => x <= k end.
  Proof.
    unfold all_Le_K.
    intros L.
    induction k.
    - simpl. destruct (pure_equiv 0). destruct x. intros [E|E].
      + enough (x = 0). omega.
        congruence.
      + contradiction E.
    - simpl. decide (pure (le_k k') (S k)) as [D|D].
      + simpl. intros [E|E].
        * destruct x. enough (x = S k). omega. congruence.
        * destruct x. enough (x <= k). omega.
          apply IHk; auto. omega.
      + exfalso. apply D. apply pure_le_k_if. omega.
  Qed.

  Lemma dup_free_all_Le_K k n : n <= k -> dupfree (all_Le_K k n).
  Proof.
    unfold all_Le_K. revert k.
    induction n; intros k L.
    - simpl. constructor.
      + auto.
      + constructor.
    - simpl. decide (pure (le_k k) (S n)).
      + constructor.
        * intros E. apply in_all_Le_K_ifLess in E. omega. omega.
        * apply IHn. omega.
      + apply IHn. omega.
  Qed.

  Section DeclareFinType.
    Variable (k:nat).

    Instance LE_K_eq_dec : eq_dec (Le_K k).
    Proof.
      intros [n1 p1] [n2 p2].
      decide (n1 = n2).
      - left. destruct e. f_equal. now apply pure_eq.
      - right. intros L. apply n.
        congruence.
    Defined.
    Canonical Structure EqLe_K := EqType (Le_K k).

    Lemma Le_K_enum_ok (x : EqLe_K ) : count (X:= EqLe_K ) (all_Le_K k k) x =1.
    Proof.
      apply dupfreeCount.
      - apply dup_free_all_Le_K. omega.
      - apply in_all_Le_K_if.
    Qed.

    Instance finTypeC_Le_K : finTypeC EqLe_K.
    Proof.
      econstructor. apply Le_K_enum_ok.
    Defined.
    Canonical Structure finType_Le_K : finType := FinType EqLe_K.
  End DeclareFinType.

  Lemma create_Le_K n k (L: n <= k) : Le_K k.
  Proof.
   exists n.
   apply pure_equiv. unfold le_k. exact L.
  Defined.

  Lemma all_Le_K_length_all_le_k n k : n<= k -> length (all_Le_K k n) = S n.
  Proof.
    unfold all_Le_K. revert k.
    induction n; intros k L.
    - simpl. reflexivity.
    - simpl. destruct decision as [D|D].
      + simpl. f_equal. apply IHn. omega.
      + exfalso. apply D. now rewrite <-pure_equiv.
  Qed.

  Lemma card_finTypeC_Le_K k : length(enum (finTypeC := finTypeC_Le_K k )) = S k.
  Proof.
    unfold finType_Le_K. simpl.
    now apply all_Le_K_length_all_le_k.
  Qed.

  Lemma card_finType_Le_K k : Cardinality( finType_Le_K k ) = S k.
  Proof.
    unfold Cardinality. apply card_finTypeC_Le_K.
  Qed.

  Lemma bounded_type_exist k (P: (Le_K k) -> Prop) (decP: forall L, dec (P L)): dec( exists L, P L).
  Proof.
   - auto using finType_exists_dec.
  Qed.

  Lemma bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n <= k /\ P (n)).
  Proof.
    pose (P' := fun (n:Le_K k) => match n with exist _ n _ => P n end).
    enough (dec (exists (n:Le_K k), P' n)) as H.
    - destruct H as [H|H].
      + left. destruct H as [[n p] Pn].
        exists n. split.
        * change (le_k k n). rewrite pure_equiv. exact p.
        * now simpl in Pn.
      + right. intros [n [L Pn]].
        apply H. change (le_k k n) in L. rewrite pure_equiv in L.
        exists (exist (pure (le_k k)) n L).
        now simpl.
    - apply bounded_type_exist. intros L. unfold P'. now destruct L.
  Qed.

  Lemma strict_bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n < k /\ P (n)).
  Proof.
    destruct k.
    - right. intros [n [L _]]. omega.
    - destruct (bounded_exist k decP) as [D|D].
      + left. destruct D as [ n [ L Q]]. exists n. split; oauto.
      + right. intros [n [L Q]]. apply D. exists n. split; oauto.
  Qed.

End FirstKFinType.

Hint Resolve bounded_exist.
Hint Resolve strict_bounded_exist.

Instance dec_pure_le_k_public x y : dec (pure (le_k x) y).
Proof. apply dec_pure_le_k. Defined.
Hint Resolve dec_pure_le_k_public. (* The other does not work for some reasons even it is registered*)

Section ConvertFinTypeToSeq.

  Context {m : nat}.
  Context {X : finType}.

  Lemma dummy : (finType_Le_K m).
  Proof.
    exists 0. apply pure_equiv. unfold le_k. omega.
  Qed.

  Definition to_seq (b:X^(finType_Le_K m)) := fun (n:nat) => match (decision (pure (le_k m) n) ) with
                                   | left D => applyVect b (exist (pure (le_k m )) n D)
                                   | right D => applyVect b dummy
                                       end.
  Definition to_bounded(r:Seq X): X^(finType_Le_K m) := vectorise (fun (n:(finType_Le_K m)) => match n with exist _ n _ => r n end).

  Lemma to_bounded_unchanged (r:Seq X) n (L: n <= m ): applyVect (to_bounded r) (create_Le_K L) = r n.
  Proof.
    unfold to_bounded.
    rewrite apply_vectorise_inverse.
    now simpl.
  Qed.

  Lemma to_seq_unchanged (r:X^(finType_Le_K m)) n (L: n <= m ): to_seq r n = applyVect r (create_Le_K L).
  Proof.
    unfold to_seq.
    destruct (decision (pure (le_k m) n)) as [D|D].
    - f_equal. unfold create_Le_K.
      f_equal. apply pure_eq.
    - exfalso. apply D. now apply pure_equiv.
  Qed.

   Lemma bounded_unchanged (r:Seq X) n : n <=m-> to_seq (to_bounded r) n = r n.
  Proof.
   intros L.
   rewrite (to_seq_unchanged (to_bounded r) L).
   apply to_bounded_unchanged.
  Qed.

End ConvertFinTypeToSeq.

Lemma can_find_duplicate (X: finType) k (r: Seq X) : (Sigma n1 n2, n1 < n2 <= k /\ r n1 = r n2) + {k <= Cardinality X }.
Proof.
  decide (k <= Cardinality X).
  - now right.
  - left.
    assert (k > Cardinality X) as H by omega.
    pose (f := fun (k : finType_Le_K k) => match k with exist _ k _ => r k end ).
    pose (P := fun (n1 n2 : finType_Le_K k) => match n1, n2 with
             (exist _ n1 _), (exist _ n2 _) => n1 < n2 <= k /\ r n1 = r n2 end).
    assert (forall n1 n2, dec(P n1 n2)) as decP. { intros [n1 ?] [n2 ?]. simpl. auto. }
    assert (forall n1, dec (exists (n2 : finType_Le_K k), P n1 n2)) as decP'. { auto using finType_exists_dec. }
    assert (dec (exists (n1 n2 : finType_Le_K k), P n1 n2)) as D. { auto using finType_exists_dec. }
    destruct D as[ D|D].
    + destruct (finType_cc decP') as [n1 p1]. { destruct D as [n1 p]. now exists n1. }
       destruct (finType_cc (decP n1)) as [n2 p2]. { destruct p1 as [n2 p]. now exists n2. }
       destruct n1 as [n1 ?]; destruct n2 as [n2 ?].
       exists n1; exists n2.
       now simpl in p2.
    + exfalso.
       assert (injective f) as I. {
         intros x y E.
         decide (x = y).
         - assumption.
         - exfalso. apply D.
           destruct x as [x' px] eqn:EX; destruct y as [y' py] eqn:EY.
           decide (x' < y').
           + exists x; exists y. unfold P.
             rewrite EX,EY. repeat split.
             * assumption.
             * change ((le_k k) y'). rewrite pure_equiv. apply py.
             * now unfold f in E.
           + assert (y' <> x'). { intros Eq. apply n0. destruct Eq. f_equal. apply pure_eq. }
             assert (y' < x') by omega.
             exists y; exists x. unfold P.
             rewrite EX,EY. repeat split.
             * assumption.
             * change ((le_k k) x'). rewrite pure_equiv. apply px.
             * now unfold f in E.
       }
       pose (J := pidgeonHole_inj I).
       rewrite card_finType_Le_K in J.
       omega.
Qed.

Fixpoint max_of_nat_string w l:= match l with
  | 0 => w 0
  | S l => max (w (S l)) (max_of_nat_string w l) end.

Lemma max_of_nat_string_correct v l: forall n , n<=l -> (v n) <= max_of_nat_string v l.
Proof.
  induction l; intros n L.
  - now rewrite_eq (n = 0).
  - simpl. decide (n = S l) as[D|D].
    + apply max_le_left. rewrite D. omega.
    + apply max_le_right. apply IHl. omega.
Qed.

Lemma list_eq (X: Type) (l1 l2: list X) : (forall n, nth_error l1 n= nth_error l2 n) -> l1 = l2.
Proof.
  revert l2.
  induction l1; intros l2 EE.
  - specialize (EE 0). simpl in EE. now destruct l2.
  - destruct l2.
    + now specialize (EE 0).
    + f_equal.
      * specialize (EE 0). simpl in EE. congruence.
      * apply IHl1.
        intros n. specialize (EE (S n)). now simpl in EE.
Qed.

Inductive safe (p : nat -> Prop) (n : nat) : Prop :=
| safeB : p n -> safe p n
| safeS : safe p (S n) -> safe p n.

Lemma safe_dclosed k n p : k <= n -> safe p n -> safe p k.
Proof.
  intros A B. induction A as [|n A].
  - exact B.
  - apply IHA. right. exact B.
Qed.

Section First.
  Variable p : nat -> Prop.
  Variable p_dec : forall n, dec (p n).

  Fixpoint first (n : nat) (A : safe p n) : {k | p k} :=
    match p_dec n with
    | left B => exist p n B
    | right B => first match A with
    | safeB C => match B C with end
    | safeS A' => A'
    end
  end.

  Lemma cc_nat : (exists x, p x) -> {x | p x}.
  Proof.
    intros A. apply first with (n:=0).
    destruct A as [n A].
    apply safe_dclosed with (n:=n). omega. left. exact A.
  Qed.

End First.