Require Import ssreflect ssrbool eqtype ssrnat seq.
Require Import ssrfun choice fintype finset path fingraph bigop.
Require Import Relations.
Require Import tactics.

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

Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
Proof. move => Hmn. exact:leq_trans. Qed.

Lemma orS b1 b2 : ( b1 || b2 ) -> {b1} + {b2}.
Proof. case: b1 b2 => [|] [|] //= _; first [by left| by right]. Qed.

Lemma introP' (P:Prop) (b:bool) : (P -> b) -> (b -> P) -> reflect P b.
Proof. case : b => ? ?; by constructor; auto. Qed.

Lemma setD1id (T : finType) (A : {set T}) x : A :\ x == A = (x \notin A).
Proof.
  apply/eqP/idP => [|e]; [move/setDidPl|apply/setDidPl];
    rewrite disjoint_sym (@eq_disjoint1 _ x) // => ?; by rewrite in_set.
Qed.

Lemma wf_proper (T : finType) : well_founded (fun x y : {set T} => y \proper x).
Proof.
  apply : Wf_nat.well_founded_lt_compat.
  instantiate (1 := fun x => #|T| - #|x|).
  move => x y. rewrite properEcard. case/andP => H H'.
  apply/leP. rewrite ltn_sub2l //.
  apply : ltn_leq_trans ; first by apply H'.
  by rewrite max_card.
Qed.

Lemma set1sub (T : finType) (x : T) (A : {set T}) : ([set x] \subset A) = (x \in A).
Proof.
  apply/subsetP/idP. apply. by rewrite in_set1. move => H y. rewrite in_set1. by move/eqP->.
Qed.

Lemma properU1 (T : finType) (A : {set T}) x : (x \notin A) -> (A \proper x |: A).
Proof. rewrite -set1sub. exact: properUr. Qed.

Lemma enum1s (T : finType) (x : T) : enum [set x] = [:: x].
Proof. rewrite -(@eq_enum _ (pred1 x)) ?enum1 // => y. by rewrite !inE. Qed.

Lemma slack_ind (T : finType) (P : {set T} -> Type) :
  (forall A : {set T}, (forall B : {set T}, A \proper B -> P B) -> P A) -> forall A : {set T}, P A.
Proof. move => IS A. elim: (wf_proper A) => {A} A B. exact: IS. Qed.

Lemma set1mem (T:finType) (A : {set T}) x : x \in A -> A = x |: A.
Proof.
  move => inA. apply/setP => y. apply/idP/setUP; first tauto.
  by case => [/set1P ->|->].
Qed.

Implicit Arguments SeqSub [T s].

Section TreeCountType.

  Variable X : countType.

  Inductive tree := Node : X -> (seq tree) -> tree.

  Section TreeInd.
    Variable P : tree -> Type.
    Variable P' : seq (tree) -> Type.

    Hypothesis Pnil : forall x , P (Node x [::]).
    Hypothesis Pcons : forall x xs, P' xs -> P (Node x xs).

    Hypothesis P'nil : P' nil.
    Hypothesis P'cons : forall t ts , P t -> P' ts -> P' (t::ts).

    Lemma tree_rect' : forall t , P t.
    Proof.
      fix 1. case => t ts.
      apply : Pcons. elim : ts => [|t' tr]. apply : P'nil.
      apply : P'cons. apply tree_rect'.
    Qed.
  End TreeInd.

  Lemma tree_eq_dec : forall (x y : tree) , { x = y } + { x <> y }.
  Proof.
    fix 1.
    have trees_eq_dec : forall (xs ys : seq tree) , { xs = ys } + { xs <> ys }.
      fix trees_eq_dec 1. case => [|x xs]; case => [|y ys]; try by [left | right].
      case (tree_eq_dec x y). move->. case (trees_eq_dec xs ys). move-> ; by left.
      move => H. right; injection. apply H. move => H. right; injection => _ . by apply H.
    case => x ts . case => y ts'. case e : (x == y). rewrite (eqP e).
    case (trees_eq_dec ts ts'); first by move-> ; left. move => H. right. injection. apply H.
    right; injection => _ ?; subst. by rewrite eq_refl in e.
  Qed.

  Definition tree_eqMixin := EqMixin (compareP (@tree_eq_dec)).
  Canonical Structure tree_eqType := Eval hnf in @EqType tree tree_eqMixin.

  Section SimpleTreeInd.
    Variable P : tree -> Type.

    Hypothesis Pnil : forall x , P (Node x [::]).
    Hypothesis Pcons : forall x xs , (forall y , y \in xs -> P y) -> P (Node x xs).

    Lemma simple_tree_rect : forall t , P t.
    Proof.
      apply: (tree_rect' (P' := fun xs => forall y , y \in xs -> P y)) => //.
      move => t ts Pt H y. rewrite in_cons. case/orS. by move/eqP ->. apply: H.
    Qed.
  End SimpleTreeInd.

  Fixpoint t_pickle (t : tree) : seq (X * nat) :=
    let: Node x ts := t in (x, (size ts)) :: flatten (map t_pickle ts).

  Fixpoint t_parse (xs : seq (X * nat)) :=
    match xs with
      | [::] => [::]
      | (x,n) :: xr => let: ts := t_parse xr in Node x (take n ts) :: drop n ts
    end.

  Definition t_unpickle := ohead \o t_parse.

  Lemma t_inv : pcancel t_pickle t_unpickle.
  Proof.
    elim/simple_tree_rect => x xs H.
    rewrite /t_unpickle /=. do 2 f_equal. rewrite /t_unpickle /comp /= in H.
    elim : xs H => //= t ts IHts H.
    Lemma parse_pickle_xs t xs : t_parse (t_pickle t ++ xs) = t :: t_parse xs.
      elim/simple_tree_rect : t xs => x ts IH xs /=. do 2 f_equal.
      - elim : ts IH => //= ; first by move => H; rewrite take0.
        move => t tr IHtr H. rewrite -catA H //= ; last by rewrite in_cons eq_refl.
        f_equal. apply : IHtr. move => y Hy xs'. by rewrite H //= in_cons Hy.
      - elim : ts IH => //= ; first by move => H; rewrite drop0.
        move => t tr IHtr H. rewrite -catA H //= ; last by rewrite in_cons eq_refl.
        apply IHtr. move => y Hy xs'. by rewrite H //= in_cons Hy.
    Qed.
    rewrite parse_pickle_xs /= IHts //=. move => y Hy. by rewrite H //= in_cons Hy.
  Qed.

  Definition tree_countMixin := PcanCountMixin t_inv.
  Definition tree_choiceMixin := CountChoiceMixin tree_countMixin.

  Canonical Structure tree_ChoiceType := Eval hnf in ChoiceType tree tree_choiceMixin.
  Canonical Structure tree_CountType := Eval hnf in CountType tree tree_countMixin.

End TreeCountType.

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 mu := iter #|T|.+1 F set0.

  Lemma mu_ind (P : {set T} -> Type) : P set0 -> (forall s , P s -> P (F s)) -> P mu.
  Proof.
    move => P0 Pn. rewrite /mu. set n := #|T|.+1. 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 muE : mu = F mu.
  Proof.
    have: ~~ forallb m : 'I_#|T|.+1 , iter m F set0 \proper iter m.+1 F set0.
      apply/negP => /forallP H.
      have P : forall n : 'I_#|T|.+1 , exists x : T , x \in iter n.+1 F set0 :\: iter n F set0.
        move => n ; move : (H n). case/properP => _ [x x1 x2]. exists x. by rewrite in_setD x1 x2.
      pose i (o : 'I_#|T|.+1) : T := xchoose (P o).
      have inj_i : injective i.
        move => o o'. rewrite /i => e. move : (xchooseP (P o)) (xchooseP (P o')).
        rewrite e {e}. set x := xchoose _. move : o o' x => [n pn] [m pm] x.
        rewrite !in_setD /=. case/andP => Hn1 Hn2. case/andP => Hm1 Hm2.
        case (ltngtP n m); last by move/eqP => e'; apply/eqP.
        - move => /iterFsubn /subsetP /(_ x Hn2). by rewrite (negbTE Hm1).
        - move => /iterFsubn /subsetP /(_ x Hm2). by rewrite (negbTE Hn1).
      move : (max_card (codom i)). by rewrite (card_codom inj_i) /= !card_ord ltnn.
    rewrite negb_forall. case/existsP => x H.
    have A : iter x F set0 = iter x.+1 F set0.
      apply/eqP. by rewrite eqEproper iterFsub /= H.
    apply : iter_fix; first apply A. by case:x {H A} => *; auto.
  Qed.
End FixPoint.