Files

  • mathcomp

    • Top

    Module mathcomp.classical.classical_orders

    From mathcomp Require Import all_ssreflect 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 ```

    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 big_lexi_order {I : Type} (T : I -> Type) : Type := forall i, T i.
    HB.instance Definition _ (I : Type) (K : I -> choiceType) :=
      Choice.on (big_lexi_order K).

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

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

    Lemma same_prefix0 t1 t2 : same_prefix 0 t1 t2
    Proof.
    by []. Qed.
    Hint Resolve same_prefix0 : core.

    Lemma same_prefix_sym n t1 t2 : same_prefix n t1 t2 <-> same_prefix n t2 t1.
    Proof.
    by rewrite /same_prefix; split => + m mn => /(_ m mn). Qed.

    Lemma same_prefix_leq n m t1 t2 :
      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_refl n x : same_prefix n x x
    Proof.
    by []. Qed.

    Lemma same_prefix_trans n x y z :
      same_prefix n x y ->
      same_prefix n y z ->
      same_prefix n x z.
    Proof.
    by move=> + + m mn => /(_ _ mn) ->; exact. Qed.

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

    Lemma first_diff_sym t1 t2 : 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 first_diff_unique (x y : forall n, K n) n m :
      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_SomeP x y n :
      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 first_diff_NoneP t1 t2 : 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 n x, 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 first_diff_lt a x y n m :
      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_eq a x y n m :
      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 first_diff_dfwith (x : forall n : nat, K n) i b :
      x i != b <-> first_diff x (dfwith x i b) = Some i.
    Proof.
    split => [xBn|/first_diff_SomeP[_]]; last by rewrite dfwithin.
    apply/first_diff_SomeP; split; last by rewrite dfwithin.
    by move=> n ni; rewrite dfwithout// gt_eqF.
    Qed.

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

    Lemma big_lexi_le_reflexive R : reflexive (big_lexi_le R).
    Proof.
    move=> x; rewrite /big_lexi_le /= /first_diff.
    by case: xgetP => //= -[n _|//] [m []]; rewrite eqxx.
    Qed.

    Lemma big_lexi_le_anti R : (forall n, 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 big_lexi_le_trans R :
      (forall n, transitive (R n)) ->
      (forall n, 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 big_lexi_le_total R : (forall n, 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 start_with n (t1 t2 : forall n, K n) (i : nat) : K i :=
      if (i < n)%O then t1 i else t2 i.

    Lemma start_with_prefix n x y : 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 {d} {K : nat -> porderType d}.

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

    Local Lemma big_lexi_ord_reflexive : reflexive (big_lexi_le Rn).
    Proof.
    exact: big_lexi_le_reflexive. Qed.

    Local Lemma big_lexi_ord_anti : antisymmetric (big_lexi_le Rn).
    Proof.
    by apply: big_lexi_le_anti => n; exact: le_anti. Qed.

    Local Lemma big_lexi_ord_trans : transitive (big_lexi_le Rn).
    Proof.
    by apply: big_lexi_le_trans => n; [exact: le_trans|exact: le_anti]. Qed.

    HB.instance Definition _ := Order.Le_isPOrder.Build d (big_lexi_order K)
      big_lexi_ord_reflexive big_lexi_ord_anti big_lexi_ord_trans.

    Lemma leEbig_lexi_order (a b : 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 {d} {K : nat -> orderType d}.

    Local Lemma big_lexi_ord_total : total (@Order.le _ (big_lexi_order K)).
    Proof.
    by apply: big_lexi_le_total => ?; exact: le_total. Qed.

    HB.instance Definition _ := Order.POrder_isTotal.Build _
      (big_lexi_order K) big_lexi_ord_total.

    End big_lexi_total.

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

    Let b : big_lexi_order K := (fun=> \bot)%O.
    Local Lemma big_lex_bot (x : big_lexi_order K) : (b <= x)%O.
    Proof.
    by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.le0x.
    Qed.

    HB.instance Definition _ := @Order.hasBottom.Build _
      (big_lexi_order K) b big_lex_bot.

    End big_lexi_bottom.

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

    Let t : big_lexi_order K := (fun=> \top)%O.
    Local Lemma big_lex_top (x : big_lexi_order K) : (x <= t)%O.
    Proof.
    by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.lex1.
    Qed.

    HB.instance Definition _ := @Order.hasTop.Build _
      (big_lexi_order K) t big_lex_top.

    End big_lexi_top.

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

    Lemma big_lexi_order_prefix_lt (b a x: big_lexi_order K) n :
      (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_prefix_gt (b a x : big_lexi_order K) n :
      (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_between (a x b : big_lexi_order K) n :
      (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 big_lexi_order_interval_prefix (i : interval (big_lexi_order K))
        (x : big_lexi_order K) :
      itv_open_ends i -> x \in i ->
      exists n, 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.
    Generated by a fork of coq2html