(* Set Implicit Arguments. *)
Require Import BasicDefs.
Require Export FinTypes.FinTypes.

Lemma dupfree_injective_map (X Y:Type) (f: X -> Y) (L : list X) : dupfree L -> injective f -> dupfree (map f L).
Proof.
  intros D Inj. induction D as [| x A]; simpl; constructor.
  - intros [y [E1 E2]] % in_map_iff. apply Inj in E1. now subst y.
  - apply IHD.
Qed.

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}.

  Instance dec_pure_le_k k n : dec (pure (le_k k) n).
  Proof.
    apply dec_trans with (P:= le_k k n); auto using pure_equiv.
  Qed.

  Hint Resolve dec_pure_le_k.

  Lemma pure_le_k_iff k n : n <= k <-> pure (le_k k) n.
  Proof.
    rewrite <-pure_equiv. unfold le_k. tauto.
  Qed.

  Definition upgrade_bound k (x: Le_K k): Le_K (S k).
  Proof.
    destruct x as [n L]. exists n. apply pure_le_k_iff. constructor. now apply pure_le_k_iff.
  Defined.

  Definition id_Le_K k : Le_K k.
  Proof.
    exists k. apply pure_le_k_iff. constructor.
  Defined.

  Definition create_Le_K k n: n <= k -> Le_K k.
  Proof.
    intros L. exists n. now apply pure_le_k_iff.
  Defined.

  Fixpoint nums_leq_K (k : nat) : list (Le_K k) :=
     match k with
     | 0 => [id_Le_K 0]
     | S k => id_Le_K (S k) :: map (upgrade_bound (k:=k)) (nums_leq_K k)
  end.

  Lemma nums_leq_K_complete k (x:Le_K k ) : x el (nums_leq_K k).
  Proof.
    induction k; destruct x as [n L].
    - cbn. left. unfold id_Le_K.
      assert(n = 0). { apply pure_le_k_iff in L. omega. } subst n.
      f_equal. apply pure_eq.
    - decide (n = S k) as [-> |D]; cbn.
      + left. unfold id_Le_K. f_equal. apply pure_eq.
      + right. apply in_map_iff.
        assert (n <= k) as H. { apply pure_le_k_iff in L. omega. }
        exists (create_Le_K H). split.
        * unfold upgrade_bound. cbn. f_equal. apply pure_eq.
        * apply IHk.
  Qed.

  Lemma nums_leq_K_dupfree k: dupfree (nums_leq_K k).
  Proof.
    induction k; cbn; constructor; auto.
    - constructor.
    - intros [[n L] [E1 E2]] % in_map_iff. enough (n = S k).
      + clear E1 E2. apply pure_le_k_iff in L. omega.
      + unfold upgrade_bound, id_Le_K in E1. congruence.
    - apply dupfree_injective_map.
      + apply IHk.
      + intros [n1 L1] [n2 L2]. unfold upgrade_bound. intros L.
        assert (n1 = n2) by congruence. subst n2. f_equal. apply pure_eq.
  Qed.

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

  Lemma Le_K_enum_ok k (x : EqLe_K k) : count (X:= EqLe_K k) (nums_leq_K k) x =1.
  Proof.
    apply dupfreeCount.
    - apply nums_leq_K_dupfree.
    - apply nums_leq_K_complete.
  Qed.

  Instance finTypeC_Le_K k: finTypeC (EqLe_K k).
  Proof.
    econstructor. apply Le_K_enum_ok.
  Defined.

  Canonical Structure finType_Le_K k: finType := FinType (EqLe_K k).

  Lemma nums_leq_K_length k : length (nums_leq_K k) = S k.
  Proof.
    induction k.
    - now cbn.
    - cbn. now rewrite map_length, IHk.
  Qed.

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

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

  Lemma le_L_is_le k (N : finType_Le_K k): proj1_sig N <= k.
  Proof.
    destruct N. cbn. now apply pure_le_k_iff.
  Qed.

End FirstKFinType.

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

Instance bounded_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n <= k -> P (n)).
Proof.
  pose (P' := fun (n:Le_K k) => P (proj1_sig n)).
  enough (dec (forall (n:Le_K k), P' n)) as [H|H].
  - left. intros n L. apply (H (create_Le_K L)).
  - right. intros N. apply H. intros [n L]. apply N. cbn. now apply pure_le_k_iff.
  - auto.
Qed.

Instance 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) => P (proj1_sig n)).
  enough (dec (exists (n:Le_K k), P' n)) as [H|H].
  - left. destruct H as [[n p] Pn]. exists n. split; auto.
    now apply pure_le_k_iff.
  - right. intros [n [L Pn]].
    apply H. now exists (create_Le_K L).
  - auto.
Qed.

Instance bounded_strict_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n < k -> P (n)).
Proof.
  destruct k.
  - left. intros n L. exfalso. omega.
  - apply dec_trans with (P:= forall n, n <= k -> P n); auto.
    split; intros Q n L; apply Q; omega.
Qed.

Instance 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.
  - apply dec_trans with (P:= exists n, n <= k /\ P n); auto.
    split; intros [n [L Q]]; exists n; split; oauto.
Qed.

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*)

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). cbn in EE. now destruct l2.
  - destruct l2.
    + now specialize (EE 0).
    + f_equal.
      * specialize (EE 0). cbn in EE. congruence.
      * apply IHl1.
        intros n. specialize (EE (S n)). now cbn in EE.
Qed.

Notation "A ^^ l" := (A^(finType_fromList l)) (at level 30).
Section Vectors.

  Lemma vector_eq (X Y: finType) (a b : X^Y) : (forall y, applyVect a y = applyVect b y) -> a = b.
  Proof.
    intros E.
    apply vector_extensionality.
    rewrite <-(vectorise_apply_inverse a).
    rewrite <-(vectorise_apply_inverse b). cbn.
    unfold getImage. apply list_eq.
    induction (elem Y); intros n; cbn; auto.
    destruct n; cbn; auto using IHl. now f_equal.
  Qed.

  Context {B:finType}.
  Context {C:eqType}.


  Definition toFinTypeFromList (L:list C)(x:C) (E: x el L) : (finType_fromList L) :=
         exist (pure (fun x => x el L)) x (match (pure_equiv (p:= fun x => x el L) x) with conj P _ => P E end).
  Definition fromFinTypeFromList (L:list C) (l:finType_fromList L) : C := match l with
         | exist _ x P => x end.

  Lemma toFinTypeFromListEq (L : list C) (x:C) (E1: x el L) (E2: x el L) : toFinTypeFromList E1 = toFinTypeFromList E2.
  Proof.
    unfold toFinTypeFromList. f_equal. destruct pure_equiv. apply pure_eq.
  Qed.

  Lemma from_to_fin_type_from_list (L : list C) (x:C) (E: x el L): x = (fromFinTypeFromList (toFinTypeFromList E)).
  Proof.
    reflexivity.
  Qed.

  Section Narrowing.
    Context {l_1 l_2 : list C}.
    Variable (P: l_1 <<= l_2).

    Definition narrowVector: B^^l_2 -> B^^l_1.
    Proof.
      intros v. apply vectorise. intros [a Q]. apply (applyVect v).
      exists a. apply pure_equiv in Q. now apply pure_equiv, P.
    Defined.

    Lemma narrowVectorCorrect c (M_1:c el l_1) (M_2:c el l_2) v: applyVect v (toFinTypeFromList M_2) = applyVect (narrowVector v) (toFinTypeFromList M_1).
    Proof.
      unfold narrowVector, toFinTypeFromList.
      rewrite apply_vectorise_inverse. f_equal. f_equal. apply pure_eq.
    Qed.

  End Narrowing.

  Context{l:list C} (c:C).
  Implicit Types (b:B)(c:C).

  Lemma rem_sub : rem l c <<= l. Proof. auto. Qed.

  Definition separate : B ^^l -> B ^^(rem l c) := narrowVector rem_sub.

  Definition rest (M: c el l) : B ^^l -> B.
  Proof.
    intros Z. apply (applyVect Z). exists c. now apply pure_equiv.
  Defined.

  Definition join : (B ^^ (rem l c))*B -> B ^^l.
  Proof.
    intros [Z x]. apply vectorise. intros [y P]. decide (y = c).
    - exact x.
    - apply (applyVect Z). exists y. apply pure_equiv in P. now apply pure_equiv, in_rem_iff.
  Defined.

  Lemma join_fst (M: c el l)(v: B ^^ (rem l c)) b : applyVect (join (v, b)) (toFinTypeFromList M) = b.
  Proof.
    unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. now destruct decision; (try (now exfalso; auto)).
  Qed.

  Lemma join_snd (v: B ^^ (rem l c)) b c' (Q: c' el l) (Q': c' el (rem l c)): applyVect (join (v, b)) (toFinTypeFromList Q) = applyVect v (toFinTypeFromList Q').
  Proof.
    unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. destruct decision.
    - exfalso. subst c'. apply in_rem_iff in Q'. tauto.
    - f_equal. f_equal. apply pure_eq.
  Qed.

  Lemma inv_separate_join Z b: separate(join (Z, b)) = Z.
  Proof.
    unfold separate,join, narrowVector. destruct Z as [x Z]. apply vector_eq. intros [y P].
    rewrite !apply_vectorise_inverse. destruct decision.
    - exfalso. apply pure_equiv in P. now apply in_rem_iff in P.
    - f_equal. f_equal. apply pure_eq.
  Qed.

  Lemma inv_join_separate (M: c el l) Z : join ( (separate Z ), (rest M Z)) = Z.
  Proof.
    unfold separate,join, rest, narrowVector. apply vector_eq. intros [x P].
    rewrite apply_vectorise_inverse. destruct decision as [<- |D].
    - repeat f_equal. apply pure_eq.
    - rewrite apply_vectorise_inverse. repeat f_equal. apply pure_eq.
  Qed.

  Section ConvertRemNotIn.
    Variable (M: ~ c el l).

    Lemma rem_not_in_eq: l <<= rem l c.
    Proof. auto. Qed.

    Definition convRemInv : B ^^ (rem l c) -> B^^l := narrowVector (rem_not_in_eq).

    Lemma convRemInv_correct Z c' (Y: c' el l) (Y': c' el (rem l c)) : applyVect Z (toFinTypeFromList Y') = applyVect (convRemInv Z) (toFinTypeFromList Y).
    Proof.
      unfold convRemInv. now rewrite <-narrowVectorCorrect with (M_2 := Y').
    Qed.

    Lemma convRemInv_correct' Z: convRemInv (separate Z) = Z.
    Proof.
      unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
      rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
    Qed.

    Lemma separate_unchanged Z: separate (convRemInv Z) = Z.
    Proof.
      unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
      rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
    Qed.

  End ConvertRemNotIn.

End Vectors.

Section Quotients.

  Context (X:finType).
  Variable (E: X -> X -> Prop).
  Variable (EisEquiv: Equivalence E).
  Context {decP : forall x y, dec (E x y)}.

  Instance EisEquivProper: Equivalence E. Proof. apply EisEquiv. Qed.

  Fixpoint get_equiv_class_rep x (L: list X) := match L with
    | [] => x
    | y::L => if (decision (E y x)) then y else (get_equiv_class_rep x L) end.

  Lemma get_equiv_class_rep_equiv x L : E (get_equiv_class_rep x L) x.
  Proof.
    induction L; cbn.
    - reflexivity.
    - destruct decision as [D|D]; auto.
  Qed.

  Lemma get_equiv_class_rep_less x y L : y el L -> getPosition L y < getPosition L (get_equiv_class_rep x L) -> ~ E (get_equiv_class_rep x L) y.
  Proof.
    intros In Leq Equiv. induction L.
    - now exfalso.
    - cbn in *. decide (y = a).
      + subst a. cbn in *. trivial_decision. destruct decision as [D'|D'] in Equiv.
        * rewrite decision_true in Leq. omega.
          now rewrite decision_true.
        * apply D'. rewrite get_equiv_class_rep_equiv in Equiv. now symmetry.
      + apply IHL.
        * destruct In as [Eq |In]. exfalso. auto. assumption.
        * decide (E a x).
          -- trivial_decision. exfalso. omega.
          -- destruct decision in Leq.
             ++ exfalso. omega.
             ++ omega.
        * decide (E a x).
          -- trivial_decision. exfalso. omega.
          -- assumption.
  Qed.

  Lemma get_equiv_class_rep_unique x y L : x el L -> y el L -> E x y -> (get_equiv_class_rep x L) = (get_equiv_class_rep y L).
  Proof.
    intros InX InY Equiv. induction L.
    - now exfalso.
    - cbn. decide (E a x) as [D|D].
      + rewrite decision_true. reflexivity. now rewrite D.
      + rewrite decision_false. apply IHL.
        * destruct InX; auto.
          exfalso. subst x. apply D. reflexivity.
        * destruct InY; auto.
          exfalso. subst a. apply D. now symmetry.
        * intros Equiv'. apply D. now rewrite Equiv.
  Qed.

  Instance dec_smallest x : dec (forall y, #y < #x -> ~E x y).
  Proof. auto. Qed.

  Definition equiv_class : finType := finType_sub (fun x => forall y, #y < #x -> ~E x y) dec_smallest.
  Definition in_equiv_class (C: equiv_class) y := match C with exist _ x _ => E x y end.

  Definition get_equiv_class (x:X) : equiv_class.
  Proof.
    exists (get_equiv_class_rep x (elem X)).
    apply pure_equiv. intros y L.
    apply get_equiv_class_rep_less; auto.
  Defined.

  Lemma get_equiv_class_correct x : in_equiv_class (get_equiv_class x) x.
  Proof.
    unfold get_equiv_class, in_equiv_class. apply get_equiv_class_rep_equiv.
  Qed.
End Quotients.