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 path_rcons T (e : rel T) p x y :
  path e x (rcons p y) = (path e x p && e (last x p) y).

Definition xchoose2_sig (T : choiceType) (p q : pred T) :
  (exists2 x , p x & q x) -> {x : T & p x & q x}.

Lemma predC_involutive (X:Type) (p : pred X) x : predC (predC p) x = p x.

Lemma ex2E X (p q : pred X) : (exists2 x , p x & q x) <-> exists x, p x && q x.

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

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

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

Lemma reflectPn P p : reflect P p -> reflect (~ P) (~~ p).

Lemma contra' (P Q : Prop) : (P -> Q) -> ~ Q -> ~P.

Lemma connectP' (T : finType) (r : rel T) a b : reflect (clos_refl_trans T r a b) (connect r a b).

Lemma leq1 n : n <= 1 = (n == 0) || (n == 1).

Lemma cards_leq1P (X : finType) (A : {set X}) :
  reflect (forall x y , x \in A -> y \in A -> x = y) (#|A| <= 1).

Implicit Arguments SeqSub [T s].

Section finset.
  Variables (T : choiceType) (xs : seq T).

  Definition msval (X : {set seq_sub xs}) (x : T) :=
  (if x \in xs is true as b return (x \in xs = b -> bool)
    then fun H => SeqSub x H \in X
    else xpred0) (refl_equal _).

  Lemma msvalP (X : {set seq_sub xs}) (x : T) :
    reflect (exists H : x \in xs , SeqSub x H \in X) (msval X x).

  Lemma msvalE x (X : {set seq_sub xs}) H : SeqSub x H \in X = msval X x.
End finset.

Notation "x \in' X" := (msval X x) (at level 20).

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.

Inductive norm (X : Type) (R : X -> X -> Prop) : X -> Prop :=
  normI x : (forall y , R x y -> norm R y) -> norm R x.

Definition sn X (R : X -> X -> Prop) := forall x, norm R x.

Lemma normEn (X:finType) (e : rel X) x : ~ norm e x -> existsb y , e x y.

Definition decidable X P := forall x : X, {P x} + {~ P x}.
Definition decidable2 X Y R := forall (x : X) (y : Y) , {R x y} + {~ R x y}.

Lemma decidable_reflect X P :
  decidable P -> {p : pred X & forall x , reflect (P x) (p x)}.

Lemma reflect_decidable X P :
  {p : pred X & forall x , reflect (P x) (p x)} -> decidable P.

Lemma classicF (P:Prop) : (P -> False) -> (~ P -> False) -> False.
Implicit Arguments classicF [].

Lemma classicb (P:Prop) (b:bool) : (P -> b) -> (~ P -> b) -> b.
Implicit Arguments classicb [].

Lemma deMorganb (P Q : Prop) (b : bool) : ((~P \/ ~Q) -> b) <-> (~ (P /\ Q) -> b).

Lemma dnb (P : Prop) (b : bool) : (P -> b) <-> (~ ~ P -> b).

Lemma deMorganE (X:Type) (P : X -> Prop) :
  (~ exists x , P x) -> (forall x , ~ P x).

Lemma deMorganAb (X:Type) (p : X -> bool) (b : bool) :
  ((exists x , ~~ p x) -> b) -> (~ forall x , p x) -> b.

Lemma deMorganE2 (Y: Type) (P Q : Y -> Prop) :
  ~ (exists2 x, P x & Q x) -> forall x, P x -> ~ Q x.

Lemma reflect_DN P p : reflect P p -> ~ ~ P -> P.

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

Lemma fin_choice_aux (T : choiceType) T' (d : T') (R : T -> T' -> Prop) (xs : seq T) :
  (forall x, x \in xs -> exists y, R x y) -> exists f , forall x, x \in xs -> R x (f x).

Lemma cardSmC (X : finType) m : (#|X|= m.+1) -> X.

Lemma fin_choice (X : finType) Y (R : X -> Y -> Prop) :
  (forall x : X , exists y , R x y) -> exists f, forall x , R x (f x).