Require Import ssreflect ssrfun ssrnat seq ssrbool eqtype fintype choice finset.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Lemma all1s {T : eqType} {a : T} {s} {P : T -> Prop} :
  (forall b, b \in a :: s -> P b) -> P a /\ (forall b, b \in s -> P b).
Proof. move => X; split => [|b Hb]; apply: X; by rewrite ?mem_head // in_cons Hb orbT. Qed.

Lemma leq_eq n m: n <= m -> m <= n -> n = m.
Proof. move => H1 H2. apply/eqP; by rewrite eqn_leq H1 H2. Qed.

Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|.
Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed.

Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
Proof. move/(inj_card_bij val_inj) => [g g1 g2 x]. rewrite -(g2 x). exact: valP. Qed.

Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
Proof.
  case => g /can_inj Hf /can_inj Hg. apply/eqP.
  by rewrite eqn_leq (card_leq_inj Hf) (card_leq_inj Hg).
Qed.

Lemma set1mem (T : finType) (A : {set T}) x : x \in A -> A = x |: A.
Proof.
  move => inA. apply/setP => y. rewrite !inE.
  case e: (y == x) => //=. by rewrite (eqP e).
Qed.

Lemma set_pick_size {F : finType} (X : {set F}) z : [pick z in X] = Some z -> #|X :\ z| < #|X|.
Proof.
  case: (pickP _) => // x [] H [] <-.
  by rewrite (cardsD1 x X) H addnC addn1.
Qed.

Definition surjective {X : eqType} {Y} (f : Y -> X) := forall x, exists w, f w == x.

Lemma surjectiveE (rT aT : finType) (f : aT -> rT) : surjective f -> #|codom f| = #|rT|.
Proof.
  move => H. apply: eq_card => x. rewrite inE. apply/codomP.
  move: (H x) => [y /eqP]. eauto.
Qed.

Lemma surj_card_bij (T T' : finType) (f : T -> T') :
  surjective f -> #|T| = #|T'| -> bijective f.
Proof.
  move => S E. apply: inj_card_bij (E). apply/injectiveP. change (uniq (codom f)).
  apply/card_uniqP. rewrite size_map -cardT E. exact: surjectiveE.
Qed.

Lemma size_induction {X : Type} (f : X -> nat) (p : X ->Prop) :
  ( forall x, ( forall y, f y < f x -> p y) -> p x) -> forall x, p x.
Proof.
  move => A x. apply: (A). elim: (f x) => // n IHn y Hy.
  apply: A => z Hz. apply: IHn. exact: leq_trans Hz Hy.
Qed.

Lemma ptrans {T} (p1 p2 p3 : pred T) : p1 =i p2 -> p2 =i p3 -> p1 =i p3.
Proof. move => H1 H2 w. by rewrite H1. Qed.

Lemma psym {T} (p1 p2 : pred T) : p1 =i p2 -> p2 =i p1.
Proof. by move => H1 w. Qed.

Lemma iter_fix T (F : T -> T) x k n :
  iter k F x = iter k.+1 F x -> k <= n -> iter n F x = iter n.+1 F x.
Proof.
  move => e. elim: n. rewrite leqn0. by move/eqP<-.
  move => n IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-.
  move/IH => /= IHe. by rewrite -!IHe.
Qed.

Section FixPoint.
  Variable T : finType.
  Definition set_op := {set T} -> {set T}.
  Definition mono (F : set_op) := forall p q : {set T} , p \subset q -> F p \subset F q.

  Variable F : {set T} -> {set T}.
  Hypothesis monoF : mono F.

  Definition lfp := iter #|T| F set0.

  Lemma lfp_ind (P : {set T} -> Type) : P set0 -> (forall s , P s -> P (F s)) -> P lfp.
  Proof.
    move => P0 Pn. rewrite /lfp. set n := #|T|. elim: n => //= n. exact: Pn.
  Qed.

  Lemma iterFsub n : iter n F set0 \subset iter n.+1 F set0.
  Proof.
    elim: n => //=; first by rewrite sub0set.
    move => n IH /=. by apply: monoF.
  Qed.

  Lemma iterFsubn m n : m <= n -> iter m F set0 \subset iter n F set0.
  Proof.
    elim : n; first by rewrite leqn0 ; move/eqP->.
    move => n IH. rewrite leq_eqVlt; case/orP; first by move/eqP<-.
    move/IH => /= IHe. apply: subset_trans; first apply IHe. exact:iterFsub.
  Qed.

  Lemma lfpE : lfp = F lfp.
  Proof.
    suff: exists k : 'I_#|T|.+1 , iter k F set0 == iter k.+1 F set0.
      case => k /eqP E. apply: iter_fix E _. exact: leq_ord.
    apply/existsP. rewrite -[[exists _,_]]negbK negb_exists.
    apply/negP => /forallP => H.
    have/(_ #|T|.+1 (leqnn _)): forall k , k <= #|T|.+1 -> k <= #|iter k F set0|.
      elim => // n IHn Hn.
      apply: leq_ltn_trans (IHn (ltnW Hn)) _. apply: proper_card.
      rewrite properEneq iterFsub andbT. exact: (H (Ordinal Hn)).
    apply/negP. rewrite leqNgt negbK. by rewrite ltnS max_card.
  Qed.

End FixPoint.

Definition cr {X : choiceType} {Y : eqType} {f : X -> Y} (Sf : surjective f) y : X :=
  xchoose (Sf y).

Lemma crK {X : choiceType} {Y : eqType} {f : X->Y} {Sf : surjective f} x: f (cr Sf x) = x.
Proof. by rewrite (eqP (xchooseP (Sf x))). Qed.

Section Quot.
  Variables (T : choiceType) (e : rel T).
  Hypothesis (e_refl: reflexive e) (e_sym : symmetric e) (e_trans : transitive e).

  Definition repr x := choose (e x) x.

  Lemma repr_rel x : e x (repr x).
  Proof. apply: chooseP. exact: e_refl. Qed.

  Lemma repr_idem x : repr x == repr (repr x).
  Proof. rewrite eq_sym. apply/eqP.
    rewrite /repr -{-3}/(repr x) (@eq_choose _ (e (repr x)) (e x)).
    - exact: choose_id (repr_rel _) (e_refl _).
    - move => y. apply/idP/idP. exact: e_trans (repr_rel _).
      apply: e_trans. rewrite e_sym. exact: repr_rel.
  Qed.

  Definition quot := { x : T | x == repr x }.

  Definition Repr (x : T) : quot := Sub (repr x) (repr_idem x).

  Lemma Repr_id x y : reflect (Repr x = Repr y) (e x y).
  Proof.
    apply: (iffP idP) => H.
    - apply: val_inj => /=.
      rewrite /repr (eq_choose (_ : e x =1 e y)).
      + by apply: choose_id; rewrite ?e_refl // e_sym.
      + move => z. by apply/idP/idP; apply e_trans; eauto.
    - inversion H. apply: e_trans (repr_rel _) _.
      by rewrite H1 e_sym repr_rel.
 Qed.
End Quot.