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.IsSuccArchimedean
:SuccOrder
wheresucc
iterated to an element gives all the greater ones.IsPredArchimedean
:PredOrder
wherepred
iterated to an element gives all the smaller ones.
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)
→ α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
∀ {a b}, a < succ b ↔ a ≤ b)
↔ a ≤ b)
≤ 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 α
.
TODO #
Is GaloisConnection pred succ
always true? If not, we should introduce
class SuccPredOrder (α : Type _) [Preorder α] extends SuccOrder α, PredOrder α :=
(pred_succ_gc : GaloisConnection (pred : α → α) succ)
→ α) succ)
covby
should help here.
A constructor for SuccOrder α
usable when α
has no maximal element.
Equations
- One or more equations did not get rendered due to their size.
A constructor for PredOrder α
usable when α
has no minimal element.
Equations
- One or more equations did not get rendered due to their size.
A constructor for SuccOrder α
for α
a linear order.
Equations
- One or more equations did not get rendered due to their size.
A constructor for PredOrder α
for α
a linear order.
Equations
- One or more equations did not get rendered due to their size.
A constructor for SuccOrder α
usable when α
is a linear order with no maximal element.
Equations
- One or more equations did not get rendered due to their size.
A constructor for PredOrder α
usable when α
is a linear order with no minimal element.
Equations
- One or more equations did not get rendered due to their size.
Successor order #
Alias of the reverse direction of Order.lt_succ_iff_not_isMax
.
Alias of the forward direction of Order.succ_le_succ_iff
.
Alias of the reverse direction of Order.succ_lt_succ_iff
.
Alias of the forward direction of Order.succ_lt_succ_iff
.
Alias of the reverse direction of Order.succ_eq_iff_isMax
.
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 the reverse direction of Order.pred_lt_iff_not_isMin
.
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_lt_pred_iff
.
Alias of the reverse direction of Order.pred_eq_iff_isMin
.
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) α)→ (Succ/Pred)Order ((WithTop/WithBot) α)
.
Equations
- One or more equations did not get rendered due to their size.
Adding a ⊤⊤
to a NoMaxOrder
#
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Adding a ⊥⊥
to a NoMinOrder
#
Equations
- One or more equations did not get rendered due to their size.
Archimedeanness #
Induction principle on a type with a SuccOrder
for all elements above a given element m
.
Induction principle on a type with a PredOrder
for all elements below a given element m
.