# Library libs.base

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.
Import Prenex Implicits.

# Generic Lemmas not in Ssreflect

Boolean Logic

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.

Lemma eqF (T : eqType) (a b : T) : a <> b -> (a == b) = false.

Lemma classic_orb a b : a || b = a || ~~ a && b.

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

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

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

Lemma hasS (T : eqType) (p : pred T) s : has p s -> {a : T | a \in s & p a}.

Sequences

Lemma sumn_bound n (s : seq nat) :
(forall x, x \in s -> x <= n) -> sumn s <= n * size s.

Lemma nilp_map aT rT (f : aT -> rT) s : nilp (map f s) = nilp s.

Lemma in_sub_has (T:eqType) (a1 a2 : pred T) s :
{in s, subpred a1 a2} -> has a1 s -> has a2 s.

Lemma in_sub_all (T : eqType) (a1 a2 : pred T) (s : seq T) :
{in s, subpred a1 a2} -> all a1 s -> all a2 s.

Lemma sub_all_dom (T : eqType) (s1 s2 : seq T) (p : pred T) :
{subset s1 <= s2} -> all p s2 -> all p s1.

Lemma all_inP (T : eqType) (s : seq T) p q :
reflect {in s, subpred p q} (all (fun x => p x ==> q x) s).

Lemma filter_subset (T: eqType) p (s : seq T) : {subset filter p s <= s}.

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.

Lemma flattenP (T : eqType) (ss : (seq (seq T))) a :
reflect (exists2 s, s \in ss & a \in s) (a \in flatten ss).

Injectivity of bitmasking. Required for the size of the powerset.
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.

Implicit Arguments SeqSub [T s].

## A least fixed point operator for finType

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

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 lfpE : lfp = F lfp.

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

Definition gfp := ~: lfp F'.

Lemma gfpE : gfp = F gfp.

Lemma gfp_ind (P : {set T} -> Type) :
P setT -> (forall s , P s -> P (F s)) -> P gfp.

Lemma gfp_ind2 (P : T -> Type) :
(forall x (X : {set T}), (forall y, P y -> y \in X) -> P x -> x \in F X) ->
forall x, P x -> x \in gfp.

End GreatestFixPoint.

## Cyclic directed distance

Lemma ex_dist i j n : (0 < n) -> exists d, (d < n) && (j == i + d %[mod n]).

Lemma unique_dist i j n d d' :
d < n -> d' < n -> (j = i + d %[mod n]) -> (j = i + d' %[mod n]) -> d = d'.

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

Lemma dist_ltn s t : dist s t < #|{:T}|.

Lemma dist0 (s t : T) : dist s t = 0 -> s = t.

Lemma next_subproof (s : T) : (enum_rank s).+1 %% #|{: T}| < #|{: T}|.

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

Finite Choice Principles

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

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.

Some tactic notations for boolean logical connectives
Ltac rightb := apply/orP; right.
Ltac leftb := apply/orP; left.
Ltac existsb s := apply/hasP; exists s.