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.
Require Import ssrfun choice fintype finset path fingraph div bigop.
Require Import Relations.
Require Import edone bcase.
Set Implicit Arguments.
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.
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].
uniq s -> size m1 == size s -> size m2 == size s -> mask m1 s =i mask m2 s -> m1 == m2.
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.
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.
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