Library eqrel
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import ssrnat.
Require Import general.
Require Import finfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section EqRel.
Variable d: finType.
Record eqrelType: Type := Eqrel {
erel: rel d;
erel_refl: forall x, erel x x;
erel_sym: forall x y, erel x y -> erel y x;
erel_trans: forall x y z, erel x y -> erel y z -> erel x z
}.
Implicit Arguments Eqrel [].
Lemma classes_equal: forall r x y, (erel r x y) -> (erel r x) =1 (erel r y).
move=> r x y R z.
apply: iffB=>[S|S].
apply (erel_trans (erel_sym R) S).
apply (erel_trans R S).
Qed.
Definition set_rel(r: eqrelType): pred {d * d :as finType}.
Proof.
move=>r [x y].
exact (erel r x y).
Defined.
Definition canonical_fun (r: eqrelType) (x: d) :=
if (pick ((erel r) x)) is Some y then y else x.
Lemma canonical_elem: forall r x, (erel r) x (canonical_fun r x).
Proof.
move=>r x.
rewrite /canonical_fun.
case: (pickP ((erel r) x))=>//=.
by rewrite erel_refl.
Qed.
Lemma canonical_congr1: forall r x y, (erel r) x y -> (canonical_fun r x) == (canonical_fun r y) .
Proof.
move=> r x y H.
rewrite /canonical_fun.
have U: (erel r x) =1 (erel r y). by apply classes_equal.
rewrite (eq_pick U).
case: (pickP ((erel r) y))=>[z _|I]//=.
by case: (I y); rewrite erel_refl.
Qed.
Lemma canonical_inj1: forall r x y, (canonical_fun r x) == (canonical_fun r y) -> (erel r) x y.
Proof.
move=> r x y H.
have K: (erel r x (canonical_fun r x)) by apply canonical_elem.
have L: (erel r (canonical_fun r y) y) by apply (erel_sym (canonical_elem r y)).
by rewrite (eqP H) in K; apply (erel_trans K L).
Qed.
Lemma canonical_congr: forall r s, (erel r =2 erel s) -> (canonical_fun r) =1 (canonical_fun s).
Proof.
move=>r s E x.
rewrite /canonical_fun.
by rewrite (eq_pick (E x)).
Qed.
Lemma canonical_inj: forall r s, (canonical_fun r) =1 (canonical_fun s) -> (erel r =2 erel s).
Proof.
move=>r s E x y.
have H: forall u v, (canonical_fun u) =1 (canonical_fun v) -> (erel u x y) -> (erel v x y).
by move=>u v F rxy; apply: canonical_inj1; rewrite -!F; apply canonical_congr1.
case U: (erel r x y).
by rewrite (H r s E).
case V: (erel s x y)=>//=.
by rewrite (H s r (fsym E)) in U.
Qed.
Define an intensional representation of equivalence relation, in order to
define finite equivalence relations as a finite type with decidable equality.
The intensional representation consists of a finite function that maps each
element of the base type to a canonical representative of its equivalence
class.
Definition ieqrelType: finType := finFun d d.
Definition ieqrelType_of_eqrel: eqrelType -> ieqrelType :=
fun r => (fgraph_of_fun (canonical_fun r)).
Definition eqrel_of_ieqrelType: ieqrelType -> eqrelType.
Proof.
move=>rf.
apply (Eqrel (fun x y => rf x == rf y))=>//=.
by move=>x y H; rewrite (eq_sym (rf y) (rf x)).
by move=>x y z; move/eqP=>H; move/eqP=> K; apply/eqP; rewrite H K.
Defined.
Lemma eqrel_of_ieqrelType_congr: forall r s,
r == s -> erel (eqrel_of_ieqrelType r) =2 erel (eqrel_of_ieqrelType s).
move=>r s E x y.
by case: (eqP E)=>[->].
Qed.
Lemma ieqrelType_of_eqrel_congr: forall r s,
erel r =2 erel s -> (ieqrelType_of_eqrel r) == (ieqrelType_of_eqrel s).
move=>r s E.
rewrite /ieqrelType_of_eqrel //=.
apply/eqP. apply: fgraph_of_fun_congr.
move=>x.
rewrite /canonical_fun.
by rewrite (eq_pick (E x)).
Qed.
A type of intensional equivalence relations that corresponds exactly
to the extensional one.
Definition ieqrel_pred: pred (finFun d d) :=
fun f => ieqrelType_of_eqrel (eqrel_of_ieqrelType f) == f.
Record ieqrel: Type := ieqrelI { ieqrelE: sub_finType ieqrel_pred } .
Definition eqd_ieqrel(r s: ieqrel): bool.
case=>r; case=>s; exact (r == s).
Defined.
Lemma eqd_ieqrelPx: reflect_eq eqd_ieqrel.
Proof.
case=>r; case=>s.
rewrite /eqd_ieqrel.
elim: (@eqP _ r s)=>[->|]//=.
by apply: Reflect_true.
by move=>*; apply: Reflect_false; case.
Qed.
Canonical Structure ieqrelData := EqType eqd_ieqrelPx.
Lemma ieqrel_eqd: forall r s:ieqrel, ieqrelE r == ieqrelE s -> r == s.
Proof. by case=>r; case=>s. Qed.
Definition ieqrel_enum: seq ieqrelData :=
maps ieqrelI (enum (sub_finType ieqrel_pred)).
Lemma ieqrel_enumP: forall r:ieqrel, count (pred1 r) ieqrel_enum = 1.
Proof.
case=>r.
rewrite /ieqrel_enum count_maps /comp.
rewrite (eq_count (a2:=pred1 r)).
by rewrite FinType.enumP.
by move=>x//=.
Qed.
Canonical Structure ieqrelFin := FinType ieqrel_enumP.
Lemma ieqrel_of_eqrelP: forall r, ieqrel_pred (ieqrelType_of_eqrel r).
Proof.
move=>r.
rewrite /ieqrel_pred {1 3}/ieqrelType_of_eqrel.
apply/eqP; apply: fgraph_of_fun_congr.
move=>*; apply canonical_congr.
move=>x y.
rewrite [ieqrelType_of_eqrel]lock /= -lock.
rewrite /ieqrelType_of_eqrel !fgraph_fun_eq.
case U: (erel r x y)=>//=.
rewrite canonical_congr1 //=.
elim: (canonical_fun r x == canonical_fun r y)
(canonical_inj1 (r:=r) (x:=x) (y:=y)) => //=.
by rewrite U; move=>H; rewrite H.
Save.
Definition ieqrel_of_eqrel: eqrelType -> ieqrel.
Proof.
move=>r.
apply: ieqrelI.
apply: EqSig (ieqrel_of_eqrelP r).
Defined.
Definition eqrel_of_ieqrel: ieqrel -> eqrelType.
Proof.
case; move=>[r _].
exact (eqrel_of_ieqrelType r).
Defined.
Coercion eqrel_of_ieqrel: ieqrel >-> eqrelType.
Lemma eqrel_of_ieqrel_congr: forall r s:ieqrel,
r == s -> erel (eqrel_of_ieqrel r) =2 erel (eqrel_of_ieqrel s).
move=>r s E x y.
by case: (eqP E)=>[->].
Qed.
Lemma ieqrel_of_eqrel_congr: forall r s,
erel r =2 erel s -> (ieqrel_of_eqrel r) == (ieqrel_of_eqrel s).
move=>r s E.
apply: ieqrel_eqd.
rewrite -val_eqE /ieqrel_of_eqrel //=.
by apply: ieqrelType_of_eqrel_congr.
Qed.
Lemma eqrel_of_ieqrel_inj: forall ri si:ieqrel,
((erel (eqrel_of_ieqrel ri)) =2 (erel (eqrel_of_ieqrel si))) -> ri == si.
Proof.
case=>ri; case=>si; move=>E.
apply: ieqrel_eqd; rewrite -val_eqE.
case: ri E=>[ri ri_mem E]=>//=.
case: si E=>[si si_mem /=E]=>//=.
rewrite /ieqrel_pred in ri_mem si_mem.
rewrite -(eqP ri_mem) -(eqP si_mem).
apply ieqrelType_of_eqrel_congr.
apply E.
Qed.
Lemma ieqrel_of_eqrel_inj: forall r s,
(ieqrel_of_eqrel r) == (ieqrel_of_eqrel s) -> erel r =2 erel s.
Proof.
move=>r s E x y.
apply: canonical_inj.
have U:(val (ieqrelE (ieqrel_of_eqrel r)) = val (ieqrelE (ieqrel_of_eqrel s)))
by rewrite (eqP E).
rewrite /ieqrel_of_eqrel /ieqrelType_of_eqrel /= in U.
by apply: fgraph_of_fun_inj.
Qed.
Lemma ieqrel_eqrel: forall r , (ieqrel_of_eqrel (eqrel_of_ieqrel r)) == r.
Proof.
move=>r.
have H: (val (ieqrelE (ieqrel_of_eqrel (eqrel_of_ieqrel r))) == val (ieqrelE r)).
by case:r; case.
rewrite val_eqE in H.
by apply ieqrel_eqd.
Qed.
Lemma eqrel_ieqrel: forall r ,
erel (eqrel_of_ieqrel (ieqrel_of_eqrel r)) =2 erel r.
Proof.
move=>r.
apply ieqrel_of_eqrel_inj.
by rewrite (eqP (ieqrel_eqrel (ieqrel_of_eqrel r))) eq_refl.
Qed.
Equivalence classes, given by canonical representatives
Definition eqclasses(r: eqrelType) := image (canonical_fun r) d.
Quotients
Definition quotient(r: eqrelType) := sub_finType (eqclasses r).
Choice of canonical elements from equivalence classes
Definition pickeqc(r:eqrelType): (quotient r) -> d.
by move=>r; elim=>x x_mem; exact x.
Defined.
Lemma pickeqc_eqd: forall r (u v:quotient r),
erel r (pickeqc u) (pickeqc v) -> u == v.
Proof.
move=>r [u um] [v vm] /=.
rewrite -val_eqE /=.
elim: (image_exists um)=>x ->.
elim: (image_exists vm)=>y ->.
move=>rxy.
apply: canonical_congr1.
apply (@erel_trans r x (canonical_fun r x)).
apply: canonical_elem.
apply (@erel_trans r (canonical_fun r x) (canonical_fun r y))=>//.
apply: erel_sym.
apply: canonical_elem.
Qed.
Definition eqclass(r:eqrelType): d -> (quotient r).
Proof.
move=>r x.
apply: (@EqSig d (eqclasses r) (canonical_fun r x)).
rewrite /eqclasses /image /preimage /disjoint /predI /pred0b /card.
apply/negP=>H.
have K: has (fun x0=>(canonical_fun r x == canonical_fun r x0) && d x0) (enum d).
by apply/hasP; exists x; (rewrite mem_enum || (apply/andP; rewrite eq_refl)).
by rewrite has_count (eqP H) in K.
Defined.
Lemma eqclass_eq(r:eqrelType): forall x y,
erel r x y -> eqclass r x == eqclass r y.
Proof.
move=>r x y rxy;
rewrite /eqclass /= -val_eqE /=;
by apply: canonical_congr1.
Qed.
Lemma eq_eqclass(r:eqrelType): forall x y,
eqclass r x == eqclass r y -> erel r x y.
Proof.
move=>r x y exy.
rewrite /eqclass /= -val_eqE /= in exy.
by apply: canonical_inj1.
Qed.
Lemma eqclass_pickeqc(r:eqrelType):
forall x, eqclass r (pickeqc x) == x.
Proof.
move=>r [x xm].
rewrite -val_eqE.
rewrite /eqclass /pickeqc /=.
case: (image_exists xm)=>[y ->].
apply: canonical_congr1; apply: erel_sym; apply: canonical_elem.
Qed.
Lemma pickeqc_eqclass(r:eqrelType): forall x,
erel r (pickeqc (eqclass r x)) x.
Proof.
move=>r x.
rewrite /eqclass /pickeqc /=.
apply: erel_sym. apply: canonical_elem.
Qed.
End EqRel.
Opaque ieqrel_of_eqrel eqrel_of_ieqrel pickeqc.
Section Tools.
Variable d: finType.
The equality relation on
d
Definition equals_ieqrel: (ieqrel d).
apply: ieqrel_of_eqrel.
apply: (Eqrel (erel:=fun x y => x == y)).
by move=>x; rewrite eq_refl.
by move=>x y; rewrite (eq_sym x y).
by move=>x y z H K; rewrite (eqP H) (eqP K) eq_refl.
Defined.
End Tools.
General Results for Analysing the Cardinality of Quotients
Section CardQuotientTools.
Variables d1 d2: finType.
Variable r:eqrelType d1.
Definition quotient_map: (d1 -> d2) -> (quotient r) -> d2.
by move=>f [x E]; exact (f x). Defined.
Lemma quotient_map_injective: forall f,
(forall x y, (f x) = (f y) -> (erel r x y) )
-> (injective (quotient_map f)).
Proof.
move=> f I [x xH] [y yH] K.
have E:x=y.
elim: (image_exists xH) => [x1 x1H]//=.
elim: (image_exists yH) => [y1 y1H]//=.
rewrite x1H y1H.
have R:erel r x y by apply I.
have Rx1: erel r x1 x by rewrite x1H; apply canonical_elem.
have Ry1: erel r y1 y by rewrite y1H; apply canonical_elem.
have Rxy: erel r x1 y1 by apply (erel_trans Rx1 (erel_trans R (erel_sym Ry1))).
by apply (eqP (canonical_congr1 Rxy)).
by clear K; move:xH yH; rewrite E => [xH yH]; apply/val_eqP.
Qed.
Lemma card_quotient: forall f:d1->d2,
(forall x y, (f x) = (f y) -> (erel r x y) )
-> card (quotient r) <= card d2.
move=>f H.
have U: (injective (quotient_map f)) by apply: quotient_map_injective.
by apply (injective_card U).
Qed.
End CardQuotientTools.
Section CardQuotient.
Variables d: finType.
Variable r:eqrelType d.
Lemma card_quotient_equals: card (quotient (equals_ieqrel d)) = card d.
Proof.
set f: d -> quotient (equals_ieqrel d) := fun x => eqclass _ x.
have H: injective f.
move=>x y H.
have K: erel (equals_ieqrel d) x y.
by apply: eq_eqclass; rewrite /f in H; rewrite H eq_refl.
rewrite /equals_ieqrel eqrel_ieqrel /= in K.
by apply: (eqP K).
have K: forall y, exists x, f x == y.
by move=>y; exists (pickeqc y); rewrite /f eqclass_pickeqc.
rewrite -(@card_image _ _ f)=>//.
apply: eq_card=>x.
elim: (K x)=>[y y_mem]; rewrite -(eqP y_mem).
by rewrite image_f.
Qed.
Lemma card_quotient_lower: 0 < card d -> 0 < card (quotient r).
Proof.
move=>H.
case: (pickP d)=>[x _ | z].
by rewrite (cardD1 (eqclass r x)) add1n.
by rewrite (eq_card0 z) in H.
Qed.
Lemma card_quotient_upper: card (quotient r) <= card d .
Proof.
apply: (card_quotient (f:=fun x=>x));
move=>x y [->]; apply (erel_refl r).
Qed.
Variable s:eqrelType d.
Lemma card_quotient_leq: (forall x y, erel s x y -> erel r x y) ->
card (quotient r) <= card (quotient s).
Proof.
by move=>H; apply: (card_quotient (f:=eqclass s)) => x y; move/eqP=>E;
apply: (H x y (eq_eqclass E)).
Qed.
End CardQuotient.
Section EqrelCard.
Variable d:finType.
We define a few operations for modifying equivalence relations and analyse
their effect on the cardinality of the quotient.
Make equivalence relation from
r, in which x is only related to
itself:
Definition separate (r: ieqrel d) (x:d) : ieqrel d.
move=>r x.
apply: ieqrel_of_eqrel.
apply: (Eqrel (erel:=fun u v =>
match (u == x, v == x) with
| (false, false) => erel r u v
| (true, true) => true
| _ => false
end)).
by move=>u; case: (u == x)=>//; apply: erel_refl.
by move=>u v; case (u == x); case (v == x)=>//; try apply erel_sym.
by move=>u v w; case (u == x); case (v == x)=>//; case (w == x)=>//;
try apply erel_trans.
Defined.
Lemma erel_separate(r: ieqrel d): forall x u v,
erel (separate r x) u v = match (u == x, v == x) with
| (false, false) => erel r u v
| (true, true) => true
| _ => false
end.
Proof. by move=>r x u v; rewrite /separate eqrel_ieqrel /=. Qed.
Lemma separate_singleton: forall (r:ieqrel d) z,
(forall x, erel r z x -> z == x) ->
r == separate r z.
Proof.
move=>r z H.
apply: eqrel_of_ieqrel_inj=>x y.
rewrite erel_separate.
case U: (x == z); case V: (y == z).
by rewrite (eqP U) (eqP V) erel_refl.
by rewrite (eqP U); case W:(erel r z y)=>//; rewrite (eq_sym y z) (H y) in V=>//.
by rewrite (eqP V); case W:(erel r x z)=>//; rewrite (eq_sym x z) (H x) in U=>//;
apply erel_sym.
by done.
Qed.
Lemma card_quotient_separate: forall (r:ieqrel d) z,
card (quotient r) <= card (quotient (separate r z)).
Proof.
move=>r z.
set f: d -> quotient (separate r z) := fun x => eqclass (separate r z) x.
have H: forall x y, (erel (separate r z) x y) -> (erel r x y).
move=>x y.
rewrite erel_separate.
case xz: (x == z); case yz: (y == z)=>//.
by rewrite (eqP xz) (eqP yz); move=>_; apply erel_refl.
apply (card_quotient (r:=r) (f:=f)).
rewrite /f; move=>u v E.
by apply H; apply eq_eqclass; apply/eqP.
Qed.
Lemma card_separate_quotient: forall (r:ieqrel d) z,
card (quotient (separate r z)) <= (card (quotient r)).+1 .
Proof.
move=>r z.
set f: d -> optionFin (quotient r) :=
fun x => if x == z then None else Some (eqclass r x).
have H: forall x y,
negb (x == z) -> negb (y == z) -> (erel r x y) -> (erel (separate r z) x y).
move=>x y xiz yiz rxy.
rewrite /separate eqrel_ieqrel/=.
case xz: (x == z); case yz: (y == z)=>//.
by rewrite xz in xiz.
by rewrite yz in yiz.
rewrite -card_option.
apply (card_quotient (r:=separate r z) (f:=f)).
rewrite /f.
move=>x y.
case U:(x == z); case V:(y == z)=>//.
by rewrite (eqP U) (eqP V); move=>_; apply erel_refl.
by case=>K; apply H; rewrite ?U ?V=>//; apply: canonical_inj1; rewrite K eq_refl.
Qed.
Definition is_singleton_class(r:ieqrel d) (x:d) : Prop :=
forall y, erel r x y -> x = y.
Lemma card_separate_quotient_eq: forall (r:ieqrel d) z z',
(negb (z == z')) -> (erel r z z') ->
card (quotient (separate r z)) = S (card (quotient r)).
Proof.
move=>r z.
set f: (quotient (separate r z)) -> optionFin (quotient r) :=
(fun c=>
if (pickeqc c) == z then None else Some (eqclass r (pickeqc c))).
have H: injective f.
move=>x y.
rewrite /f.
case U: (pickeqc x == z); case V: (pickeqc y == z)=>//.
by move=>_; apply/eqP; apply pickeqc_eqd;
rewrite (eqP U) (eqP V) erel_refl.
move=>H.
apply/eqP; apply pickeqc_eqd; rewrite erel_separate.
case: ifP=>[c1|c2];
case: ifP=>[d1|d2]=>//.
by rewrite U in c1.
by rewrite V in d1.
apply: canonical_inj1. case: H=>K. apply/eqP. auto.
move=>z' nzz' rzz'.
rewrite -card_option -(@card_image _ _ f)=>//.
apply: eq_card.
move=>c.
have F: (exists x, f x == c).
rewrite /f.
have K: pickeqc (eqclass (separate r z) z) == z.
have K': erel (separate r z) (pickeqc (eqclass (separate r z) z)) z
by apply: pickeqc_eqclass.
rewrite erel_separate eq_refl in K'.
by case: (_ == z) K'.
case: c =>[c'|].
exists (eqclass (separate r z)
(if (erel r z (pickeqc c')) then z' else (pickeqc c'))).
case U: (erel r z (pickeqc c')).
case V: (_ == z).
have W: erel (separate r z) z z'.
apply: (erel_trans (y:=pickeqc (eqclass (separate r z) z'))).
by rewrite (eqP V) erel_refl.
by apply pickeqc_eqclass.
by rewrite erel_separate eq_refl (eq_sym z' z) (negbET nzz') in W.
have W: eqclass r (pickeqc (eqclass (separate r z) z')) == c'.
rewrite -(eqP (eqclass_pickeqc c')).
apply: eqclass_eq.
have L: erel (separate r z) (pickeqc (eqclass (separate r z) z')) z'
by apply: pickeqc_eqclass.
rewrite erel_separate (eq_sym z' z) (negbET nzz') in L.
case: (_ == z) in L=>//.
apply: (erel_trans (erel_trans L (erel_sym rzz')) U).
by rewrite -(eqP W) eq_refl.
case V: (_ == z).
have W: erel (separate r z) (pickeqc c') z.
by apply: eq_eqclass; apply: pickeqc_eqd;
rewrite (eqP V) (eqP K) erel_refl.
by rewrite erel_separate eq_refl in W;
case Y: (_== z) W=>//; rewrite (eqP Y) erel_refl in U.
have W: erel (separate r z)
(pickeqc (eqclass (separate r z) (pickeqc c')))
(pickeqc c')
by apply: pickeqc_eqclass.
rewrite erel_separate V in W; case Y: (_ == z) W=>//W.
have W': eqclass r (pickeqc (eqclass (separate r z) (pickeqc c'))) == c'.
by rewrite -{2}(eqP (eqclass_pickeqc c')); apply: eqclass_eq.
by rewrite (eqP W') eq_refl.
exists (eqclass (separate r z) z).
by case U:(_ == z)=>//; rewrite K in U.
elim:F =>[x E].
by rewrite -(eqP E) image_f.
Qed.
Join equivalence classes of
x and y
Definition join(r: ieqrel d) (x y:d) : ieqrel d.
move=>r x y.
apply: ieqrel_of_eqrel.
apply (Eqrel (erel:=fun u v => (erel r u v) || ((erel r u x && erel r y v)
|| (erel r u y && erel r x v)))).
move=>u.
by rewrite erel_refl orTb.
move=>u v.
move/or3P=>[H1|H2|H3].
by rewrite erel_sym.
by move/andP: H2=>[H21 H22]; rewrite (@erel_sym _ r u x)=>//;
rewrite (@erel_sym _ r y v)=>//; rewrite andbT !orbT.
by move/andP: H3=>[H31 H32]; rewrite (@erel_sym _ r u y)=>//;
rewrite (@erel_sym _ r x v)=>//; rewrite andbT !orbT.
move=>u v w.
move/or3P=>[H1|H2|H3].
move/or3P=>[K1|K2|K3].
by rewrite (@erel_trans _ r u v w).
by move/andP: K2=>[K21 K22]; rewrite (@erel_trans _ r u v x)=>//; rewrite K22 andTb!orbT.
by move/andP: K3=>[K31 K32]; rewrite (@erel_trans _ r u v y)=>//; rewrite K32 andTb!orbT.
move/or3P=>[K1|K2|K3].
by move/andP: H2=>[H21 H22]; rewrite (@erel_trans _ r y v w)=>//; rewrite H21 andTb!orbT.
by move/andP: H2=>[H21 H22]; move/andP: K2=>[K21 K22]; rewrite H21 K22 andTb!orbT.
by move/andP: H2=>[H21 H22]; move/andP: K3=>[K31 K32]; rewrite (@erel_trans _ r u x w)=>//; rewrite andTb!orTb.
move/or3P=>[K1|K2|K3].
by move/andP: H3=>[H31 H32]; rewrite (@erel_trans _ r x v w)=>//; rewrite H31 andTb!orbT.
by move/andP: H3=>[H31 H32]; move/andP: K2=>[K21 K22]; rewrite (@erel_trans _ r u y w)=>//; rewrite orTb.
by move/andP: H3=>[H31 H32]; move/andP: K3=>[K31 K32]; rewrite H31 K32 andTb!orbT.
Defined.
Lemma erel_join(r: ieqrel d): forall x y u v,
(erel (join r x y) u v) = (erel r u v) || ((erel r u x && erel r y v)
|| (erel r u y && erel r x v)).
Proof. by move=>r x y u v; rewrite /join eqrel_ieqrel /=. Qed.
Lemma card_quotient_join_leq: forall (r:ieqrel d) u v,
card (quotient (join r u v)) <= card (quotient r).
Proof.
move=>r u v; apply (card_quotient (r:=join r u v) (f:=eqclass r)).
by move=>x y E; rewrite /join eqrel_ieqrel /= eq_eqclass ?orTb ?E ?eqd_refl.
Qed.
Lemma card_quotient_join_lt: forall (r:ieqrel d) u v,
negb (erel r u v) ->
(card (quotient (join r u v))).+1 = card (quotient r).
Proof.
move=>r u v E.
set f: optionFin (quotient (join r u v)) -> (quotient r) :=
(fun x=>
match x with
| Some c => if erel r (pickeqc c) v
then (eqclass r u) else (eqclass r (pickeqc c))
| None => eqclass r v
end).
have H: injective f.
case=>c1.
case=>c2.
rewrite /f.
case V1:(erel r (pickeqc c1) v).
case V2:(erel r (pickeqc c2) v).
move=>_.
have H: c1 == c2.
apply pickeqc_eqd.
apply: (@erel_trans _ _ _ v _).
by rewrite erel_join V1 orTb.
by rewrite erel_join (erel_sym V2) orTb.
by rewrite (eqP H).
move=>F.
have H: c1 == c2.
by apply pickeqc_eqd;
rewrite erel_join V1 (eq_eqclass (x:=u)) ?andTb ?orbT ?F ?eqd_refl.
by rewrite (eqP H).
case V2:(erel r (pickeqc c2) v).
move=>F.
have H: c1 == c2.
by apply pickeqc_eqd;
rewrite erel_join (erel_sym V2) (eq_eqclass (y:=u))
?andTb ?orbT ?F ?eqd_refl.
by rewrite (eqP H).
move=>F.
have H: c1 == c2.
by apply pickeqc_eqd; rewrite erel_join eq_eqclass ?orTb ?F ?eqd_refl.
by rewrite (eqP H).
rewrite /f in c2.
move:c2; case U: (erel r (pickeqc c1) v); move=>c2.
have H: (erel r u v) by apply: eq_eqclass; apply/eqP.
by rewrite (negbET E) in H.
have H: (erel r (pickeqc c1) v) by apply: eq_eqclass; apply/eqP.
by rewrite U in H.
case c1=>//.
move=>c2. rewrite /f.
case U: (erel r (pickeqc c2) v); move=>F.
have H: (erel r u v) by apply: eq_eqclass; apply/eqP.
by rewrite (negbET E) in H.
have H: (erel r (pickeqc c2) v) by apply: eq_eqclass; apply/eqP.
by rewrite U in H.
rewrite -card_option -(@card_image _ _ f)=>//.
apply: eq_card.
move=>c.
have F: (exists x, f x == c).
rewrite /f.
case V: (erel r (pickeqc c) v).
exists (None: optionFin (quotient (join r u v))).
by rewrite -(eqP (eqclass_pickeqc c)); apply eqclass_eq; apply erel_sym.
exists (Some (eqclass (join r u v) (pickeqc c))).
have K: erel (join r u v)
(pickeqc (eqclass (join r u v) (pickeqc c)))
(pickeqc c)
by apply: pickeqc_eqclass.
rewrite erel_join in K.
case/or3P: K=>[K1|K2|K3].
case L: (erel r (pickeqc (eqclass (join r u v) (pickeqc c))) v) .
by rewrite (erel_trans (erel_sym K1) L) in V.
by rewrite -(eqP (eqclass_pickeqc c)); apply: eqclass_eq;
rewrite (eqP (eqclass_pickeqc c)).
by case/andP: K2=>[K21 K22]; rewrite (erel_sym K22) in V.
case/andP: K3=>[K31 K32].
by rewrite K31 -(eqP (eqclass_pickeqc c)); apply: eqclass_eq.
elim: F=>[x e].
rewrite -(eqP e) image_f=>//.
Qed.
End EqrelCard.