Interaction between successors and arithmetic #
We define the SuccAddOrder
and PredSubOrder
typeclasses, for orders satisfying succ x = x + 1
and pred x = x - 1
respectively. This allows us to transfer the API for successors and
predecessors into these common arithmetical forms.
Todo #
In the future, we will make x + 1
and x - 1
the simp
-normal forms for succ x
and pred x
respectively. This will require a refactor of Ordinal
first, as the simp
-normal form is
currently set the other way around.
A typeclass for succ x = x + 1
.
- succ : α → α
- le_succ : ∀ (a : α), a ≤ SuccOrder.succ a
- max_of_succ_le : ∀ {a : α}, SuccOrder.succ a ≤ a → IsMax a
- succ_le_of_lt : ∀ {a b : α}, a < b → SuccOrder.succ a ≤ b
- succ_eq_add_one : ∀ (x : α), SuccOrder.succ x = x + 1
Instances
theorem
SuccAddOrder.succ_eq_add_one
{α : Type u_1}
:
∀ {inst : Preorder α} {inst_1 : Add α} {inst_2 : One α} [self : SuccAddOrder α] (x : α), SuccOrder.succ x = x + 1
A typeclass for pred x = x - 1
.
- pred : α → α
- pred_le : ∀ (a : α), PredOrder.pred a ≤ a
- min_of_le_pred : ∀ {a : α}, a ≤ PredOrder.pred a → IsMin a
- le_pred_of_lt : ∀ {a b : α}, a < b → a ≤ PredOrder.pred b
- pred_eq_sub_one : ∀ (x : α), PredOrder.pred x = x - 1
Instances
theorem
PredSubOrder.pred_eq_sub_one
{α : Type u_1}
:
∀ {inst : Preorder α} {inst_1 : Sub α} {inst_2 : One α} [self : PredSubOrder α] (x : α), PredOrder.pred x = x - 1
theorem
Order.succ_eq_add_one
{α : Type u_1}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
(x : α)
:
Order.succ x = x + 1
theorem
Order.add_one_le_of_lt
{α : Type u_1}
{x : α}
{y : α}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
(h : x < y)
:
theorem
Order.add_one_le_iff
{α : Type u_1}
{x : α}
{y : α}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
@[simp]
@[simp]
theorem
Order.covBy_add_one
{α : Type u_1}
[Preorder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
(x : α)
:
theorem
Order.pred_eq_sub_one
{α : Type u_1}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
(x : α)
:
Order.pred x = x - 1
theorem
Order.le_sub_one_of_lt
{α : Type u_1}
{x : α}
{y : α}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
(h : x < y)
:
theorem
Order.le_sub_one_iff
{α : Type u_1}
{x : α}
{y : α}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
@[simp]
@[simp]
theorem
Order.sub_one_covBy
{α : Type u_1}
[Preorder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
(x : α)
:
@[simp]
theorem
Order.succ_iterate
{α : Type u_1}
[Preorder α]
[AddMonoidWithOne α]
[SuccAddOrder α]
(x : α)
(n : ℕ)
:
@[simp]
theorem
Order.pred_iterate
{α : Type u_1}
[Preorder α]
[AddCommGroupWithOne α]
[PredSubOrder α]
(x : α)
(n : ℕ)
:
theorem
Order.not_isMax_zero
{α : Type u_1}
[PartialOrder α]
[Zero α]
[One α]
[ZeroLEOneClass α]
[NeZero 1]
:
theorem
Order.one_le_iff_pos
{α : Type u_1}
{x : α}
[PartialOrder α]
[AddMonoidWithOne α]
[ZeroLEOneClass α]
[NeZero 1]
[SuccAddOrder α]
:
theorem
Order.covBy_iff_add_one_eq
{α : Type u_1}
{x : α}
{y : α}
[PartialOrder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
theorem
Order.covBy_iff_sub_one_eq
{α : Type u_1}
{x : α}
{y : α}
[PartialOrder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
theorem
Order.le_of_lt_add_one
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Add α]
[One α]
[SuccAddOrder α]
(h : x < y + 1)
:
x ≤ y
theorem
Order.lt_add_one_iff_of_not_isMax
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Add α]
[One α]
[SuccAddOrder α]
(hy : ¬IsMax y)
:
theorem
Order.lt_add_one_iff
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Add α]
[One α]
[SuccAddOrder α]
[NoMaxOrder α]
:
theorem
Order.le_of_sub_one_lt
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Sub α]
[One α]
[PredSubOrder α]
(h : x - 1 < y)
:
x ≤ y
theorem
Order.sub_one_lt_iff_of_not_isMin
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Sub α]
[One α]
[PredSubOrder α]
(hx : ¬IsMin x)
:
theorem
Order.sub_one_lt_iff
{α : Type u_1}
{x : α}
{y : α}
[LinearOrder α]
[Sub α]
[One α]
[PredSubOrder α]
[NoMinOrder α]
:
theorem
Order.lt_one_iff_nonpos
{α : Type u_1}
{x : α}
[LinearOrder α]
[AddMonoidWithOne α]
[ZeroLEOneClass α]
[NeZero 1]
[SuccAddOrder α]
: