Require Import ssreflect ssrbool eqtype ssrnat ssrfun.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Require Export sset4.


Import Correspondence.
Import Bfunction.
Module Border.

Definition antisymmetric_r (r:Set -> Set -> Prop) :=
  forall x y, r x y -> r y x -> x = y.

Definition is_antisymmetric (r:Set) :=
 is_graph r & forall x y, related r x y -> related r y x -> x = y.

Definition reflexive_rr (r:Set -> Set -> Prop) :=
  forall x y, r x y -> (r x x & r y y).

Definition order_r (r:Set -> Set -> Prop) :=
  transitive_r r & antisymmetric_r r & reflexive_rr r.

Definition preorder_r (r:Set -> Set -> Prop) :=
  transitive_r r & reflexive_rr r.

Lemma equality_is_order: order_r(fun x y => x = y).
Proof.
split.
  by hnf; intuition; ue.
split;hnf; intuition.
Qed.

Lemma sub_is_order: order_r sub.
Proof.
split; first by move=> x y t xy yz; apply (sub_trans xy yz).
split; first by move=> x y xy yx; apply extensionality.
move=> x y; split; apply sub_refl.
Qed.

Definition opposite_relation (r:Set -> Set -> Prop) := fun x y => r y x.

Lemma opposite_is_preorder_r: forall r,
  preorder_r r -> preorder_r (opposite_relation r).
Proof.
rewrite /preorder_r/opposite_relation => r [tr rr].
split.
  by move=> x y z xy yz; apply (tr _ _ _ yz xy).
by move=> x y yx /=; move: (rr _ _ yx); intuition.
Qed.

Lemma opposite_is_order_r: forall r,
  order_r r -> order_r (opposite_relation r).
Proof.
move=> r [tr [ar rr]].
have pr: preorder_r r by hnf.
move: (opposite_is_preorder_r pr)=> [tr' rr'].
hnf; ee; rewrite/opposite_relation => x y xy yx.
by apply: (ar _ _ yx).
Qed.

Definition order_re (r:Set -> Set -> Prop) x :=
  order_r r & reflexive_r r x.

Definition order (r:Set) :=
  is_reflexive r & is_transitive r & is_antisymmetric r.

Lemma order_is_graph: forall r, order r -> is_graph r.
Proof. by move => r [[g _] _]. Qed.

Hint Resolve order_is_graph : fprops.

Definition opposite_order := inverse_graph.

Definition preorder (r: Set) :=
  is_reflexive r & is_transitive r.

Lemma preorder_graph : forall r, preorder r -> is_graph r.
Proof. by move => r [[g _] _]. Qed.

Lemma order_preorder : forall r, order r -> preorder r.
Proof. by move => r [tr [ar rr]]; hnf. Qed.

Lemma order_has_graph0: forall r x,
  order_re r x -> is_graph_of (graph_on r x) r.
Proof.
move=> r x [ [_ [_ rrr]] rr].
move => u v ; rewrite /related/graph_on.
apply iff_eq ; rewrite Z_rw; aw; last by intuition.
move=> ruv; split=>//; split; fprops.
move: (rrr _ _ ruv) => [ruu rvv].
by rewrite 2! rr.
Qed.

Lemma graph_on_rw3: forall r x u v,
  order_re r x ->
  related (graph_on r x) u v = r u v.
Proof. move=> r x u v hyp; symmetry; apply (order_has_graph0 hyp).
Qed.

Lemma order_has_graph: forall r x,
  order_re r x -> exists g, is_graph_of g r.
Proof.
move=> r x hyp; exists (graph_on r x).
by apply order_has_graph0.
Qed.

Lemma order_if_has_graph: forall r g,
  is_graph g -> is_graph_of g r ->
  order_r r -> order_re r (domain g).
Proof.
move=> r g gg gor or; split=>//.
move : gor; rewrite /is_graph_of/related => gor.
move => x; apply iff_eq; dw.
  move => [y]; rewrite -gor=> rxy.
  by move: or=> [_ [_ rr]]; move: (rr _ _ rxy); case.
by move=> h; exists x;rewrite - gor.
Qed.

Lemma order_if_has_graph2: forall r g,
  is_graph g -> is_graph_of g r ->
  order_r r -> order g.
Proof.
move=> r g gg gor or.
move: gor; rewrite /is_graph_of/related => gor.
move: or => [tr [ar rer]].
split.
  split=>//.
  move=> y; rewrite inc_substrate_rw /related // -gor.
  by case; move=> [z]; rewrite - gor => aux; move: (rer _ _ aux); intuition.
split; split=>//.
  move=> x y z; rewrite /related -3! gor; apply tr.
move=> x y; rewrite /related -2! gor; apply ar.
Qed.

Lemma order_has_graph2: forall r x,
  order_re r x -> exists g,
    g = graph_on r x &
    order g & (forall u v, r u v = related g u v).
Proof.
move=> r x or; exists (graph_on r x).
have gg: is_graph (graph_on r x) by apply graph_on_graph.
have gor: is_graph_of (graph_on r x) r by apply order_has_graph0.
move: or => [or1 or2].
ee; apply (order_if_has_graph2 gg gor or1).
Qed.

Lemma preorder_from_rel: forall r x,
  preorder_r r -> preorder (graph_on r x).
Proof.
move=> r x pr.
have gg: (is_graph (graph_on r x)) by apply graph_on_graph.
move: pr=> [tr rr].
split; split=>//.
  move=> y; rewrite inc_substrate_rw // /related.
  case; move=> [z]; rewrite 2! graph_on_rw0;
     move=> [yx [zx ryz]];move: (rr _ _ ryz); intuition.
move=> a b c; rewrite 3! graph_on_rw1.
move=> [ax [bx rab]] [_ [cx rbc]]; intuition; apply (tr _ _ _ rab rbc).
Qed.

Lemma order_from_rel: forall r x,
  order_r r -> order (graph_on r x).
Proof.
move=> r x or.
have po: preorder (graph_on r x) .
  by apply preorder_from_rel; red in or; hnf; intuition.
move: po => [tr rr].
hnf; intuition.
split; first by move: tr => [g _].
move=> a b; rewrite 2! graph_on_rw1.
move=> [ax [bx rab]] [_ [_ rba]].
by move: or=> [_ [ta _]]; apply ta.
Qed.

Lemma order_reflexivity_pr: forall r x u v,
  order_re r x -> r u v -> (inc u x & inc v x).
Proof.
move=> r x u v [ [_ [_ rrr]] rr] ruv.
by rewrite 2!rr; apply rrr.
Qed.

Lemma order_symmetricity_pr: forall r x u v,
  order_re r x -> (r u v & r v u) = (inc u x & inc v x & u = v).
Proof.
move=> r x u v or.
apply iff_eq.
  move=> [ruv rvu].
  move: (order_reflexivity_pr or ruv)=> [ux vx].
  by intuition; move: or => [[ _ [asy _]] _]; apply asy.
move=> [ux [vx]] ->.
by move: or=> [_ rr]; rewrite rr in vx.
Qed.

Lemma order_reflexivity: forall r a,
  order r -> inc a (substrate r) = related r a a.
Proof.
move=> r a [[_ or] _].
apply iff_eq => h; first by apply or.
substr_tac.
Qed.

Lemma order_antisymmetry: forall r a b,
  order r -> related r a b -> related r b a -> a = b.
Proof.
move=> r a b [ _ [_ [_]]]; apply.
Qed.

Lemma order_transitivity: forall r a b c,
  order r -> related r a b -> related r b c -> related r a c.
Proof.
by move=> r a b c [ _ [[ _ t] _]]; apply t.
Qed.

Lemma inter_rel_order : forall z,
  nonempty z -> (forall r, inc r z -> order r) ->
  order (intersection z).
Proof.
move=> z nez alo.
have ri: (is_reflexive (intersection z)) .
  apply inter_rel_reflexive=> //.
  by move=> r rz; move: (alo _ rz) => [re _].
split =>//.
split.
  apply inter_rel_transitive=> //.
  by move=> r rz; move: (alo _ rz) => [_ [tr _]].
split; first by move: ri => [g _].
move=> x y xi yi; move: nez => [t tz].
move: (intersection_forall xi tz)(intersection_forall yi tz).
by move: (alo _ tz)=> [ _ [ _ [_ ra] ]]; apply ra.
Qed.

Definition gle (r x y:Set) := related r x y.
Definition gge (r x y:Set) := gle r y x.
Definition glt (r x y:Set) := gle r x y & x <> y.
Definition ggt (r x y:Set) := gge r x y & x <> y.

Lemma lt_leq_trans : forall r x y z,
  order r -> glt r x y -> gle r y z -> glt r x z.
Proof.
move=> r x y z or [le1 nxy] le2; split.
  by apply order_transitivity with y.
dneg xz.
rewrite -xz in le2.
apply (order_antisymmetry or le1 le2).
Qed.

Lemma leq_lt_trans : forall r x y z,
  order r -> gle r x y -> glt r y z -> glt r x z.
Proof.
move=> r x y z or le1 [le2 nxy]; split.
  by apply order_transitivity with y.
dneg xz.
rewrite xz in le1.
apply (order_antisymmetry or le2 le1).
Qed.

Lemma lt_lt_trans: forall r a b c, order r ->
  glt r a b -> glt r b c -> glt r a c.
Proof. move=> r x y z or [le1 nxy] le2. apply (leq_lt_trans or le1 le2).
Qed.

Lemma not_le_gt: forall r x y, order r -> gle r x y -> glt r y x -> False.
Proof.
move=> r x y or le1 le2.
move: (leq_lt_trans or le1 le2) => [_ xx].
by elim xx.
Qed.

Ltac order_tac:=
  match goal with
    | H1: gle ?r ?x _ |- inc ?x (substrate ?r)
      => exact (inc_arg1_substrate H1)
    | H1: glt ?r ?x _ |- inc ?x (substrate ?r)
      => move: H1 => [H1 _] ; order_tac
    | H1:gle ?r _ ?x |- inc ?x (substrate ?r)
      => exact (inc_arg2_substrate H1)
    | H1:glt ?r _ ?x |- inc ?x (substrate ?r)
      => move: H1 => [H1 _]; order_tac
    | H: order ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u
      => rewrite - order_reflexivity //
    | H: order ?r |- inc (J ?u ?u) ?r
       => change (related r u u); rewrite - order_reflexivity //
    | H: order ?r |- gle ?r ?u ?u
       => rewrite /gle -order_reflexivity //
    | H1: gle ?r ?x ?y, H2: gle ?r ?y ?x, H:order ?r |-
        ?x = ?y => exact (order_antisymmetry H H1 H2)
    | H:order ?r, H1:related ?r ?x ?y, H2: related ?r ?y ?x |- ?x = ?y
      => apply (order_antisymmetry H H1 H2)
    | H:order ?r, H1: inc (J ?x ?y) ?r , H2: inc (J ?y ?x) ?r |- ?x = ?y
      => apply (order_antisymmetry H H1 H2)
    | H:order ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w
      |- related ?r ?u ?w
      => apply (order_transitivity H H1 H2)
    | H:order ?r, H1:gle ?r ?u ?v, H2: gle ?r ?v ?w
      |- gle ?r ?u ?w
      => apply (order_transitivity H H1 H2)
    | H: order ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |-
      inc (J ?u ?w) ?r
      => change (related r u w); apply (order_transitivity H H1 H2)
    | H1: gle ?r ?x ?y, H2: glt ?r ?y ?x, H: order ?r |- _
      => elim (not_le_gt H H1 H2)
    | H1:glt ?r ?x ?y, H2: glt ?r ?y ?x, H:order ?r |- _
      => destruct H1 as [H1 _] ; elim (not_le_gt H H1 H2)
    | H1:order ?r, H2:glt ?r ?x ?y, H3: gle ?r ?y ?z |- glt ?r ?x ?z
       => exact (lt_leq_trans H1 H2 H3)
    | H1:order ?r, H2:gle ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
       => exact (leq_lt_trans H1 H2 H3)
    | H1:order ?r, H2:glt ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
       => exact (lt_lt_trans H1 H2 H3)
    | H1:order ?r, H2:gle ?r ?x ?y |- glt ?r ?x ?y
       => split =>//
    | H:glt ?r ?x ?y |- gle ?r ?x ?y
       => by move: H=> []
end.

Lemma le_antisym: forall r a b,
  order r -> gle r a b -> gle r b a -> a = b.
Proof.
move=> r a b [ _ [_ [_]]]; apply.
Qed.

Lemma order_is_order: forall r,
  order r -> order_r (related r).
Proof.
move => r [[g rr] [[_ t] [_ s]]].
hnf; ee; move=> x y xy.
by move: (rr _ (inc_arg1_substrate xy)) (rr _ (inc_arg2_substrate xy)).
Qed.

Lemma substrate_opposite_order: forall r,
  order r -> substrate (opposite_order r) = substrate r.
Proof.
move=> r or.
have gr: is_graph r by fprops.
have go: is_graph (opposite_order r) by fprops.
set_extens x; do 2 rewrite inc_substrate_rw //.
case; move=> [y]; aw => h; [ right | left ]; ex_tac.
case; move=> [y]; [ right | left ]; exists y; aw.
Qed.

Hint Rewrite substrate_opposite_order : aw.

Lemma substrate_domain_order: forall f,
  order f -> substrate f = domain f.
Proof.
move=> f or.
set_extens x => xs.
  have Jf: inc (J x x) f by order_tac.
  by rewrite /domain; aw; exists (J x x); aw; auto.
by rewrite /substrate; apply union2_first.
Qed.

Lemma opposite_is_order: forall r,
  order r -> order (opposite_order r).
Proof.
move=> r or;
set (g:= opposite_order r).
have gg: is_graph g by rewrite /g; fprops.
have go: is_graph_of g (opposite_relation (related r)).
  move=> x y.
  by rewrite/ opposite_relation/g/related ; aw.
have ori: order_r (opposite_relation (related r)).
  by apply opposite_is_order_r; apply order_is_order.
by apply (order_if_has_graph2 gg go ori).
Qed.

Hint Resolve opposite_is_order: fprops.

Lemma diagonal_order : forall x,
  order (identity_g x).
Proof.
move=> x.
move: (diagonal_equivalence x) => [ir [it _]].
hnf; intuition.
split; first by move: ir=> [h _].
move=> a b; rewrite /related;aw. intuition.
Qed.

Lemma order_from_rel1: forall r x,
  transitive_r r ->
  (forall u v, inc u x -> inc v x -> r u v -> r v u -> u = v) ->
  (forall u, inc u x -> r u u) ->
  order (graph_on r x).
Proof.
move=> r x tr sy re.
have go: (graph_on r x = graph_on (fun a b => inc a x & inc b x & r a b) x).
  rewrite /graph_on.
  set_extens w; rewrite Z_rw Z_rw; aw; intuition.
rewrite go; apply order_from_rel.
split.
  move => a b c [ax [bx rab]] [_ [cx rbc]]; intuition; apply(tr _ _ _ rab rbc).
split=>//.
  by move=> a b [ax [bx rab]] [_ [cx rbc]]; apply sy.
by move=> a b [ax [bx rab]]; intuition.
Qed.

Lemma substrate_graph_on: forall (r:Set -> Set -> Prop) x,
  (forall a, inc a x -> r a a) ->
  substrate (graph_on r x) = x.
Proof.
move=> r x rr.
apply extensionality; first by apply graph_on_substrate.
move => t xt; move: (rr _ xt) => rtt.
have aux: (related (graph_on r x) t t).
  by rewrite /graph_on /related Z_rw; aw; fprops.
substr_tac.
Qed.

Definition inclusion_suborder (b:Set) :=
  graph_on sub b.
Definition inclusion_order (a:Set) := inclusion_suborder (powerset a).

Lemma subinclusion_is_order: forall a,
  order (inclusion_suborder a).
Proof.
rewrite /inclusion_suborder => a.
apply order_from_rel; apply sub_is_order.
Qed.

Lemma inclusion_is_order: forall a,
  order (inclusion_order a).
Proof.
rewrite /inclusion_order => a. apply subinclusion_is_order.
Qed.

Lemma substrate_subinclusion_order:forall a,
  substrate (inclusion_suborder a) = a.
Proof.
rewrite /inclusion_suborder => a.
apply substrate_graph_on.
move=> x; fprops.
Qed.

Lemma substrate_inclusion_order: forall a,
  substrate (inclusion_order a) = powerset a.
Proof. rewrite /inclusion_order=> a. apply substrate_subinclusion_order.
Qed.

Lemma subinclusion_order_rw: forall a u v ,
  related (inclusion_suborder a) u v = (inc u a & inc v a & sub u v).
Proof. by move=> a u v; rewrite /inclusion_suborder graph_on_rw1.
Qed.

Lemma inclusion_order_rw: forall a u v,
  related (inclusion_order a) u v = (sub u a & sub v a & sub u v).
Proof. move => a u v; rewrite /inclusion_order subinclusion_order_rw; aw.
Qed.

Hint Rewrite substrate_inclusion_order : aw.
Hint Rewrite substrate_subinclusion_order : aw.
Hint Resolve inclusion_is_order subinclusion_is_order: fprops.
Hint Rewrite subinclusion_order_rw inclusion_order_rw: aw.

Definition extension_order x y :=
  graph_on extends (set_of_sub_functions x y).

Hint Rewrite set_of_sub_functions_rw : bw.

Lemma extends_in_prop: forall x y,
  order_r extends &
  (forall u, inc u (set_of_sub_functions x y) -> extends u u).
Proof.
move=> x y; rewrite /extends.
split; last by move=> u; bw; intuition.
split.
  move=> a b c [fb [fa [gba tba]]] [fc [_ [gcb tcb]]].
  intuition.
    by apply sub_trans with (graph b).
  by apply sub_trans with (target b).
split; last by red; intuition.
move=> a b [fb [fa [gba tba]]] [_ [_ [gab tab]]].
have grab: graph a = graph b by apply extensionality.
have tgab: target a = target b by apply extensionality.
by apply function_exten1.
Qed.

Lemma extension_is_order: forall x y,
  order (extension_order x y).
Proof.
rewrite /extension_order=> x y.
move: (extends_in_prop x y) => [p1 _].
by apply order_from_rel.
Qed.

Lemma substrate_extension_order: forall x y,
  substrate (extension_order x y) = (set_of_sub_functions x y).
Proof.
rewrite /extension_order => x y.
by move: (extends_in_prop x y)=> [_ p1]; apply substrate_graph_on.
Qed.

Lemma extension_order_rw : forall E F f g,
  gle (extension_order E F) g f =
  (inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
    & extends g f).
Proof.
by move=> E F f g; rewrite /gle/related /extension_order graph_on_rw0.
Qed.

Lemma extension_order_pr1 : forall E F f g,
  gle (extension_order E F) g f =
  (inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
    & sub (graph f) (graph g)).
Proof.
move=> E F f g; rewrite extension_order_rw /extends.
apply iff_eq; first by intuition.
move=> [p1 [p2 sh]]; split=>//; split=>//.
move: p1 p2; bw; move=> [fg [_ tg]] [ff [_ tf]]; rewrite tg tf.
fprops.
Qed.

Lemma extension_order_pr2 : forall E F f g,
  gle (opposite_order (extension_order E F)) g f =
  (inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
    & sub (graph g) (graph f)).
Proof.
move=> E F f g. rewrite /gle/related; aw.
rewrite -[inc (J f g) (extension_order E F)]/(gle (extension_order E F) f g).
rewrite extension_order_pr1.
by apply iff_eq; intuition.
Qed.

Hint Rewrite extension_order_rw: aw.
Hint Resolve extension_is_order: fprops.

Lemma extension_order_pr : forall E F f g x,
  gle (opposite_order (extension_order E F)) f g ->
  inc x (source f) -> W x f = W x g.
Proof.
move=> E F f g x; rewrite /opposite_order; bw; aw.
move => [gs [fs et]] xsf.
apply (W_extends et xsf).
Qed.

Hint Rewrite substrate_extension_order: aw.

Definition set_of_partition_set x :=
  Zo(powerset(powerset x)) (fun z => partition z x).

Definition partition_fun_of_set y x:=
  canonical_injection y (powerset x).

Lemma partition_set_in_double_powerset: forall y x,
  partition y x -> inc y (powerset (powerset x)).
Proof.
move=> y x [pa _]; aw; move => t ty; aw; move => z zt.
move: (union_inc zt ty); ue.
Qed.

Lemma set_of_partition_rw: forall x y,
  inc y (set_of_partition_set x) = partition y x.
Proof.
move=> x y; rewrite /set_of_partition_set.
apply iff_eq; rewrite Z_rw; intuition.
by apply partition_set_in_double_powerset.
Qed.

Lemma pfs_function: forall y x,
  partition y x -> is_function (partition_fun_of_set y x).
Proof.
move=> y x pa; rewrite/partition_fun_of_set.
by apply ci_function; apply powerset_sub; apply partition_set_in_double_powerset.
Qed.

Lemma pfs_W: forall y x a,
  partition y x -> inc a y ->
  W a (partition_fun_of_set y x) = a.
Proof.
rewrite /partition_fun_of_set=> y x a pa ay.
by apply ci_W => //; apply powerset_sub; apply partition_set_in_double_powerset.
Qed.

Lemma pfs_partition: forall y x,
  partition y x -> partition_fam (graph (partition_fun_of_set y x)) x.
Proof.
move=> y x pa.
move: (pfs_function pa) => fpa.
move: (pa)=> [ux [_ di]].
have Wp: forall i, inc i y -> V i (graph (partition_fun_of_set y x)) = i.
  by move => i iy; apply pfs_W.
have dg: domain (graph (partition_fun_of_set y x)) = y.
  by rewrite f_domain_graph// /partition_fun_of_set /canonical_injection; aw.
split; fprops; split.
  move=> i j; rewrite dg => iy jy; rewrite Wp // Wp //.
  by apply di.
set_extens v => vs.
   move: (unionb_exists vs)=> [w]; rewrite dg.
   move=> [wy]; rewrite Wp // -ux => vW; union_tac.
rewrite -ux in vs; move: (union_exists vs)=> [w [vw wy]].
by srw; exists w; rewrite dg (Wp _ wy).
Qed.

Definition coarser x := graph_on coarser_c (set_of_partition_set x).

Lemma coarser_related: forall x y y',
  related (coarser x) y y' =
  (partition y x & partition y' x & coarser_c y y').
Proof.
rewrite /coarser/graph_on/related=> x y y'.
apply iff_eq; rewrite Z_rw product_pair_rw 2! set_of_partition_rw ; aw;
  intuition.
Qed.

Lemma coarser_related_bis: forall x y y',
  related (coarser x) y y' =
  (partition y x & partition y' x &
    forall a, inc a y' -> exists b, inc b y & sub a b).
Proof. by move=> x y y'; rewrite coarser_related.
Qed.

Lemma coarser_substrate : forall x,
  substrate (coarser x) = set_of_partition_set x.
Proof.
move=> x; rewrite /coarser.
apply extensionality; first by apply graph_on_substrate.
move => t ts.
apply inc_arg1_substrate with t.
rewrite /related/graph_on Z_rw product_pair_rw; aw.
intuition; apply coarser_reflexive.
Qed.

Lemma coarser_order : forall x, order (coarser x).
Proof.
move=> x.
have gc: is_graph (coarser x) by rewrite /coarser; apply graph_on_graph.
hnf; intuition; split=>//.
    move=> y; rewrite coarser_related coarser_substrate set_of_partition_rw.
    intuition; apply coarser_reflexive.
  move=> a b c; rewrite 3! coarser_related.
  by intuition; apply coarser_transitive with b.
move=> a b;rewrite 2!coarser_related. intuition.
by apply coarser_antisymmetric with x.
Qed.

Lemma smallest_partition_is_smallest: forall x y,
  nonempty x ->
  partition y x -> related (coarser x) (smallest_partition x) y.
Proof.
move=> x y nex pa; rewrite coarser_related.
intuition; first by apply partition_smallest.
move=> u uy; rewrite /smallest_partition.
ex_tac.
move: (partition_set_in_double_powerset pa); aw => yp.
by apply powerset_sub; apply yp.
Qed.

Lemma largest_partition_is_largest: forall x y,
  partition y x -> related (coarser x) y (largest_partition x).
Proof.
move=> x y pa; rewrite coarser_related.
intuition; first by apply partition_largest.
move=> u; rewrite /largest_partition; aw.
move=> [b [bx]] <-.
move: pa=> [ux _]; move: bx; rewrite -ux; srw.
by move=> [z [bz zy]]; ex_tac; move=> t; aw=> ->.
Qed.

Definition partition_relation_set y x :=
  partition_relation (partition_fun_of_set y x) x.

Lemma prs_is_equivalence: forall y x,
  partition y x -> is_equivalence (partition_relation_set y x).
Proof.
move=> y x pa; rewrite /partition_relation_set.
apply partition_is_equivalence.
  by apply pfs_function.
by apply pfs_partition.
Qed.

Definition partition_relation_set_aux y x :=
  Zo (powerset (coarse x)) (fun z => exists a, inc a y & z = coarse a).

Lemma partition_relation_set_pr1: forall y x a,
  partition y x ->
  inc a y -> inc (coarse a) (partition_relation_set_aux y x).
Proof.
move=> y x a pa ay.
move: (partition_set_in_double_powerset pa).
rewrite powerset_inc_rw=> yp.
have ap: (inc a (powerset x)) by apply yp.
rewrite /partition_relation_set_aux /coarse Z_rw; aw.
split; first by awi ap; apply product_monotone.
ex_tac.
Qed.

Lemma partition_relation_set_pr: forall y x,
  partition y x ->
  partition_relation_set y x =
  union (partition_relation_set_aux y x).
Proof.
move=> y x pa.
have pfa: (partition_fam (graph(partition_fun_of_set y x)) x).
  by apply pfs_partition.
move: (partition_set_in_double_powerset pa) => ypp.
have sp:source (partition_fun_of_set y x) = y.
  by rewrite /partition_fun_of_set /canonical_injection; aw.
awi ypp.
have p1: is_function (partition_fun_of_set y x) by apply pfs_function.
have p2: partition_fam (graph (partition_fun_of_set y x)) x.
  by move: (prs_is_equivalence pa); fprops.
have p3: is_graph (partition_relation (partition_fun_of_set y x) x).
  by rewrite /partition_relation; apply graph_on_graph.
have p4:is_graph (union (partition_relation_set_aux y x)).
  move=> t tp; move: (union_exists tp); rewrite/partition_relation_set_aux.
  move=> [z]; rewrite Z_rw powerset_inc_rw /coarse.
  by move=> [tz [zp _]]; move: (zp _ tz); aw; intuition.
rewrite /partition_relation_set graph_exten //.
move=> u v; rewrite partition_relation_pr /in_same_coset // sp.
apply iff_eq.
  move=> [i [iy []]]; rewrite pfs_W // /related => ui vi.
  apply union_inc with (coarse i).
    rewrite/coarse; fprops.
  by apply partition_relation_set_pr1.
rewrite /related; srw; move=> [z [Jz]].
rewrite/ partition_relation_set_aux Z_rw; move => [zp [a [ay zc]]].
ex_tac.
by rewrite pfs_W //; move: Jz; rewrite zc /coarse product_pair_rw.
Qed.

Lemma sub_partition_relation_set_coarse: forall y x,
  partition y x -> sub (partition_relation_set y x) (coarse x).
Proof.
move=> y x pa; rewrite partition_relation_set_pr //.
move=> t tu.
move: (union_exists tu) => [z [tz]].
rewrite /partition_relation_set_aux Z_rw.
by move=> [zp _ ]; awi zp; apply zp.
Qed.

Lemma nondisjoint :forall a b c, inc a b -> inc a c -> disjoint b c -> False.
Proof.
by move=> a b c ab ac dg; red in dg; empty_tac1 a; apply intersection2_inc.
Qed.

Lemma partition_relation_set_order: forall x y y',
  partition y x -> partition y' x ->
  sub (partition_relation_set y' x)(partition_relation_set y x) =
  related (coarser x) y y'.
Proof.
move=> x y y' pa pa'.
do 2 rewrite partition_relation_set_pr //.
rewrite coarser_related /coarser_c; apply iff_eq.
  move => suu; split=>//; split=>//; move=> a ay.
  have nea: (nonempty a) by move: pa'=> [_ [ne _]]; apply ne.
  move: nea=> [b ba].
  have p: (forall u,inc u a -> exists c, (inc c y & inc b c & inc u c)).
    move=> u ua.
    have q: (inc (J b u) (union (partition_relation_set_aux y' x))).
      apply union_inc with (coarse a)=>//; rewrite /coarse; fprops.
      apply(partition_relation_set_pr1 pa' ay).
    move: (union_exists (suu _ q)) => [z [Jbb]].
    rewrite /partition_relation_set_aux Z_rw; move=> [zp [c [cy zc]]].
    by ex_tac; move: Jbb; rewrite zc /coarse product_pair_rw.
  move: (p _ ba) => [c [cy [bc _]]].
  ex_tac.
  move=> d da.
  move: (p _ da)=> [f [fy [bf df]]].
  move:pa => [_ [_ aux ]]; case:(aux _ _ cy fy).
    by move => ->.
  by move=> dcf;elim (nondisjoint bc bf dcf).
move=> [_ [_ hyp]] z zu.
move: (union_exists zu)=> [t [zt]].
rewrite /partition_relation_set_aux Z_rw; move => [tp [a [ay tc]]].
move: (hyp _ ay)=> [b [iby ab]].
apply union_inc with (coarse b); last by apply partition_relation_set_pr1.
have scab: (sub (coarse a) (coarse b)) by apply product_monotone.
apply scab; ue.
Qed.

Lemma partition_relation_set_order_antisymmetric: forall x y y',
  partition y x -> partition y' x ->
  (partition_relation_set y' x = partition_relation_set y x) ->
   y = y'.
Proof.
suff: (forall x y y',
  partition y x -> partition y' x ->
  (partition_relation_set y' x = partition_relation_set y x) ->
  sub y y').
  move=> aux a b c p1 p2 eq. apply extensionality.
  apply (aux _ _ _ p1 p2 eq). apply (aux _ _ _ p2 p1 (sym_eq eq)).
move=> x y y' pa pa'.
rewrite (partition_relation_set_pr pa) (partition_relation_set_pr pa').
move=> eq a ay.
move: (partition_relation_set_pr1 pa ay)=> cpy.
have nea: (nonempty a) by move: pa=> [_ [ne _]]; apply ne.
move: nea=> [b ba].
have p: (forall u v,inc u a -> inc v a->
    exists c, (inc c y' & inc u c & inc v c)).
   move=> u v ua va.
   have p1: inc (J u v) (coarse a) by rewrite /coarse; fprops.
   have p2: (inc (J u v) (union (partition_relation_set_aux y' x))).
   rewrite eq; union_tac.
   move: (union_exists p2) => [z [Jbb]].
   rewrite /partition_relation_set_aux Z_rw; move=> [zp [c [cy zc]]].
   by ex_tac; move: Jbb; rewrite zc /coarse product_pair_rw.
move: (p _ _ ba ba) => [c [cy [bc _]]].
suff: a = c by move=> ->.
set_extens t => ta.
  move: (p _ _ ta ta) => [c' [cy' [tc' _]]].
  move: (p _ _ ba ta) => [c'' [cy'' [bc'' tc'']]].
  move: pa' => [_ [_ aux ]]; case:(aux _ _ cy cy'').
    move => ->; case:(aux _ _ cy'' cy'); first by move => ->.
    by move=> dcf;elim (nondisjoint tc'' tc' dcf).
  by move=> dcf;elim (nondisjoint bc bc'' dcf).
have p1: (inc (J b t) (coarse c)) by rewrite/coarse; fprops.
have p2: (inc (J b t) (union (partition_relation_set_aux y' x))).
  apply union_inc with (coarse c) => //.
  apply (partition_relation_set_pr1 pa' cy).
move: p2; rewrite eq /partition_relation_set_aux => p2.
move: (union_exists p2)=> [z [Jbb]]; rewrite Z_rw;move=> [zp [d [dy zx]]].
move: Jbb; rewrite zx /coarse; aw; move=> [_ [bd td]].
move: pa => [_ [_ aux ]]; case:(aux _ _ ay dy).
    by move=> ->.
move=> dfc; elim (nondisjoint ba bd dfc).
Qed.

Lemma preorder_prop1: forall g,
  is_graph g ->
  sub (identity_g (substrate g)) g -> sub (compose_graph g g) g ->
  compose_graph g g = g.
Proof.
move=> g gg sig scg.
apply extensionality; first by aw.
move => x xg; aw; split; first by apply gg.
exists (Q x); rewrite (gg _ xg); ee; apply sig; aw; ee; substr_tac.
Qed.

Theorem order_pr: forall r,
  order r =
    (compose_graph r r = r &
    intersection2 r (opposite_order r) = identity_g (substrate r)).
Proof.
move=> r.
apply iff_eq.
  move=> or.
  set (d:= identity_g (substrate r)).
  have i2: (intersection2 r (opposite_order r) = d).
    set_extens t.
      aw; move=> [tr].
      rewrite inverse_graph_rw;fprops; move=> [pt Jr].
      have px: (J (P t) (Q t) = t) by aw.
      rewrite - px in tr.
      move: (order_antisymmetry or tr Jr)=> pq.
      by rewrite /d -px pq; aw; split=>//; substr_tac.
    rewrite/d; rewrite inc_diagonal_rw; move=> [pt [Ps pq]].
    have Jpq: (J (P t) (Q t) = t) by aw.
    rewrite -Jpq -pq.
    have rpp: (related r (P t) (P t)) by order_tac.
    by apply intersection2_inc=>//; aw.
  have gr: (is_graph r) by fprops.
  have sd: (sub d r) by rewrite -i2; apply intersection2sub_first.
  have sc: (sub (compose_graph d r) (compose_graph r r)).
    by apply composition_increasing; fprops.
  have crrr: (sub (compose_graph r r) r).
    by move: or => [_[t _]];rewrite -idempotent_graph_transitive //.
  by split =>//; apply preorder_prop1.
move=> [crrr iro].
have gr: is_graph r by rewrite -crrr; apply composition_is_graph.
hnf; intuition; split=>//.
- move=> y ys.
  have: (inc (J y y) (identity_g (substrate r))) by aw; auto.
  by rewrite -iro; move=> Ji; apply (intersection2_first Ji).
- have: sub (compose_graph r r) r by rewrite crrr; fprops.
  by rewrite -idempotent_graph_transitive //; move=> [_].
- move => x y rxy ryx.
  have p1: (inc (J x y) (opposite_order r)) by aw.
  have: (inc (J x y) (identity_g (substrate r))).
    by rewrite - iro; apply intersection2_inc.
  aw ; intuition.
Qed.

Lemma preorder_is_preorder: forall r,
  preorder r -> preorder_r (related r).
Proof.
move=> r [[gr rr] [_ tr]].
split=>//.
move=> x y rxy.
have p1: (inc x (substrate r)) by substr_tac.
have p2: (inc y (substrate r)) by substr_tac.
by split; apply rr.
Qed.

Lemma opposite_is_preorder1: forall r,
  preorder r -> preorder (opposite_order r).
Proof.
move=> r [[gr rr] [_ tr]].
have go: (is_graph (opposite_order r)) by fprops.
have ss: (sub (substrate (opposite_order r)) (substrate r)).
  move=> t; rewrite inc_substrate_rw //inc_substrate_rw //.
  by case;move=> [y]; aw =>h; [ right | left ] ;ex_tac.
split.
  by split=>//; move=> y ys; red; aw; apply rr; apply ss.
split=>//; move => x y z; rewrite /related;aw.
move =>p1 p2; apply (tr _ _ _ p2 p1).
Qed.

Lemma equivalence_preorder: forall r,
  preorder_r r ->
  equivalence_r (fun x y => r x y & r y x).
Proof.
move=> r [ tr _]; split; first by move=> x y [rxy ryx].
move=> x y z [xy yx] [yz zy].
split; [ apply (tr _ _ _ xy yz) | apply (tr _ _ _ zy yx)].
Qed.

Lemma compatible_equivalence_preorder: forall r,
  let s := (fun x y => r x y & r y x) in
  preorder_r r -> forall x y x' y', r x y -> s x x' -> s y y' -> r x' y'.
Proof.
move=> r s [tr _] x y x' y' rxy [rxx' rx'x] [ryy' ry'y].
move: (tr _ _ _ rx'x rxy)=> rx'y.
apply (tr _ _ _ rx'y ryy').
Qed.

Definition equivalence_associated_o r:= intersection2 r (opposite_order r).

Lemma equivalence_preorder1: forall r,
  preorder r ->
  is_equivalence (equivalence_associated_o r).
Proof.
move=> r pr.
rewrite /equivalence_associated_o.
have gr: is_graph r by apply preorder_graph.
have gi: is_graph (opposite_order r) by fprops.
move: (inter2_is_graph2 gr (x:=r)) => gi2.
have gi3: is_graph (intersection2 r (opposite_order r)).
  by move=> x xi; apply (gr _ (intersection2_first xi)).
apply symmetric_transitive_equivalence.
  split=>//; move=> x y; rewrite /related; aw; intuition.
split=>//; move=> x y z;rewrite /related; aw.
move=> [xy yx][yz zy]; move: pr=> [_ [_ tr]].
split; [apply (tr _ _ _ xy yz) | apply (tr _ _ _ zy yx) ].
Qed.

Lemma substrate_equivalence_associated_o: forall r,
  preorder r ->
  substrate (equivalence_associated_o r) = substrate r.
Proof.
move=> r pr.
move: (equivalence_preorder1 pr)=> eq.
set_extens x => xs.
  move: (reflexivity_e eq xs).
  rewrite/related /equivalence_associated_o=> h.
  by move:(intersection2_first h)=> h1; substr_tac.
move: pr=> [[gr rr] _].
move: (rr _ xs); rewrite /related=> Js.
have Je: (inc (J x x) (equivalence_associated_o r)).
  rewrite /equivalence_associated_o; apply intersection2_inc =>//; aw.
substr_tac.
Qed.

Lemma compatible_equivalence_preorder1: forall r u v x y,
  preorder r -> related r x y ->
  related (equivalence_associated_o r) x u ->
  related (equivalence_associated_o r) y v->
  related r u v.
Proof.
rewrite /related /equivalence_associated_o=> r u v x y pr rxy.
aw.
move: pr => [_ [_ tr]] [_ ux] [yv _].
move: (tr _ _ _ ux rxy)=> uy.
apply (tr _ _ _ uy yv).
Qed.

Lemma preorder_prop: forall g,
  is_graph g ->
  preorder g = (sub (identity_g (substrate g)) g & sub (compose_graph g g) g).
Proof.
move=> g gg.
apply iff_eq.
  move=> [[_ rr] tr].
  split; move=> x.
  rewrite inc_diagonal_rw; move=> [px [Px pq]].
    have : (J (P x) (Q x) = x) by aw.
    by move=> <-; rewrite -pq; apply rr.
  rewrite idempotent_graph_transitive // in tr.
  apply tr.
move=> [s1 s2].
split.
  split=>//.
  move=> y ys; rewrite /related; apply s1.
  by rewrite inc_diagonal_rw; aw; fprops.
by rewrite idempotent_graph_transitive.
Qed.

Lemma preorder_prop2: forall g,
  preorder g -> compose_graph g g = g.
Proof.
move=> g pg.
have gg: is_graph g by apply preorder_graph.
rewrite (preorder_prop gg) in pg.
by apply preorder_prop1; intuition.
Qed.

Lemma preorder_reflexivity: forall r a,
  preorder r -> inc a (substrate r) = related r a a.
Proof.
move=> r a [[g pr] _].
apply iff_eq; first by apply pr.
move=> h; substr_tac.
Qed.

Definition order_associated (r:Set) :=
  let s := (graph(canon_proj (equivalence_associated_o r))) in
  compose_graph (compose_graph s r) (opposite_order s).

Lemma order_associated_graph: forall r,
  is_graph (order_associated r).
Proof.
rewrite /order_associated=> r; apply composition_is_graph.
Qed.

Lemma compose3_related: forall s r u v,
  related (compose_graph (compose_graph s r) (opposite_order s)) u v =
  exists x, exists y, related s x u & related s y v & related r x y.
Proof.
move=> s r u v; rewrite compose_related ;apply iff_eq.
  move=> [y []]; aw; bw; move=> yu [z [yz zv]].
  by exists y; exists z.
move=> [x [y [xu [yv xy]]]]; exists x.
aw; bw; ee.
by exists y.
Qed.

Lemma order_associated_related1: forall r u v,
  preorder r->
  related (order_associated r) u v =
  ( inc u (quotient (equivalence_associated_o r)) &
    inc v (quotient (equivalence_associated_o r)) &
    exists x, exists y, inc x u & inc y v & related r x y).
Proof.
move=> r u v pr.
set (s:= equivalence_associated_o r).
set (p:= graph (canon_proj s)).
rewrite /order_associated -/s -/p.
have es:is_equivalence s by rewrite /s; apply equivalence_preorder1.
rewrite compose3_related.
apply iff_eq.
  move=> [x [y [xu [yv xy]]]].
  have fc: is_function (canon_proj s) by apply canon_proj_function.
  move: (inc_pr1graph_source fc xu); aw => xs.
  move: (inc_pr1graph_source fc yv); aw => ys.
  have: (u = W x (canon_proj s)) by symmetry; apply W_pr=>//.
  have: (v = W y (canon_proj s)) by symmetry; apply W_pr=>//.
  rewrite canon_proj_W // canon_proj_W //.
  move=> -> ->; ee.
  exists x; exists y; split; first by apply inc_itself_class.
  by split=>//; apply inc_itself_class.
move=> [uq [vq [x [y [xu [yv xy]]]]]].
exists x; exists y.
split.
  rewrite /p/related related_graph_canon_proj //.
  apply (inc_in_quotient_substrate es xu uq).
split =>//.
rewrite /p/related related_graph_canon_proj //.
apply (inc_in_quotient_substrate es yv vq).
Qed.

Lemma order_associated_related2: forall r u v,
  preorder r->
  related (order_associated r) u v =
  ( inc u (quotient (equivalence_associated_o r)) &
    inc v (quotient (equivalence_associated_o r)) &
    forall x y, inc x u -> inc y v -> related r x y).
Proof.
move=> r u v pr; rewrite order_associated_related1 //.
set (s:= equivalence_associated_o r).
have es: is_equivalence s by rewrite /s; apply equivalence_preorder1.
apply iff_eq.
  move=> [uq [vq [x [y [xu [yv xy]]]]]].
  ee.
  move=> a b au bv.
  have xa: (related s x a).
    by rewrite in_class_related //; exists u; intuition; rewrite - inc_quotient.
  have yb: (related s y b).
    by rewrite in_class_related //; exists v; intuition; rewrite - inc_quotient.
  apply (compatible_equivalence_preorder1 pr xy xa yb).
move => [uq [vq hyp]]; split =>//; split=>//.
move: (non_empty_in_quotient es uq)=> [x xu].
move: (non_empty_in_quotient es vq)=> [y yv].
by exists x; exists y ; auto.
Qed.

Lemma eao_related: forall r a b,
 related (equivalence_associated_o r) a b -> related r a b.
Proof.
by move=> r a b; rewrite/equivalence_associated_o/related; aw; case.
Qed.

Lemma order_associated_substrate: forall r,
  preorder r-> substrate (order_associated r) =
  (quotient (equivalence_associated_o r)).
Proof.
move=> r pr.
have ea:is_equivalence (equivalence_associated_o r).
  by apply equivalence_preorder1.
set eao:= (equivalence_associated_o r).
have prop: forall a b, inc (J a b) (order_associated r)->
  (inc a (quotient eao) & inc b (quotient eao)).
  move=> a b Jab.
  have: (related (order_associated r) a b) by done.
  by rewrite order_associated_related2//; intuition.
set_extens x.
  rewrite inc_substrate_rw; last by apply order_associated_graph.
  by case; move=> [y yp]; move: (prop _ _ yp); intuition.
move=> xq.
suff: (related (order_associated r) x x) by move => w; substr_tac.
rewrite order_associated_related2 //; ee.
move=> z y zx yx.
have: (related (equivalence_associated_o r) z y).
  rewrite in_class_related //; exists x.
  by intuition; rewrite - inc_quotient.
apply eao_related.
Qed.

Lemma order_associated_order: forall r,
  preorder r-> order (order_associated r).
Proof.
move=> r pr.
have go: is_graph (order_associated r) by apply order_associated_graph.
have eea:is_equivalence (equivalence_associated_o r)
  by apply equivalence_preorder1.
have gr: is_graph r by move: pr=> [[]].
hnf; intuition;split =>//.
- move=> y; rewrite order_associated_substrate // => ys.
  move: pr=> [rr rt].
  rewrite order_associated_related2; split=>//; split=>//.
  move=> x z xy zy.
  have: (related (equivalence_associated_o r) x z).
     by rewrite in_class_related//; exists y; split=>//; rewrite - inc_quotient.
   apply eao_related.
- move=> x y z; do 3 rewrite order_associated_related2 //.
  move=>[xq [yq rxy]][_ [zq ryz]]; split=>//; split=>//.
  move => a b ax bz; move: (non_empty_in_quotient eea yq)=> [c cy].
  move:pr => [_ [_ tr]].
  apply (tr _ _ _ (rxy _ _ ax cy) (ryz _ _ cy bz)).
- move=> x y; do 2 rewrite order_associated_related2 //.
  move=> [xq [yq rxy]][_ [_ ryx]].
  move: (non_empty_in_quotient eea xq)=> [a ax].
  move: (non_empty_in_quotient eea yq)=> [b biy].
  move: (rxy _ _ ax biy)(ryx _ _ biy ax)=> rab rba;
  have reab: (related (equivalence_associated_o r) a b).
    rewrite /related /equivalence_associated_o; apply intersection2_inc =>//.
    aw.
  move: xq yq; srw => // xq yq.
  have bx: inc b x.
    move: xq; rewrite is_class_rw //.
    by move=> [_ [_ h]]; rewrite -(h a b ax) in reab.
  case (class_dichot xq yq) =>// hyp.
  elim (nondisjoint bx biy hyp).
Qed.

Lemma order_associated_pr: forall r,
  preorder r ->
  order_associated r = image_by_fun (
    ext_to_prod(canon_proj (equivalence_associated_o r))
    (canon_proj (equivalence_associated_o r))) r.
Proof.
move=> r pr.
set (s:= equivalence_associated_o r).
have es:is_equivalence s by rewrite /s; apply equivalence_preorder1.
have ss:substrate s = substrate r.
  by rewrite /s substrate_equivalence_associated_o.
have fep: is_function (ext_to_prod (canon_proj s) (canon_proj s)).
  by apply ext_to_prod_function; apply canon_proj_function=>//.
have gi:
  is_graph (image_by_fun (ext_to_prod (canon_proj s) (canon_proj s)) r).
  move=> t; rewrite /image_by_fun; aw; move=> [x [xr Jg]].
  by move:(inc_pr2graph_target fep Jg); rewrite /ext_to_prod; aw; intuition.
 rewrite graph_exten //; last by apply order_associated_graph.
move=> u v; rewrite order_associated_related2 //.
fold s; rewrite /related/image_by_fun; apply iff_eq.
  move=> [uq [vq hyp]].
  aw;exists (J (rep u) (rep v)).
  split; first by apply hyp; apply (inc_rep_itself es).
  have p1: (class s (rep u) =u) by apply class_rep.
  have p2: (class s (rep v) =v) by apply class_rep.
  have : (J u v = J (class s (rep u)) (class s (rep v))) by rewrite p1 p2.
  rewrite - ext_to_prod_rel_W; fprops; move =>->.
  apply W_pr3=> //.
  by rewrite /ext_to_prod; aw; fprops.
aw; move=> [x [xr]].
rewrite/related=> Jg; move: (W_pr fep Jg)=> Wx.
have px: (is_pair x) by move: pr=> [[g _] _]; apply g.
have Jpq: J (P x) (Q x) = x by aw.
have ps: (inc (P x) (substrate s)) by rewrite ss; substr_tac.
have qs: (inc (Q x) (substrate s)) by rewrite ss; substr_tac.
move: Wx; rewrite -Jpq ext_to_prod_rel_W // => JJ.
move: (pr1_def JJ) (pr2_def JJ) => e1 e2.
have uq: inc u (quotient s) by rewrite - e1; gprops.
have vq: inc v (quotient s) by rewrite - e2; gprops.
ee; move=> a b au bv.
suff: (related (order_associated r) u v).
  by rewrite order_associated_related2 //; move=> [_ [_ h]]; apply (h _ _ au bv).
rewrite order_associated_related1 //;ee.
exists (P x); exists (Q x).
rewrite -e1 -e2; split; first by apply inc_itself_class.
split; first by apply inc_itself_class.
by red; rewrite px.
Qed.