Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.

Require Import Relations.
Require Import edone bcase.

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

Lemma forall_inPn (T : finType) (p q : pred T) :
  reflect (exists2 x, p x & ~~ q x) (~~ [∀ (x | p x), q x]).
Proof.
  rewrite negb_forall (eq_existsb (P2 := fun x ⇒ p x && ~~ q x)) ⇒ [|x].
  exact: exists_inP. exact: negb_imply.
Qed.

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 hasS (T : eqType) (p : pred T) s : has p s → {a : T | a \in s & p a}.
Proof.
  case: s ⇒ // b s H. pose a := (nth b (b :: s) (find p (b :: s))).
  ∃ a ; by rewrite ?mem_nth -?has_find ?nth_find.
Qed.

Lemma forall_nil (T : eqType) (P : T → Prop) :
  (∀ x, x \in nil → P x) ↔ True.
Proof. intuition. by rewrite in_nil in H0. Qed.

Lemma forall_cons (T : eqType) (P : T → Prop) a s :
  (∀ x, x \in a :: s → P x) ↔ P a ∧ (∀ x, x \in s → P x).
Proof.
  firstorder using mem_head. by apply H; rewrite in_cons H0.
  rewrite in_cons in H0. case/predU1P : H0 ⇒ [->//|]. exact: H1.
Qed.

Lemma sub_behead (T : eqType) x (xs ys : seq T) :
  {subset x :: xs ≤ ys} → {subset xs ≤ ys}.
Proof. move ⇒ sub a H. apply: sub. by rewrite inE H orbT. Qed.

Lemma sumn_bound n (s : seq nat) :
  (∀ x, x \in s → x ≤ n) → sumn s ≤ n × size s.
Proof.
  elim: s ⇒ //= m s IHs H. rewrite mulnS leq_add ?H ?IHs ? mem_head //.
  move ⇒ x Hx. by rewrite H //= in_cons Hx.
Qed.

Lemma nilp_map aT rT (f : aT → rT) s : nilp (map f s) = nilp s.
Proof. by case: s. 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. ∃ 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 sub_has_dom (T : eqType) (s1 s2 : seq T) (p : pred T) :
  {subset s2 ≤ s1} → has p s2 → has p s1.
Proof. move ⇒ H /hasP [x /H Hx] ?. by apply/hasP; ∃ x. 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. ∃ 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]].
  - ∃ s0; by rewrite ?mem_head.
  - ∃ s ⇒ //. by rewrite in_cons in_ss.
  - rewrite in_cons. case/orP ⇒ [/eqP->|*]; auto. right. apply/IHss. by eexists.
Qed.

Lemma mask_inj (T : eqType) (m1 m2 : bitseq) (s : seq T) :
  uniq s → size m1 == size s → size m2 == size s → mask m1 s =i mask m2 s → m1 == m2.
Proof.
  elim: s m1 m2 ⇒ [m1 m2|a s IHs [|b1 m1] [|b2 m2] // U S1 S2 E].
  - by rewrite /= !size_eq0 ⇒ _ /eqP→ /eqP→.
  - rewrite /= in U. move: U ⇒ /andP[U1 U2].
    have mask_s : a \in mask _ s = false.
      move ⇒ b. apply: contraNF U1. exact: mem_mask.
    move: (E a). rewrite !mem_mask_cons !eqxx !andbT !mask_s !orbF ⇒ b12.
    rewrite eqseq_cons b12 eqxx IHs // ⇒ b.
    move: (E b). rewrite !mem_mask_cons.
    case: (boolP (b == a)) ⇒ [/eqP->|_]; by rewrite ?mask_s // ?andbF.
Qed.

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 LeastFixPoint.
  Variable T : finType.
  Definition set_op := {set T} → {set T}.
  Definition mono (F : set_op) := ∀ 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 → (∀ 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: ∃ 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 -[[∃ _,_]]negbK negb_exists.
    apply/negP ⇒ /forallP ⇒ H.
    have/(_ #|T|.+1 (leqnn _)): ∀ 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 LeastFixPoint.

Section GreatestFixPoint.
  Variable (T : finType) (F : {set T} → {set T}).
  Hypothesis F_mono : mono F.

  Let F' A := ~: F (~: A).

  Lemma mono_F' : mono F'.
  Proof. move ⇒ A B. rewrite /F' -setCS [~: F _ \subset _]setCS. exact: F_mono. Qed.

  Definition gfp := ~: lfp F'.

  Lemma gfpE : gfp = F gfp.
  Proof. by rewrite /gfp {1}(lfpE mono_F') setCK. Qed.

  Lemma gfp_ind (P : {set T} → Type) :
    P setT → (∀ s , P s → P (F s)) → P gfp.
  Proof.
    move ⇒ H1 H2. rewrite /gfp /F'.
    apply lfp_ind ⇒ [|A]; rewrite ?setC0 ?setCK //. exact: H2.
  Qed.

  Lemma gfp_ind2 (P : T → Type) :
    (∀ x (X : {set T}), (∀ y, P y → y \in X) → P x → x \in F X) →
    ∀ x, P x → x \in gfp.
  Proof. move ⇒ H. apply gfp_ind ⇒ [x|*]; first by rewrite inE. exact: H. Qed.

End GreatestFixPoint.

Lemma ex_dist i j n : (0 < n) → ∃ d, (d < n) && (j == i + d %[mod n]).
Proof.
  move ⇒ n0. case: (leqP i j) ⇒ H.
  - ∃ ((j - i) %% n). by rewrite ltn_mod n0 /= modnDmr (subnKC H).
  - ∃ ((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/andP: (xchooseP (ex_dist (enum_rank s) (enum_rank t) Tgt0)).
  Qed.

  Lemma dist_ltn s t : dist s t < #|{:T}|.
  Proof. by case/andP: (xchooseP (ex_dist (enum_rank s) (enum_rank t) Tgt0)). 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 ∃ 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) :
  (∀ x, x \in xs → ∃ y, R x y) → ∃ f , ∀ x, x \in xs → R x (f x).
Proof.
  elim: xs. move ⇒ _. ∃ (fun _ ⇒ d) ⇒ ?. by rewrite in_nil.
  move ⇒ x s IH step.
  have/IH: ∀ x : T, x \in s → ∃ 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.
  ∃ (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) :
  (∀ x : X , ∃ y , R x y) → ∃ f, ∀ 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.
    ∃ (fun x ⇒ match F x with end) ⇒ x. done.
  - move ⇒ step.
    have H : ∀ x, x \in enum X → ∃ y, R x y. by move ⇒ ×.
    case (step (cardSmC n)) ⇒ d.
    move/(fin_choice_aux d) : H ⇒ [f Hf].
    ∃ f ⇒ x. apply: Hf. by rewrite mem_enum.
Qed.

Lemma fin_choices (T : finType) (P : T → Prop) (Pdec : ∀ x, P x ∨ ¬ P x) :
  ∃ A : {set T}, ∀ x, x \in A ↔ P x.
Proof.
  pose R x (b :bool) := b ↔ P x.
  have/fin_choice [f Hf]: ∀ x, ∃ b, R x b.
    move ⇒ x. case (Pdec x); [by ∃ true|by ∃ false].
  ∃ (finset f) ⇒ x. rewrite inE. exact: Hf.
Qed.

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

Definition XM := ∀ P : Prop, P ∨ ¬ P.