From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import div ssralg ssrint ssrnum binomial.
Require Import tools combclass sorted ordtype partition.

Set Implicit Arguments.

Import LeqGeqOrder.
Import Order.TTheory.

Lemma pblock_in (T : finType) (P : {set {set T}}) (x : T) :
  set0 \notin P -> (pblock P x \in P) = (x \in cover P).

Lemma mem_pblockC (T : finType) (P : {set {set T}}) :
  trivIset P -> forall x y : T, (x \in pblock P y) = (y \in pblock P x).

Lemma equivalence_partitionE (T : finType) (R S : rel T) (D : {set T}) :
  R =2 S -> equivalence_partition R D = equivalence_partition S D.

Section Defs.

Variable T : finType.
Variable S : {set T}.

Structure setpart : predArgType :=
  SetPart {setpartval :> {set {set T}}; _ : partition setpartval S}.

Implicit Type (P Q : setpart) (A B : {set T}).

Lemma setpartP P : partition P S.

Lemma trivIsetpart P : trivIset P.

Lemma cover_setpart P : cover P = S.

Lemma setpart_non0 P : set0 \notin P.

Hint Resolve setpartP trivIsetpart setpart_non0 : core.

Lemma setpart_subset P A : A \in P -> A \subset S.

Lemma setpart_eq P x A B :
  A \in P -> B \in P -> x \in A -> x \in B -> A = B.

Lemma mem_eq_pblock P A : A \in P -> forall x, x \in A -> pblock P x = A.

Lemma mem_setpart_pblock P A : A \in P -> exists x, x \in A.

Lemma mem_pblock_setpart P x y : x \in pblock P y -> x \in S.

Lemma pblock_notin P x : (pblock P x != set0) = (x \in S).

Fact setpart1_subproof : partition [set [set x] | x in S] S.
Canonical setpart1 := SetPart setpart1_subproof.

Lemma pblock_setpart1 x : x \in S -> pblock setpart1 x = [set x].

Fact trivsetpart_subproof :
  partition (T := T) (if S == set0 then set0 else [set S]) S.
Canonical trivsetpart := SetPart trivsetpart_subproof.

Lemma pblock_trivsetpart x : x \in S -> pblock trivsetpart x = S.

End Defs.
Hint Resolve setpartP trivIsetpart setpart_non0 : core.

Section Empty.

Variable T : finType.

Fact part_ordinal0 : partition (T := T) set0 set0.
Definition setpart_set0 := SetPart part_ordinal0.

Lemma setpart_set0_eq_set0 (p : setpart set0) : p = setpart_set0.

Lemma enum_setpart_set0 : enum (setpart (@set0 T)) = [:: setpart_set0 ].

End Empty.

Section Singleton.

Variable T : finType.
Variable x : T.

Implicit Type (A B : {set T}).

Fact part_ordinal1 : partition [set [set x]] [set x].
Definition setpart_set1 := SetPart part_ordinal1.

Lemma subset_set1 A :
  A \subset [set x] -> (A = set0) \/ (A = [set x]).

Lemma part_set1_eq (P : {set {set T}}) :
  partition P [set x] -> P = [set [set x]].

Lemma setpart_set1_eq_set1 (p : setpart [set x]) : p = setpart_set1.

Lemma enum_setpart_set1 : enum (setpart [set x]) = [:: setpart_set1].

End Singleton.

Module RefinmentOrder.
Section RefinmentOrder.

Import LeqGeqOrder.

Context {T : finType} (S : {set T}).

Implicit Type (P Q R : setpart S) (A B X Y : {set T}).

Definition is_finer P Q :=
  [forall (x | x \in S), pblock P x \subset pblock Q x].

Lemma is_finer_pblockP P Q :
  reflect (forall x, x \in S -> pblock P x \subset pblock Q x) (is_finer P Q).

Lemma is_finer_refl : reflexive is_finer.

Lemma is_finer_trans : transitive is_finer.

Fact is_finer_setpart_anti : antisymmetric is_finer.
Lemma setpartfiner_display : unit.
#[export]
HB.instance Definition _ :=
  Order.Le_isPOrder.Build setpartfiner_display (setpart S)
    is_finer_refl is_finer_setpart_anti is_finer_trans.

Lemma is_finerP P Q :
  reflect
    (forall A, A \in P -> exists2 B : {set T}, B \in Q & A \subset B)
    (P <= Q)%O.

Fact setpart1_bottom P : (setpart1 S <= P)%O.
Fact trivsetpart_top P : (P <= trivsetpart S)%O.
#[export]
HB.instance Definition _ :=
  Order.hasBottom.Build setpartfiner_display (setpart S) setpart1_bottom.
#[export]
HB.instance Definition _ :=
  Order.hasTop.Build setpartfiner_display (setpart S) trivsetpart_top.

Fact meet_finer_subproof P Q :
  partition [set A :&: B | A in P, B in Q & A :&: B != set0] S.
Definition meet_finer P Q := SetPart (meet_finer_subproof P Q).

Variant meet_spec P Q X : Prop :=
  MeetSpec A B of A \in P & B \in Q & A :&: B != set0 & X = A :&: B.
Lemma mem_meet_finerP P Q X :
  reflect (meet_spec P Q X) (X \in meet_finer P Q).

Lemma meet_finerC : commutative meet_finer.

Lemma le_meet_finer P Q : (meet_finer P Q <= P)%O.

Fact meet_finerP R P Q : (R <= meet_finer P Q)%O = (R <= P)%O && (R <= Q)%O.

Lemma setpart_conn P : connect_sym (fun x y : T => y \in (pblock P x)).

Definition join_finer_eq P Q :=
  connect (relU (fun x y => y \in pblock P x) (fun x y => y \in pblock Q x)).

Lemma join_finer_equivalence P Q :
  {in S & &, equivalence_rel (join_finer_eq P Q)}.

Definition join_finer P Q :=
  SetPart (equivalence_partitionP (join_finer_equivalence P Q)).

Lemma join_finerC : commutative join_finer.

Lemma le_join_finer P Q : (P <= join_finer P Q)%O.

Fact join_finerP P Q R : (join_finer P Q <= R)%O = (P <= R)%O && (Q <= R)%O.
#[export]
HB.instance Definition _ :=
  Order.POrder_MeetJoin_isLattice.Build setpartfiner_display (setpart S)
    meet_finerP join_finerP.

End RefinmentOrder.

Module Exports.

Section Finer.

Context {T : finType} (S : {set T}).
Implicit Type (P Q R : setpart S) (A B X Y : {set T}).

Definition is_finerP P := is_finerP P.
Definition is_finer_pblockP P Q :
  reflect (forall x, x \in S -> pblock P x \subset pblock Q x) (P <= Q)%O
  := is_finer_pblockP P Q.

Lemma is_finer_subpartP P Q :
  reflect
    (exists2 subpart : {set T} -> {set {set T}},
        forall B, B \in Q -> partition (subpart B) B
        & \bigcup_(B in Q) subpart B = P)
    (P <= Q)%O.

Lemma setpart_bottomE : 0%O = setpart1 S.
Lemma setpart_topE : 1%O = trivsetpart S.

Definition mem_meet_finerP P Q X : reflect (meet_spec P Q X) (X \in P `&` Q)%O
  := mem_meet_finerP P Q X.

Lemma join_finer_eq_in_S P Q x y :
  x \in S -> join_finer_eq P Q x y -> y \in S.

Lemma join_finerE P Q x y :
  x \in S -> y \in pblock (P `|` Q)%O x = join_finer_eq P Q x y.

End Finer.

Notation join_finer_eq := join_finer_eq.

End Exports.
End RefinmentOrder.

Section FinerCard.

Context {T : finType} (S : {set T})
  (P Q : setpart S) (finPQ : (P <= Q)%O).

Implicit Types (A B : {set T}).

Definition map_finer A : {set T} :=
    if (boolP (A \in P)) is AltTrue pin then
      let: exist2 B _ _ := sig2W (is_finerP P Q finPQ A pin) in B
    else set0.

Lemma map_finer_subset A : A \in P -> A \subset map_finer A.

Lemma map_finer_in A : A \in P -> map_finer A \in Q.

Lemma map_finer_pblock x : map_finer (pblock P x) = pblock Q x.

Lemma image_map_finer : [set map_finer x | x in P] = Q.

Lemma is_finer_card : #|Q| <= #|P| ?= iff (P == Q).

End FinerCard.