Successor and predecessor #
This file defines successor and predecessor orders. succ a
, the successor of an element a : α
is
the least element greater than a
. pred a
is the greatest element less than a
. Typical examples
include ℕ
, ℤ
, ℕ+
, Fin n
, but also ENat
, the lexicographic order of a successor/predecessor
order...
Typeclasses #
SuccOrder
: Order equipped with a sensible successor function.PredOrder
: Order equipped with a sensible predecessor function.
Implementation notes #
Maximal elements don't have a sensible successor. Thus the naïve typeclass
class NaiveSuccOrder (α : Type*) [Preorder α] where
(succ : α → α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
can't apply to an OrderTop
because plugging in a = b = ⊤
into either of succ_le_iff
and
lt_succ_iff
yields ⊤ < ⊤
(or more generally m < m
for a maximal element m
).
The solution taken here is to remove the implications ≤ → <
and instead require that a < succ a
for all non maximal elements (enforced by the combination of le_succ
and the contrapositive of
max_of_succ_le
).
The stricter condition of every element having a sensible successor can be obtained through the
combination of SuccOrder α
and NoMaxOrder α
.
A well-order is a SuccOrder
.
Equations
Instances For
A linear order with well-founded greater-than relation is a PredOrder
.
Equations
Instances For
Successor order #
Alias of Order.succ_le_of_lt
.
Alias of the forward direction of Order.succ_le_iff_isMax
.
Alias of the reverse direction of Order.succ_le_iff_isMax
.
Alias of the reverse direction of Order.lt_succ_iff_not_isMax
.
See also Order.succ_eq_of_covBy
.
Alias of Order.le_succ_of_wcovBy
.
See also Order.succ_eq_of_covBy
.
Alias of the reverse direction of Order.succ_eq_iff_isMax
.
See also Order.le_succ_of_wcovBy
.
Alias of Order.succ_eq_of_covBy
.
See also Order.le_succ_of_wcovBy
.
Alias of the forward direction of Order.succ_le_succ_iff
.
Alias of the forward direction of Order.succ_lt_succ_iff
.
Alias of the reverse direction of Order.succ_ne_succ_iff
.
There is at most one way to define the successors in a PartialOrder
.
Predecessor order #
Alias of Order.le_pred_of_lt
.
Alias of the forward direction of Order.le_pred_iff_isMin
.
Alias of the reverse direction of Order.le_pred_iff_isMin
.
Alias of the reverse direction of Order.pred_lt_iff_not_isMin
.
See also Order.pred_eq_of_covBy
.
Alias of Order.pred_le_of_wcovBy
.
See also Order.pred_eq_of_covBy
.
Alias of the reverse direction of Order.pred_eq_iff_isMin
.
See also Order.pred_le_of_wcovBy
.
Alias of Order.pred_eq_of_covBy
.
See also Order.pred_le_of_wcovBy
.
Alias of the forward direction of Order.pred_le_pred_iff
.
Alias of the forward direction of Order.pred_lt_pred_iff
.
Alias of the reverse direction of Order.pred_ne_pred_iff
.
There is at most one way to define the predecessors in a PartialOrder
.
Successor-predecessor orders #
WithBot
, WithTop
#
Adding a greatest/least element to a SuccOrder
or to a PredOrder
.
As far as successors and predecessors are concerned, there are four ways to add a bottom or top element to an order:
- Adding a
⊤
to anOrderTop
: Preservessucc
andpred
. - Adding a
⊤
to aNoMaxOrder
: Preservessucc
. Never preservespred
. - Adding a
⊥
to anOrderBot
: Preservessucc
andpred
. - Adding a
⊥
to aNoMinOrder
: Preservespred
. Never preservessucc
. where "preserves(succ/pred)
" means(Succ/Pred)Order α → (Succ/Pred)Order ((WithTop/WithBot) α)
.
Equations
Equations
Adding a ⊥
to a NoMinOrder
#
Equations
Alias of isMin_of_pred_notMem
.
Alias of pred_notMem_iff_isMin
.
Equations
Alias of isMax_of_succ_notMem
.
Alias of succ_notMem_iff_isMax
.