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

Import Prenex Implicits.

Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.

Lemma orS b1 b2 : ( b1 || b2 ) -> {b1} + {b2}.

Lemma introP' (P:Prop) (b:bool) : (P -> b) -> (b -> P) -> reflect P b.

Lemma setD1id (T : finType) (A : {set T}) x : A :\ x == A = (x \notin A).

Lemma wf_proper (T : finType) : well_founded (fun x y : {set T} => y \proper x).

Lemma set1sub (T : finType) (x : T) (A : {set T}) : ([set x] \subset A) = (x \in A).

Lemma properU1 (T : finType) (A : {set T}) x : (x \notin A) -> (A \proper x |: A).

Lemma enum1s (T : finType) (x : T) : enum [set x] = [:: x].

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.

Lemma set1mem (T:finType) (A : {set T}) x : x \in A -> A = x |: A.

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.
  End TreeInd.

  Lemma tree_eq_dec : forall (x y : tree) , { x = y } + { x <> y }.

  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.
  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.
    Lemma parse_pickle_xs t xs : t_parse (t_pickle t ++ xs) = t :: t_parse xs.
  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.

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.

  Lemma iterFsub n : iter n F set0 \subset iter n.+1 F set0.

  Lemma iterFsubn m n : m <= n -> iter m F set0 \subset iter n F set0.

  Lemma muE : mu = F mu.
End FixPoint.