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 α] :=
(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 α
.
Order equipped with a sensible successor function.
- succ : α → α
Successor function
- le_succ : ∀ (a : α), a ≤ SuccOrder.succ a
Proof of basic ordering with respect to
succ
- max_of_succ_le : ∀ {a : α}, SuccOrder.succ a ≤ a → IsMax a
Proof of interaction between
succ
and maximal element - succ_le_of_lt : ∀ {a b : α}, a < b → SuccOrder.succ a ≤ b
Proof that
succ a
is the least element greater thana
Instances
Proof of basic ordering with respect to succ
Proof of interaction between succ
and maximal element
Proof that succ a
is the least element greater than a
Order equipped with a sensible predecessor function.
- pred : α → α
Predecessor function
- pred_le : ∀ (a : α), PredOrder.pred a ≤ a
Proof of basic ordering with respect to
pred
- min_of_le_pred : ∀ {a : α}, a ≤ PredOrder.pred a → IsMin a
Proof of interaction between
pred
and minimal element - le_pred_of_lt : ∀ {a b : α}, a < b → a ≤ PredOrder.pred b
Proof that
pred b
is the greatest element less thanb
Instances
Proof of basic ordering with respect to pred
Proof of interaction between pred
and minimal element
Proof that pred b
is the greatest element less than b
A constructor for SuccOrder α
usable when α
has no maximal element.
Equations
- SuccOrder.ofSuccLeIff succ hsucc_le_iff = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
Instances For
A constructor for PredOrder α
usable when α
has no minimal element.
Equations
- PredOrder.ofLePredIff pred hle_pred_iff = { pred := pred, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
Instances For
A constructor for SuccOrder α
for α
a linear order.
Equations
- SuccOrder.ofCore succ hn hm = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
Instances For
A constructor for PredOrder α
for α
a linear order.
Equations
- PredOrder.ofCore pred hn hm = { pred := pred, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
Instances For
A well-order is a SuccOrder
.
Equations
- SuccOrder.ofLinearWellFoundedLT α = SuccOrder.ofCore (fun (a : α) => if h : (Set.Ioi a).Nonempty then ⋯.min (Set.Ioi a) h else a) ⋯ ⋯
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
.
Equations
- ⋯ = ⋯
Predecessor order #
Alias of Order.le_pred_of_lt
.
Alias of the reverse direction of Order.le_pred_iff_isMin
.
Alias of the forward 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
.
Equations
- ⋯ = ⋯
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
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Adding a ⊥
to a NoMinOrder
#
Equations
- ⋯ = ⋯
SuccOrder
transfers across equivalences between orders.
Equations
- SuccOrder.ofOrderIso f = { succ := fun (y : Y) => f (SuccOrder.succ (f.symm y)), le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
Instances For
PredOrder
transfers across equivalences between orders.
Equations
- PredOrder.ofOrderIso f = { pred := fun (y : Y) => f (PredOrder.pred (f.symm y)), pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }