Module mathcomp.classical.classical_orders

From mathcomp Require Import boot order ssralg ssrnum interval.
From mathcomp Require Import mathcomp_extra boolp classical_sets.
From HB Require Import structures.
From mathcomp Require Import functions set_interval.

# classical orders This file provides some additional order theory that requires stronger axioms than mathcomp's own orders expect. ``` same_prefix n == two elements in a product space agree up n first_diff x y == the first occurrence where x n != y n, or None big_lexi_le == the (countably) infinite lexicographical ordering big_lexi_order == an alias for attaching this order type start_with n x y == x for the first n values, then switches to y ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.

Definition { : Type} ( : I -> Type) : Type := forall , T i.
. () ( -> choiceType) :=
Choice.on (big_lexi_order K).

Section big_lexi_le.
Context { : nat -> eqType}.

Definition ( : forall , K n) :=
forall , (m < n)%O -> t1 m = t2 m.

Lemma : same_prefix 0 t1 t2

Proof.

by []. Qed.

Hint Resolve same_prefix0 : core.

Lemma : same_prefix n t1 t2 <-> same_prefix n t2 t1.

Proof.

by rewrite /same_prefix; split => + m mn => /(_ m mn). Qed.

Lemma :
n <= m -> same_prefix m t1 t2 -> same_prefix n t1 t2.

Proof.

move=> nm + r rn; apply.
by move: nm; rewrite leq_eqVlt => /predU1P[<-//|]; exact: ltn_trans.
Qed.

Lemma : same_prefix n x x

Proof.

by []. Qed.

Lemma :
  same_prefix n x y ->
  same_prefix n y z ->
  same_prefix n x z.

Proof.

by move=> + + m mn => /(_ _ mn) ->; exact. Qed.

Definition ( : forall , K n) : option nat :=
xget None (Some @` [set | same_prefix n t1 t2 /\ t1 n != t2 n]).

Lemma : first_diff t1 t2 = first_diff t2 t1.

Proof.

rewrite /first_diff /=; congr (xget _ (image _ _)).
under eq_set do rewrite eq_sym.
by apply/seteqP; split => z/= [] /same_prefix_sym.
Qed.

Lemma ( : forall , K n) :
  same_prefix n x y -> x n != y n ->
  same_prefix m x y -> x m != y m ->
  n = m.

Proof.

move=> nfx xyn mfx xym; apply/eqP; rewrite eq_le 2!leNgt; apply/andP; split.
by apply/negP => /nfx; exact/eqP.
by apply/negP => /mfx; exact/eqP.
Qed.

Lemma :
first_diff x y = Some n <-> same_prefix n x y /\ x n != y n.

Proof.

split => [|[pfx xNy]]; rewrite /first_diff.
by case: xgetP=> //= -[m ->|//] [p + <-[]] => /[swap] ->.
case: xgetP => /=; last by move=> /(_ (Some n))/forall2NP/(_ n)[/not_andP[]|].
by move=> [m|? []//] -> [p [pxy xyp]] <-; rewrite (@first_diff_unique x y n p).
Qed.

Lemma : t1 = t2 <-> first_diff t1 t2 = None.

Proof.

rewrite /first_diff; split => [->|].
by case: xgetP => //= -[n|//] -> [m []]; rewrite eqxx.
case: xgetP => [? -> [i /=] [?] ? <-//|/= R _].
apply/functional_extensionality_dep.
suff : forall , x < n -> t1 x = t2 x by move=> + n => /(_ n.+1)/(_ n); exact.
elim => [//|n ih x]; rewrite ltnS leq_eqVlt => /predU1P[->|xn]; last exact: ih.
by have /forall2NP/(_ n)[/not_andP[//|/negP/negPn/eqP]|] := R (Some n).
Qed.

Lemma :
  n < m ->
  first_diff a x = Some n ->
  first_diff a y = Some m ->
  first_diff x y = Some n.

Proof.

move=> nm /first_diff_SomeP [xpfx xE] /first_diff_SomeP [ypfx yE].
apply/first_diff_SomeP; split; last by rewrite -(ypfx _ nm) eq_sym.
by move=> o /[dup] on /xpfx <-; exact/ypfx/(ltn_trans on).
Qed.

Arguments first_diff_lt a {x y n m}.

Lemma :
  first_diff a x = Some n ->
  first_diff a y = Some n ->
  first_diff x y = Some m ->
  n <= m.

Proof.

case/first_diff_SomeP => axPfx axn /first_diff_SomeP[ayPfx ayn].
case/first_diff_SomeP => xyPfx; apply: contraNleq => mn.
by rewrite -(ayPfx _ mn) -(axPfx _ mn).
Qed.

Lemma ( : forall : nat, K n) :
x i != b <-> first_diff x (dfwith x b) = Some i.

Proof.

split => [xBn|/first_diff_SomeP[_]]; last by rewrite dfwith_in.
apply/first_diff_SomeP; split; last by rewrite dfwith_in.
by move=> n ni; rewrite dfwith_out// gt_eqF.
Qed.

Definition
( : forall , K n -> K n -> bool) ( : forall , K n) :=
if first_diff t1 t2 is Some n then R n (t1 n) (t2 n) else true.

Lemma : reflexive (big_lexi_le R).

Proof.

move=> x; rewrite /big_lexi_le /= /first_diff.
by case: xgetP => //= -[n _|//] [m []]; rewrite eqxx.
Qed.

Lemma : (forall , antisymmetric (R n)) ->
antisymmetric (big_lexi_le R).

Proof.

move=> antiR x y /andP[xy yx]; apply/first_diff_NoneP; move: xy yx.
rewrite /big_lexi_le first_diff_sym.
case E : (first_diff y x) => [n|]// Rxy Ryx.
case/first_diff_SomeP : E => _.
by apply: contra_neqP => _; apply/antiR; rewrite Ryx.
Qed.

Lemma :
  (forall , transitive (R n)) ->
  (forall , antisymmetric (R n)) ->
  transitive (big_lexi_le R).

Proof.

move=> Rtrans Ranti y x z; rewrite /big_lexi_le /=.
case Ep : (first_diff x y) => [p|]; last by move/first_diff_NoneP : Ep ->.
case Er : (first_diff x z) => [r|]; last by move/first_diff_NoneP : Er ->.
case Eq : (first_diff y z) => [q|]; first last.
  by move: Ep Er; move/first_diff_NoneP: Eq => -> -> [->].
have [pq|qp|pqE]:= ltgtP p q.
- move: Er.
  rewrite (first_diff_lt y pq)// 1?first_diff_sym// => -[<-] ? _.
  by case/first_diff_SomeP : Eq => /(_ _ pq) <-.
- move: Er.
  rewrite first_diff_sym (first_diff_lt y qp)// 1?first_diff_sym// => -[<-] _ ?.
  by case/first_diff_SomeP: Ep => /(_ _ qp) ->.
- move: Ep Eq; rewrite pqE => Eqx Eqz.
  rewrite first_diff_sym in Eqx; have := first_diff_eq Eqx Eqz Er.
  rewrite leq_eqVlt => /predU1P[->|qr]; first exact: Rtrans.
  case/first_diff_SomeP : Er => /(_ _ qr) -> _ qzy qyz.
  case/first_diff_SomeP : Eqz => _; apply: contra_neqP => _.
  by apply/Ranti/andP; split.
Qed.

Lemma : (forall , total (R n)) -> total (big_lexi_le R).

Proof.

move=> Rtotal x y.
case E : (first_diff x y) => [n|]; first last.
by move/first_diff_NoneP : E ->; rewrite big_lexi_le_reflexive.
by rewrite /big_lexi_le E first_diff_sym E; exact: Rtotal.
Qed.

Definition ( : forall , K n) ( : nat) : K i :=
if (i < n)%O then t1 i else t2 i.

Lemma : same_prefix n x (start_with n x y).

Proof.

by move=> r rn; rewrite /start_with rn. Qed.

End big_lexi_le.

Section big_lexi_porder.
Context {} { : nat -> porderType d}.

Let ( : K n) := (k1 <= k2)%O.

Local Lemma : reflexive (big_lexi_le Rn).

Proof.

exact: big_lexi_le_reflexive. Qed.

Local Lemma : antisymmetric (big_lexi_le Rn).

Proof.

by apply: big_lexi_le_anti => n; exact: le_anti. Qed.

Local Lemma : transitive (big_lexi_le Rn).

Proof.

by apply: big_lexi_le_trans => n; [exact: le_trans|exact: le_anti]. Qed.

..Le_isPOrder.Build d (big_lexi_order K)
big_lexi_ord_reflexive big_lexi_ord_anti big_lexi_ord_trans.

Lemma ( : big_lexi_order K) :
(a <= b)%O = if first_diff a b is Some n then (a n <= b n)%O else true.

Proof.

by []. Qed.

End big_lexi_porder.

Section big_lexi_total.
Context {} { : nat -> orderType d}.

Local Lemma : total (@Order.le _ (big_lexi_order K)).

Proof.

by apply: big_lexi_le_total => ?; exact: le_total. Qed.

..POrder_isTotal.Build _
(big_lexi_order K) big_lexi_ord_total.

End big_lexi_total.

Section big_lexi_bottom.
Context {} { : nat -> bPOrderType d}.

Let : big_lexi_order K := (fun=> \bot)%O.
Local Lemma ( : big_lexi_order K) : (b <= x)%O.

Proof.

by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.le0x.
Qed.

..hasBottom.Build _
(big_lexi_order K) b big_lex_bot.

End big_lexi_bottom.

Section big_lexi_top.
Context {} { : nat -> tPOrderType d}.

Let : big_lexi_order K := (fun=> \top)%O.
Local Lemma ( : big_lexi_order K) : (x <= t)%O.

Proof.

by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.lex1.
Qed.

..hasTop.Build _
  (big_lexi_order K) t big_lex_top.

End big_lexi_top.

Section big_lexi_intervals.
Context {} { : nat -> orderType d}.

Lemma ( : big_lexi_order K) :
  (a < b)%O ->
  first_diff a b = Some n ->
  same_prefix n.+1 x b ->
  (a < x)%O.

Proof.

move=> + /[dup] abD /first_diff_SomeP[pfa abN].
case E1 : (first_diff a x) => [m|]; first last.
by move/first_diff_NoneP : E1 <- => _/(_ n (ltnSn _))/eqP/negPn; rewrite abN.
move=> ab pfx; rewrite lt_neqAle; apply/andP; split.
by apply/eqP => /first_diff_NoneP; rewrite E1.
move: ab; rewrite lt_neqAle => /andP[ba].
rewrite 2!leEbig_lexi_order E1 abD.
suff : n = m by have := pfx n (ltnSn _) => /[swap] -> ->.
apply: (@first_diff_unique _ a x) => //=; [| |by case/first_diff_SomeP : E1..].
- by apply/(same_prefix_trans pfa)/same_prefix_sym; exact: same_prefix_leq.
- by rewrite (pfx n (ltnSn _)).
Qed.

Lemma ( : big_lexi_order K) :
  (b < a)%O ->
  first_diff a b = Some n ->
  same_prefix n.+1 x b ->
  (x < a)%O.

Proof.

move=> + /[dup] abD /first_diff_SomeP[pfa /eqP abN].
case E1 : (first_diff x a) => [m|]; first last.
  by move/first_diff_NoneP : E1 -> => _ /(_ n (ltnSn _)).
move=> ab pfx; rewrite lt_neqAle; apply/andP; split.
  by apply/negP => /eqP/first_diff_NoneP; rewrite E1.
move: ab; rewrite lt_neqAle => /andP[ba].
rewrite 2!leEbig_lexi_order (@first_diff_sym _ b a) E1 abD.
suff : n = m by have := pfx n (ltnSn _) => /[swap] -> ->.
apply: (@first_diff_unique _ x a) => //=; [| |by case/first_diff_SomeP : E1..].
- apply/same_prefix_sym/(same_prefix_trans pfa)/same_prefix_sym.
  exact: same_prefix_leq.
- by rewrite (pfx n (ltnSn _)) eq_sym; exact/eqP.
Qed.

Lemma ( : big_lexi_order K) :
  (a <= x <= b)%O ->
  same_prefix n a b ->
  same_prefix n x a.

Proof.

move=> axb; elim: n => // n IH pfxSn m mSn.
have pfxA : same_prefix n a x.
  exact/same_prefix_sym/IH/(same_prefix_leq _ pfxSn).
have pfxB : same_prefix n x b.
  apply: (@same_prefix_trans _ n x a b); first exact/same_prefix_sym.
  exact: (same_prefix_leq _ pfxSn).
move: mSn; rewrite ltEnat/= ltnS leq_eqVlt => /predU1P[->|]; first last.
  by move: pfxA; rewrite same_prefix_sym; exact.
apply: le_anti; apply/andP; split.
  case/andP: axb => ? +; rewrite leEbig_lexi_order (pfxSn n (ltnSn _)).
  case E : (first_diff x b) => [r|]; last by move/first_diff_NoneP : E ->.
  move=> xrb; have : n <= r.
    rewrite leqNgt; apply/negP=> /[dup] /pfxB xbE.
    by case/first_diff_SomeP : E => _; rewrite xbE eqxx.
  rewrite leq_eqVlt => /predU1P[->//|nr].
  by case/first_diff_SomeP : E => /(_ n nr) ->.
case/andP : axb => + ?; rewrite leEbig_lexi_order.
case E : (first_diff a x) => [r|]; last by move/first_diff_NoneP : E => <-.
move=> xrb.
have : n <= r.
  rewrite leqNgt; apply/negP => /[dup] /pfxA xbE.
  by case/first_diff_SomeP : E => _; rewrite xbE eqxx.
rewrite leq_eqVlt => /predU1P[->//|nr].
by case/first_diff_SomeP : E => /(_ n nr) ->.
Qed.

Lemma ( : interval (big_lexi_order K))
    ( : big_lexi_order K) :
  itv_open_ends i -> x \in i ->
  exists , same_prefix n x `<=` [set` i].

Proof.

move: i; case=> [][[]l|[]] [[]r|[]]// ?; rewrite ?in_itv /= ?andbT.
- move=> /andP[lx xr].
  case E1 : (first_diff l x) => [m|]; first last.
    by move: lx; move/first_diff_NoneP : E1 ->; rewrite bnd_simp.
  case E2 : (first_diff x r) => [n|]; first last.
    by move: xr; move/first_diff_NoneP : E2 ->; rewrite bnd_simp.
  exists (Order.max n m).+1 => p xppfx; rewrite set_itvE.
  apply/andP; split.
    apply: (big_lexi_order_prefix_lt lx E1) => w wm; apply/esym/xppfx.
    by move/ltnSE/leq_ltn_trans : wm; apply; rewrite ltnS leq_max leqnn orbT.
  rewrite first_diff_sym in E2.
  apply: (big_lexi_order_prefix_gt xr E2) => w wm; apply/esym/xppfx.
  by move/ltnSE/leq_ltn_trans : wm; apply; rewrite ltnS leq_max leqnn.
- move=> lx.
  case E1 : (first_diff l x) => [m|]; first last.
    by move: lx; move/first_diff_NoneP : E1 ->; rewrite bnd_simp.
  exists m.+1 => p xppfx; rewrite set_itvE /=.
  by apply: (big_lexi_order_prefix_lt lx E1) => w wm; exact/esym/xppfx.
- move=> xr.
  case E2 : (first_diff x r) => [n|]; first last.
    by move: xr; move/first_diff_NoneP : E2 ->; rewrite bnd_simp.
  exists n.+1; rewrite first_diff_sym in E2 => p xppfx.
  rewrite set_itvE /=.
  by apply: (big_lexi_order_prefix_gt xr E2) => w wm; exact/esym/xppfx.
by move=> _; exists 0 => ? ?; rewrite set_itvE.
Qed.

End big_lexi_intervals.

Lemma {} { : nat -> tbOrderType d}
  ( : big_lexi_order K) :
  same_prefix n x = `[
    (@start_with K n x (fun=>\bot):big_lexi_order K)%O,
    (start_with n x (fun=>\top))%O].

Proof.

rewrite eqEsubset; split=> [z pfxz|z]; first last.
  rewrite set_itvE /= => xbt; apply: same_prefix_trans.
    exact: (start_with_prefix _ (fun=> \bot)%O).
  apply/same_prefix_sym/(big_lexi_order_between xbt).
  apply: same_prefix_trans (start_with_prefix _ _).
  exact/same_prefix_sym/start_with_prefix.
rewrite set_itvE /= !leEbig_lexi_order; apply/andP; split;
  case E : (first_diff _ _) => [m|] //; rewrite /start_with /=.
- by case: ifPn => [/pfxz -> //|]; rewrite le0x.
- by case: ifPn => [/pfxz -> //|]; rewrite lex1.
Qed.

Files

Module mathcomp.classical.classical_orders