Add_with_order

Theorems about addition, when order relation exists.

A ring-like has an order when the variable rngl_is_ordered is true.

See the module RingLike.Core for the general description of the ring-like library.

In general, it is not necessary to import the present module. The normal usage is to do:

    Require Import RingLike.Core.

which imports the present module and some other ones.

From Stdlib Require Import Utf8 Arith.
Require Import Structures.
Require Import Order.
Require Import Add.

Order Compatibility

This structure, order_compatibility, captures the key symmetry between the two order relations rngl_le (≤) and rngl_lt (<) in a ring-like structure.

# Core Idea

Duality: If l1 a b holds, then ¬ l2 b a.
Left Monotonicity: If a ≤ b and l2 b c then l2 a c.
Right Monotonicity: If l2 a b and b ≤ c then l2 a c.
Optional (requires additive inverses):
- l1 (a + b) c ↔ l1 b (c - a)
- l2 a (b + c) ↔ l2 (a - b) c

# Example

For l1 = rngl_le (≤) and l2 = rngl_lt (<), this recovers:

a + b ≤ c ↔ b ≤ c - a
a + b < c ↔ b < c - a

# Benefit

Capturing this compatibility reduces the need to duplicate proofs for ≤ and <, making reasoning in ordered ring-like structures more concise and systematic.

Class rngl_order_compatibility {T} {ro : ring_like_op T}
  (l1 l2 : T → T → Prop) :=
  { roc_dual_1 : ∀ a b, l1 a b ↔ ¬ l2 b a;
    roc_dual_2 : ∀ a b, l2 a b ↔ ¬ l1 b a;
    roc_of_lt : ∀ a b, (a < b)%L → l1 a b;
    roc_to_le : ∀ a b, l1 a b → (a ≤ b)%L;
    roc_mono_l : ∀ a b c, (a ≤ b)%L → l1 b c → l1 a c;
    roc_mono_r : ∀ a b c, l1 a b → (b ≤ c)%L → l1 a c;
    roc_opt_add_ord_compat :
      if rngl_has_opp_or_psub T then
        ∀ a b c, l1 b c ↔ (l1 (a + b) (a + c))%L
      else not_applicable }.

Theorem roc_add_ord_compat {T} {ro : ring_like_op T} {l1 l2}
  {Hroc : rngl_order_compatibility l1 l2} :
  rngl_has_opp_or_psub T = true →
  ∀ a b c, l1 b c ↔ (l1 (a + b) (a + c))%L.

Arguments roc_add_ord_compat {T ro l1 l2 Hroc} Hop (a b c)%_L.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Tactic Notation "pauto" := progress auto.
Hint Resolve rngl_le_refl : core.

Theorem rngl_order_compatibility_comm :
  rngl_is_ordered T = true →
  ∀ l1 l2, rngl_order_compatibility l1 l2 → rngl_order_compatibility l2 l1.
Theorem rngl_add_le_mono_l :
  rngl_is_ordered T = true →
  ∀ a b c, (b ≤ c ↔ a + b ≤ a + c)%L.

Theorem rngl_add_lt_mono_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (b < c ↔ a + b < a + c)%L.
Theorem rngl_add_le_mono :
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b → c ≤ d → a + c ≤ b + d)%L.

rngl_order_compatibility works for pair (≤, <)

Theorem rngl_le_lt_comp :
rngl_is_ordered T = true →
rngl_order_compatibility rngl_le rngl_lt.

rngl_order_compatibility works for pair (<, ≤)

Theorem rngl_lt_le_comp :
rngl_is_ordered T = true →
rngl_order_compatibility rngl_lt rngl_le.

generic theorems: work for pair (≤, <) and for pair (<, ≤)

specific theorems: version for ≤, followed with version for <

Theorem rngl_add_le_mono_r :
  rngl_is_ordered T = true →
  ∀ a b c, (a ≤ b ↔ a + c ≤ b + c)%L.
Theorem rngl_add_lt_mono_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a < b ↔ a + c < b + c)%L.

Theorem rngl_le_0_sub :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 ≤ b - a ↔ a ≤ b)%L.

Theorem rngl_lt_0_sub :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < b - a ↔ a < b)%L.

Theorem rngl_le_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a - b ≤ 0 ↔ a ≤ b)%L.

Theorem rngl_lt_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a - b < 0 ↔ a < b)%L.

Theorem rngl_opp_le_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ b ↔ - b ≤ - a)%L.

Theorem rngl_opp_lt_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < b ↔ - b < - a)%L.

Theorem rngl_opp_nonneg_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ - a)%L ↔ (a ≤ 0)%L.

Theorem rngl_opp_pos_neg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < - a)%L ↔ (a < 0)%L.

Theorem rngl_opp_nonpos_nonneg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (- a ≤ 0)%L ↔ (0 ≤ a)%L.

Theorem rngl_opp_neg_pos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (- a < 0 ↔ 0 < a)%L.

Theorem rngl_sub_le_mono_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a ≤ b)%L ↔ (c - b ≤ c - a)%L.

Theorem rngl_sub_lt_mono_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a < b)%L ↔ (c - b < c - a)%L.

Theorem rngl_sub_le_mono_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a ≤ b ↔ a - c ≤ b - c)%L.

Theorem rngl_sub_lt_mono_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c : T, (a < b)%L ↔ (a - c < b - c)%L.

Theorem rngl_le_add_le_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b ≤ c ↔ b ≤ c - a)%L.

Theorem rngl_lt_add_lt_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b < c ↔ b < c - a)%L.

Theorem rngl_le_add_le_sub_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b ≤ c ↔ a ≤ c - b)%L.

Theorem rngl_lt_add_lt_sub_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a + b < c ↔ a < c - b)%L.

Theorem rngl_le_sub_le_add_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b ≤ c ↔ a ≤ b + c)%L.

Theorem rngl_lt_sub_lt_add_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b < c ↔ a < b + c)%L.

Theorem rngl_le_sub_le_add_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b ≤ c ↔ a ≤ c + b)%L.

Theorem rngl_lt_sub_lt_add_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c, (a - b < c ↔ a < c + b)%L.

Theorem rngl_add_le_lt_mono :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b)%L → (c < d)%L → (a + c < b + d)%L.

Theorem rngl_add_lt_le_mono :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b)%L → (c ≤ d)%L → (a + c < b + d)%L.

Theorem rngl_le_add_l :
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → b ≤ a + b)%L.

Theorem rngl_lt_add_l :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a)%L → (b < a + b)%L.

Theorem rngl_le_add_r :
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ b → a ≤ a + b)%L.

Theorem rngl_lt_add_r :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < b → a < a + b)%L.

Theorem rngl_sub_le_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a ≤ b → c ≤ d → a - d ≤ b - c)%L.

Theorem rngl_sub_lt_compat :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b → c < d → a - d < b - c)%L.

Theorem rngl_le_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ b ↔ a - b ≤ a)%L.

Theorem rngl_lt_sub_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < b ↔ a - b < a)%L.

Theorem rngl_le_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (- a ≤ b ↔ 0 ≤ a + b)%L.

Theorem rngl_lt_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (- a < b ↔ 0 < a + b)%L.

Theorem rngl_le_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ - b ↔ a + b ≤ 0)%L.

Theorem rngl_lt_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < - b ↔ a + b < 0)%L.

Theorem rngl_le_0_add :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → 0 ≤ a + b)%L.

Theorem rngl_lt_0_add' :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < a)%L → (0 ≤ b)%L → (0 < a + b)%L.

Theorem rngl_lt_0_add :
  rngl_is_ordered T = true →
  ∀ a b, (0 < a)%L → (0 ≤ b)%L → (0 < a + b)%L.

other theorems

Theorem rngl_add_lt_compat :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a b c d, (a < b → c < d → a + c < b + d)%L.

Theorem rngl_leb_sub_0 :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, ((a - b ≤? 0) = (a ≤? b ))%L.

Theorem rngl_eq_add_0 :
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a → 0 ≤ b → a + b = 0 → a = 0 ∧ b = 0)%L.
Theorem rngl_mul_nat_inj_le :
  rngl_is_ordered T = true →
  ∀ a, (0 < a)%L → ∀ i j, i ≤ j ↔ (rngl_mul_nat a i ≤ rngl_mul_nat a j)%L.
Theorem rngl_mul_nat_inj_lt :
  rngl_has_opp_or_psub T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 < a)%L → ∀ i j, i < j ↔ (rngl_mul_nat a i < rngl_mul_nat a j)%L.
Theorem rngl_add_nonneg_pos :
  rngl_is_ordered T = true →
  ∀ a b, (0 ≤ a)%L → (0 < b)%L → (0 < a + b)%L.

Theorem rngl_add_nonpos_nonpos :
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ 0 → b ≤ 0 → a + b ≤ 0)%L.

Theorem rngl_add_neg_nonpos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a < 0 → b ≤ 0 → a + b < 0)%L.

Theorem rngl_add_nonpos_neg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤ 0 → b < 0 → a + b < 0)%L.

Theorem rngl_abs_nonneg :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ rngl_abs a)%L.
Theorem rngl_abs_opp :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, rngl_abs (- a)%L = rngl_abs a.
Theorem rngl_le_abs_diag :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (a ≤ rngl_abs a)%L.

Theorem rngl_abs_nonneg_eq :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤ a)%L → rngl_abs a = a.

Theorem rngl_abs_nonpos_eq :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a : T, (a ≤ 0)%L → rngl_abs a = (- a)%L.

Theorem rngl_abs_le :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ x y, (- x ≤ y ≤ x ↔ rngl_abs y ≤ x)%L.
Theorem rngl_le_abs :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ x y, (x ≤ y ∨ x ≤ -y)%L ↔ (x ≤ rngl_abs y)%L.

Theorem rngl_abs_lt :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ x y, (- x < y < x ↔ rngl_abs y < x)%L.
Theorem rngl_abs_sub_comm :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, rngl_abs (a - b)%L = rngl_abs (b - a)%L.

Theorem rngl_abs_pos :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ x, (x ≠ 0 → 0 < rngl_abs x)%L.

Theorem rngl_abs_triangle :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (rngl_abs (a + b) ≤ rngl_abs a + rngl_abs b)%L.

Theorem rngl_leb_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (-a ≤? b)%L = (-b ≤? a)%L.
Theorem rngl_leb_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a ≤? -b)%L = (b ≤? -a)%L.
Theorem rngl_leb_0_opp :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a, (0 ≤? - a)%L = (a ≤? 0)%L.

Theorem rngl_ltb_opp_l :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (-a <? b)%L = (-b <? a)%L.
Theorem rngl_ltb_opp_r :
  rngl_has_opp T = true →
  rngl_is_ordered T = true →
  ∀ a b, (a <? -b)%L = (b <? -a)%L.
Theorem rngl_archimedean_ub :
  rngl_is_archimedean T = true →
  rngl_is_ordered T = true →
  ∀ a b : T, (0 < a < b)%L →
  ∃ₜ n : nat , (rngl_mul_nat a n ≤ b < rngl_mul_nat a (n + 1))%L.

Theorem rngl_archimedean :
  rngl_is_archimedean T = true →
  rngl_is_ordered T = true →
  ∀ a b, (0 < a)%L → ∃ₜ n , (b < rngl_mul_nat a n)%L.

End a.

Arguments rngl_abs_nonneg_eq {T ro rp} Hop Hor a%_L.
Arguments rngl_add_le_mono_l {T ro rp} Hor (a b c)%_L.
Arguments rngl_add_lt_mono_l {T ro rp} Hop Hor (a b c)%_L.
Arguments rngl_le_add_r {T ro rp} Hor (a b)%_L.

This page has been generated by coqdoc