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

Require Import edone bcase.

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

Definition curry aT1 aT2 rT (f : aT1 * aT2 -> rT) a b := f (a,b).
Lemma curryE aT1 aT2 rT (f : aT1 * aT2 -> rT) a b : f (a,b) = curry f a b. done. Qed.

Lemma eqF (T : eqType) (a b : T) : a <> b -> (a == b) = false.
Proof. move => H. apply/negbTE. apply/negP => /eqP. done. Qed.

Lemma classic_orb a b : a || b = a || ~~ a && b.
Proof. bcase. Qed.

Lemma contraN (b : bool) (P : Prop) : b -> ~~ b -> P.
Proof. by case b. Qed.

Lemma contraP (b : bool) (P : Prop) : ~~ b -> b -> P.
Proof. by case b. Qed.

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

Lemma in_sub_has (T:eqType) (a1 a2 : pred T) s :
  {in s, subpred a1 a2} -> has a1 s -> has a2 s.
Proof. move => H /hasP [x ins Ha]. apply/hasP. exists x => //. exact: H. Qed.

Lemma in_sub_all (T : eqType) (a1 a2 : pred T) (s : seq T) :
   {in s, subpred a1 a2} -> all a1 s -> all a2 s.
Proof. move => sub /allP H. apply/allP => x in_s. by firstorder. Qed.

Lemma sub_all_dom (T : eqType) (s1 s2 : seq T) (p : pred T) :
  {subset s1 <= s2} -> all p s2 -> all p s1.
Proof. move => sub /allP H. apply/allP => x /sub. exact: H. Qed.

Lemma all_inP (T : eqType) (s : seq T) p q :
  reflect {in s, subpred p q} (all (fun x => p x ==> q x) s).
Proof. by apply: (iffP allP) => H x /H /implyP. Qed.

Lemma filter_subset (T: eqType) p (s : seq T) : {subset filter p s <= s}.
Proof. apply: mem_subseq. exact: filter_subseq. Qed.

Definition del (T: eqType) (x:T) := filter [pred a | a != x].

Lemma size_del (T: eqType) (x:T) s : x \in s -> size (del x s) < size s.
Proof.
  move => in_s. rewrite size_filter -(count_predC [pred a | a != x]).
  rewrite -{1}[count _ s]addn0 ltn_add2l -has_count.
  apply/hasP. exists x => //. by rewrite inE /= eqxx.
Qed.

Lemma flattenP (T : eqType) (ss : (seq (seq T))) a :
  reflect (exists2 s, s \in ss & a \in s) (a \in flatten ss).
Proof.
  elim: ss => //= [|s0 ss IHss]. rewrite in_nil. constructor => [[s]]. by rewrite in_nil.
  rewrite mem_cat. apply: (iffP orP) => [[H|/IHss [s in_ss in_s]]|[s]].
  - exists s0; by rewrite ?mem_head.
  - exists s => //. by rewrite in_cons in_ss.
  - rewrite in_cons. case/orP => [/eqP->|*]; auto. right. apply/IHss. by eexists.
Qed.

Implicit Arguments SeqSub [T s].

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

Lemma ex_dist i j n : (0 < n) -> exists d, (d < n) && (j == i + d %[mod n]).
Proof.
  move => n0. case: (leqP i j) => H.
  - exists ((j - i) %% n). by rewrite ltn_mod n0 /= modnDmr (subnKC H).
  - exists ((n - i %% n + j %% n) %% n). rewrite ltn_mod n0 /= modnDmr.
    rewrite -(eqn_modDr (i %% n)). set i' := i %% n. set j' := j %% n.
    rewrite -!addnA [j' + _]addnC. rewrite [n - _ +_]addnA subnK.
    by rewrite addnC modnDml eqn_modDl modnDmr modnDl.
    by rewrite ltnW // ltn_mod n0.
Qed.

Lemma unique_dist i j n d d' :
  d < n -> d' < n -> (j = i + d %[mod n]) -> (j = i + d' %[mod n]) -> d = d'.
Proof. move => Hd Hd' -> /eqP. by rewrite eqn_modDl !modn_small // => /eqP. Qed.

Section Dist.
  Variables (T : finType) (Tgt0 : 0 < #|{:T}|).

  Definition dist (s t : T) := xchoose (ex_dist (enum_rank s) (enum_rank t) Tgt0).

  Lemma distP s t : enum_rank t = enum_rank s + dist s t %[mod #|{:T}|].
  Proof.
    apply/eqP.
    by case : (xchooseP (ex_dist (enum_rank s) (enum_rank t) Tgt0)) => /andP [? ?].
  Qed.

  Lemma dist_ltn s t : dist s t < #|{:T}|.
  Proof. by case : (xchooseP (ex_dist (enum_rank s) (enum_rank t) Tgt0)) => /andP [? ?]. Qed.

  Lemma dist0 (s t : T) : dist s t = 0 -> s = t.
  Proof.
    move => D0. move : (distP s t). rewrite D0 addn0.
    rewrite !modn_small ?ltn_ord //. move/ord_inj. move/enum_rank_inj.
    by symmetry.
  Qed.

  Lemma next_subproof (s : T) : (enum_rank s).+1 %% #|{: T}| < #|{: T}|.
  Proof. rewrite ltn_mod. apply/card_gt0P. by exists s. Qed.

  Definition next (s : T) := enum_val (Ordinal (next_subproof s)).

  Lemma distS (s t : T) n : dist s t = n.+1 -> dist (next s) t = n.
  Proof.
    move => Dn. move: (distP s t) => H.
    rewrite Dn -addn1 [_ + 1]addnC addnA addn1 -modnDml in H.
    move: (distP (next s) t) => Dn'. rewrite {1}/next enum_valK /= in Dn'.
    apply: unique_dist Dn' H; last rewrite -Dn ltnW //; exact: dist_ltn.
  Qed.
End Dist.

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).
Proof.
  elim: xs. move => _. exists (fun _ => d) => ?. by rewrite in_nil.
  move => x s IH step.
  have/IH: forall x : T, x \in s -> exists y, R x y.
    move => z ins. apply: step. by rewrite in_cons ins orbT.
  case => f Hf. (case: (step x); first by rewrite mem_head) => y Rxy.
  exists (fun z => if z == x then y else f z) => z.
  rewrite in_cons; case/orP. move/eqP=>e. by rewrite -e ?eq_refl in Rxy *.
  case e: (z == x); first by rewrite (eqP e). exact: Hf.
Qed.

Lemma cardSmC (X : finType) m : (#|X|= m.+1) -> X.
Proof. rewrite cardE. case e: (enum X) => [|x s] //=. Qed.

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).
Proof.
  case n : (#|X|) => [|m].
  - have F : X -> False. move => x. move : (max_card (pred1 x)). by rewrite card1 n.
    exists (fun x => match F x with end) => x. done.
  - move => step.
    have H : forall x, x \in enum X -> exists y, R x y. by move => *.
    case (step (cardSmC n)) => d.
    move/(fin_choice_aux d) : H => [f Hf].
    exists f => x. apply: Hf. by rewrite mem_enum.
Qed.

Lemma fin_choices (T : finType) (P : T -> Prop) (Pdec : forall x, P x \/ ~ P x) :
  exists A : {set T}, forall x, x \in A <-> P x.
Proof.
  pose R x (b :bool) := b <-> P x.
  have/fin_choice [f Hf]: forall x, exists b, R x b.
    move => x. case (Pdec x); [by exists true|by exists false].
  exists (finset f) => x. rewrite inE. exact: Hf.
Qed.

Ltac rightb := apply/orP; right.
Ltac leftb := apply/orP; left.
Ltac existsb s := apply/hasP; exists s.