Library Combi.Basic.ordtype: Ordered Types

Ordered type

Inhabited Types:
  • inhType == interface for inhabited types
  • inhPordType == interface for partially ordered inhabited types
  • inhOrdType == interface for totally ordered inhabited types
  • inhOrdFinType == interface for totally ordered finite types
Sequence on a totally ordered type:
  • maxL a L == the maximum of a and the element of the sequence L
  • allLeq v a == a is smaller or equal than all the element of v
  • allLnt v a == a is strictly smaller than all the element of v
  • rembig w == w minus last occurence of its largest letter
  • posbig w == the position of the last occurence of the largest letter of w
  • shift_pos pos i == if i < pos then i else i.+1
  • shiftinv_pos pos i == if i < pos then i else i.-1
Cover relation:
  • covers x y == y covers x where x and y belongs to a common finPOrderType.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import order.
Require Import tools.

Set Implicit Arguments.

#[local] Open Scope order_scope.
Import Order.Theory.

Induction on partially ordered types


Lemma finord_wf (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
  (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.

Lemma finord_wf_down (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
  (forall x, (forall y, y > x -> P y) -> P x) -> forall x, P x.

Covering relation

We only define covering relation for finite type, since it cannot be decided and it is not very useful for infinite orders.
Definition covers {disp : unit} {T : finPOrderType disp} :=
  [rel x y : T | (x < y) && [forall z, ~~(x < z < y)]].

Section CoversFinPOrder.

Variable (disp : unit) (T : finPOrderType disp).
Implicit Type (x y : T).

Lemma coversP x y : reflect (x < y /\ (forall z, ~(x < z < y))) (covers x y).

Lemma ltcovers x y : covers x y -> x < y.

Lemma coversEV x y : covers x y -> forall z, x <= z <= y -> z = x \/ z = y.

Lemma covers_dual x y :
  covers (T := T^d) y x = covers x y.

Lemma covers_ind (P : T -> Type) :
  (forall x y, covers x y -> P x -> P y) ->
  forall x, P x -> forall y, x <= y -> P y.

Lemma covers_connect x y : (connect covers x y) = (x <= y).

Lemma covers_path x y :
  reflect (exists2 s, path covers x s & y = last x s) (x <= y).

End CoversFinPOrder.

Lemma covers_rind (disp : unit) (T : finPOrderType disp) (P : T -> Type) :
  (forall x y, covers y x -> P x -> P y) ->
  forall x, P x -> forall y, x >= y -> P y.

Inhabited types


#[short(type=inhType)]
HB.structure Definition Inhabited := {T of isInhabited T & Choice T}.




Definition inh {T : inhType} := xchoose (@inh_ex T).

Lemma inh_xchooseE (T : inhType) (exP : exists x0 : T, true) :
  xchoose exP = @inh T.

Lemma inh_chooseE (T : inhType) (x0 : T) :
  choose xpredT x0 = @inh T.

#[short(type=inhFinType)]
HB.structure Definition InhFinite := { T of isInhabited T & Finite T }.

Inhabited ordered types

#[short(type=inhPOrderType)]
HB.structure Definition InhPOrder (d : unit) :=
  {T of isInhabited T & Order.POrder d T}.

#[short(type=inhLatticeType)]
HB.structure Definition InhLattice (d : unit) :=
  {T of isInhabited T & Order.Lattice d T}.

#[short(type=inhTBLatticeType)]
HB.structure Definition InhTBLattice (d : unit) :=
  {T of isInhabited T & Order.TBLattice d T}.

#[short(type=inhOrderType)]
HB.structure Definition InhOrder (d : unit) :=
  {T of isInhabited T & Order.Total d T}.

Inhabited finite partially ordered types

#[short(type=inhFinPOrderType)]
HB.structure Definition InhFinPOrder (d : unit) :=
  {T of isInhabited T & Order.POrder d T & Finite T}.

#[short(type=inhFinLatticeType)]
HB.structure Definition InhFinLattice (d : unit) :=
  {T of isInhabited T & Order.FinLattice d T}.

#[short(type=inhFinOrderType)]
HB.structure Definition InhFinOrder (d : unit) :=
  {T of isInhabited T & Order.FinTotal d T}.


Section Dual.

Variable d : unit.


End Dual.

sequences over an ordered types

Maximum of a sequence

Section MaxSeq.

Variables (disp : unit) (T : orderType disp).
Implicit Type a b c : T.
Implicit Type u v : seq T.

Definition maxL a := foldl Order.max a.

Lemma maxLb a u : a <= maxL a u.

Lemma in_maxL a u : (maxL a u) \in a :: u.

Lemma maxXL a b u : Order.max a (maxL b u) = maxL (Order.max a b) u.

Lemma maxL_cat a u b v : maxL a (u ++ b :: v) = Order.max (maxL a u) (maxL b v).

End MaxSeq.

Comparison of the elements of a sequence to an element

Section AllLeqLtn.

Variables (disp : unit) (T : orderType disp).
Implicit Type a b c : T.
Implicit Type u v : seq T.

Definition allLeq v a := all (<= a) v.
Definition allLtn v a := all (< a) v.

Lemma allLtn_notin s b : allLeq s b -> b \notin s -> allLtn s b.

Lemma maxLPt a u : allLeq u (maxL a u).
Lemma maxLP a u : allLeq (a :: u) (maxL a u).

Lemma allLtnW v a : allLtn v a -> allLeq v a.

Lemma allLeqE u a : allLeq u a -> maxL a u = a.
Lemma allLeqP u a : reflect (maxL a u = a) (allLeq u a).

Lemma allLeqCons b u a : b <= a -> allLeq u a -> allLeq (b :: u) a.
Lemma allLtnCons b u a : b < a -> allLtn u a -> allLtn (b :: u) a.

Lemma allLeqConsE u a b : allLeq (b :: u) a = (maxL b u <= a).

Lemma allLtnConsE u a b : allLtn (b :: u) a = (maxL b u < a).

Lemma allLeq_consK b u a : allLeq (b :: u) a -> allLeq u a.
Lemma allLtn_consK b u a : allLtn (b :: u) a -> allLtn u a.

Lemma allLeq_catE u v a : allLeq (u ++ v) a = allLeq u a && allLeq v a.
Lemma allLtn_catE u v a : allLtn (u ++ v) a = allLtn u a && allLtn v a.

Lemma maxL_perm a u b v : perm_eq (a :: u) (b :: v) -> maxL a u = maxL b v.

Lemma perm_allLeq u v a : perm_eq u v -> allLeq u a -> allLeq v a.
Lemma perm_allLeqE u v a : perm_eq u v -> allLeq u a = allLeq v a.
Lemma perm_allLtn u v a : perm_eq u v -> allLtn u a -> allLtn v a.
Lemma perm_allLtnE u v a : perm_eq u v -> allLtn u a = allLtn v a.

Lemma allLeq_rev u a : allLeq (rev u) a = allLeq u a.
Lemma allLtn_rev u a : allLtn (rev u) a = allLtn u a.

Lemma allLeq_rconsK b u a : allLeq (rcons u b) a -> allLeq u a.
Lemma allLtn_rconsK b u a : allLtn (rcons u b) a -> allLtn u a.

Lemma allLeq_last b u a : allLeq (rcons u b) a -> b <= a.
Lemma allLtn_last b u a : allLtn (rcons u b) a -> b < a.

Lemma maxL_LbR a v L b R :
  a :: v = L ++ b :: R -> allLeq L b -> allLeq R b -> maxL a v = b.

End AllLeqLtn.

Removing the largest letter of a sequence

Section RemoveBig.

Variables (disp : unit) (T : orderType disp).
Variable Z : T.
Implicit Type a b c : T.
Implicit Type u v w r : seq T.

Remove the last occurence of the largest letter from w
Fixpoint rembig w :=
  if w is a :: v then
    if allLtn v a then v else a :: rembig v
  else [::].

Position of the last occurence of the largest letter of w
Fixpoint posbig w :=
  if w is a :: v then
    if allLtn v a then 0 else (posbig v).+1
  else 0.

Lemma size_rembig w : size (rembig w) = (size w).-1.

Lemma rembig_catR a u b v :
  maxL a u <= maxL b v -> rembig (a :: u ++ b :: v) = a :: u ++ rembig (b :: v).

Lemma rembig_catL a u b v :
  maxL a u > maxL b v -> rembig (a :: u ++ b :: v) = rembig (a :: u) ++ b :: v.

Lemma rembig_cat u v :
  rembig (u ++ v) = (rembig u) ++ v \/ rembig (u ++ v) = u ++ (rembig v).

Lemma rembig_eq_permL u1 u2 v :
  perm_eq u1 u2 ->
  (rembig (u1 ++ v) = (rembig u1) ++ v /\
   rembig (u2 ++ v) = (rembig u2) ++ v)
  \/
  (rembig (u1 ++ v) = u1 ++ (rembig v) /\
   rembig (u2 ++ v) = u2 ++ (rembig v)).

Lemma rembig_eq_permR u v1 v2 :
  perm_eq v1 v2 ->
  (rembig (u ++ v1) = (rembig u) ++ v1 /\
   rembig (u ++ v2) = (rembig u) ++ v2)
  \/
  (rembig (u ++ v1) = u ++ (rembig v1) /\
   rembig (u ++ v2) = u ++ (rembig v2)).

Lemma rembigP w wb : wb != [::] ->
  reflect
    (exists u b v, [/\ w = u ++ v, wb = u ++ b :: v, allLeq u b & allLtn v b])
    (w == rembig wb).

Lemma perm_rembig u v :
  perm_eq u v -> perm_eq (rembig u) (rembig v).

Lemma rembig_rev_uniq s : uniq s -> rev (rembig s) = rembig (rev s).

Lemma rembig_subseq s : subseq (rembig s) s.

Lemma rembig_uniq s : uniq s -> uniq (rembig s).

Open Scope nat_scope.

Lemma posbig_size_cons l s : posbig (l :: s) < size (l :: s).

Lemma posbig_size s : s != [::] -> posbig s < size s.

Lemma posbigE u b v :
  (allLeq u b && allLtn v b) = (posbig (u ++ b :: v) == size u).

Lemma posbig_take_dropE l s :
  take (posbig (l :: s)) (rembig (l :: s)) ++
     maxL l s
     :: drop (posbig (l :: s)) (rembig (l :: s)) = l :: s.

Lemma nth_posbig l s : nth Z (l :: s) (posbig (l :: s)) = maxL l s.

Lemma allLeq_posbig l s :
  allLeq (take (posbig (l :: s)) (l :: s)) (maxL l s).

Lemma allLtn_posbig l s :
  allLtn (drop (posbig (l :: s)).+1 (l :: s)) (maxL l s).

Lemma rembigE l s :
  take (posbig (l :: s)) (l :: s) ++
       drop (posbig (l :: s)).+1 (l :: s) = rembig (l :: s).

Lemma nth_lt_posbig i s : i < posbig s -> nth Z (rembig s) i = nth Z s i.

Definition shift_pos pos i := if i < pos then i else i.+1.
Definition shiftinv_pos pos i := if i < pos then i else i.-1.

Lemma shift_posK pos i : shiftinv_pos pos (shift_pos pos i) = i.

Lemma shiftinv_posK pos i : i != pos -> shift_pos pos (shiftinv_pos pos i) = i.

Lemma nth_rembig s i :
  nth Z s (shift_pos (posbig s) i) = nth Z (rembig s) i.

Lemma nth_inspos s pos i n :
  pos <= size s ->
  nth Z ((take pos s) ++ n :: (drop pos s)) i =
  if i == pos then n else nth Z s (shiftinv_pos pos i).

Lemma shift_pos_mono pos : {mono shift_pos pos : i j / i <= j}.

Lemma shiftinv_pos_homo pos : {homo shiftinv_pos pos : i j / i <= j}.

End RemoveBig.


Lemma maxL_iota n i : maxL i (iota i.+1 n) = i + n.

Lemma maxL_iota_n n : maxL 0%N (iota 1 n) = n.

Lemma rembig_iota n i : rembig (iota i n.+1) = iota i n.