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}.
Sequences
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).
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 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.
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 FixPoint.
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