Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrfun ssrnat seq ssrbool eqtype fintype choice finset.
Set Implicit Arguments.
Import Prenex Implicits.
Set Implicit Arguments.
Import Prenex Implicits.
Lemma all1s {T : eqType} {a : T} {s} {P : T -> Prop} :
(forall b, b \in a :: s -> P b) -> P a /\ (forall b, b \in s -> P b).
Lemma leq_eq n m: n <= m -> m <= n -> n = m.
Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|.
Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
Lemma set1mem (T : finType) (A : {set T}) x : x \in A -> A = x |: A.
Lemma set_pick_size {F : finType} (X : {set F}) z : [pick z in X] = Some z -> #|X :\ z| < #|X|.
Definition surjective {X : eqType} {Y} (f : Y -> X) := forall x, exists w, f w == x.
Lemma surjectiveE (rT aT : finType) (f : aT -> rT) : surjective f -> #|codom f| = #|rT|.
Lemma surj_card_bij (T T' : finType) (f : T -> T') :
surjective f -> #|T| = #|T'| -> bijective f.
Lemma size_induction {X : Type} (f : X -> nat) (p : X ->Prop) :
( forall x, ( forall y, f y < f x -> p y) -> p x) -> forall x, p x.
Lemma ptrans {T} (p1 p2 p3 : pred T) : p1 =i p2 -> p2 =i p3 -> p1 =i p3.
Lemma psym {T} (p1 p2 : pred T) : p1 =i p2 -> p2 =i p1.
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.
Definition cr {X : choiceType} {Y : eqType} {f : X -> Y} (Sf : surjective f) y : X :=
xchoose (Sf y).
Lemma crK {X : choiceType} {Y : eqType} {f : X->Y} {Sf : surjective f} x: f (cr Sf x) = x.
Section Quot.
Variables (T : choiceType) (e : rel T).
Hypothesis (e_refl: reflexive e) (e_sym : symmetric e) (e_trans : transitive e).
Definition repr x := choose (e x) x.
Lemma repr_rel x : e x (repr x).
Lemma repr_idem x : repr x == repr (repr x).
Definition quot := { x : T | x == repr x }.
Definition Repr (x : T) : quot := Sub (repr x) (repr_idem x).
Lemma Repr_id x y : reflect (Repr x = Repr y) (e x y).
End Quot.
Variables (T : choiceType) (e : rel T).
Hypothesis (e_refl: reflexive e) (e_sym : symmetric e) (e_trans : transitive e).
Definition repr x := choose (e x) x.
Lemma repr_rel x : e x (repr x).
Lemma repr_idem x : repr x == repr (repr x).
Definition quot := { x : T | x == repr x }.
Definition Repr (x : T) : quot := Sub (repr x) (repr_idem x).
Lemma Repr_id x y : reflect (Repr x = Repr y) (e x y).
End Quot.