Order

Theorems about order relation of the ring-like library.

Generally applied in ordered ring-like structures which can be recognizable by

  rngl_is_ordered T = true

but sometimes work even without this hypothesis.

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

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

    Require Import RingLike.Core.

which imports the present module and some other ones.

Require Import Stdlib.Arith.Arith.
Require Import Utf8.
Require Import Structures.

Section a.

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

Definition rngl_eqb_dec a b := sumbool_of_bool (a =? b)%L.
Definition rngl_leb_dec a b := sumbool_of_bool (a ≤? b)%L.
Definition rngl_ltb_dec a b := sumbool_of_bool (a <? b)%L.

Theorem rngl_leb_le :
  ∀ a b , (a ≤? b)%L = true ↔ (a ≤ b)%L.

Theorem rngl_leb_nle :
  ∀ a b , (a ≤? b)%L = false ↔ ¬ (a ≤ b)%L.
Theorem rngl_ltb_lt :
  rngl_has_eq_dec_or_order T = true →
  ∀ a b , (a <? b)%L = true ↔ (a < b)%L.
Theorem rngl_ltb_nlt :
  rngl_has_eq_dec_or_order T = true →
  ∀ a b , (a <? b)%L = false ↔ ¬ (a < b)%L.
Theorem rngl_le_refl :
  rngl_is_ordered T = true →
  ∀ a , (a ≤ a)%L.

Theorem rngl_leb_refl :
  rngl_is_ordered T = true →
  ∀ a , (a ≤? a)%L = true.

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

Theorem rngl_le_neq : ∀ a b , (a < b ↔ a ≤ b ∧ a ≠ b)%L.

Theorem rngl_lt_le_incl : ∀ a b , (a < b → a ≤ b)%L.

Theorem rngl_lt_asymm :
  rngl_is_ordered T = true →
  ∀ a b , (a < b → ¬ b < a)%L.

Theorem rngl_nle_gt :
  rngl_is_ordered T = true →
  ∀ a b , (b < a → ¬ (a ≤ b ))%L.

Theorem rngl_leb_gt :
  rngl_is_ordered T = true →
  ∀ a b , (b < a →(a ≤? b ) = false)%L.

Theorem rngl_le_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T , (a ≤ b)%L → (b ≤ c)%L → (a ≤ c)%L.

Theorem rngl_lt_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T , (a < b)%L → (b < c)%L → (a < c)%L.
Theorem rngl_lt_le_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T , (a < b)%L → (b ≤ c)%L → (a < c)%L.
Theorem rngl_le_lt_trans :
  rngl_is_ordered T = true →
   ∀ a b c : T , (a ≤ b)%L → (b < c)%L → (a < c)%L.
Theorem rngl_le_iff_leb_eq :
  ∀ a b c d ,
  (a ≤ b ↔ c ≤ d)%L
  → ((a ≤? b ) = (c ≤? d ))%L.
Theorem rngl_lt_eq_cases :
  rngl_is_ordered T = true →
  ∀ a b : T , (a ≤ b)%L ↔ (a < b)%L ∨ a = b.
Theorem rngl_lt_irrefl : ∀ a : T , ¬ (a < a)%L.

Theorem rngl_nlt_ge :
  rngl_is_ordered T = true →
  ∀ a b , (b ≤ a → ¬ (a < b ))%L.

Theorem rngl_ltb_ge :
  rngl_is_ordered T = true →
  ∀ a b , (b ≤ a → (a <? b ) = false)%L.

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

Theorem rngl_min_id :
  rngl_is_ordered T = true →
  ∀ a , rngl_min a a = a.

Theorem rngl_max_id :
  rngl_is_ordered T = true →
  ∀ a , rngl_max a a = a.

Theorem rngl_min_l_iff :
  rngl_is_ordered T = true →
  ∀ a b , rngl_min a b = a ↔ (a ≤ b)%L.
Theorem rngl_le_min_r :
  rngl_is_ordered T = true →
  ∀ a b , (rngl_min a b ≤ b)%L.

Theorem rngl_le_max_l :
  rngl_is_ordered T = true →
  ∀ a b , (a ≤ rngl_max a b)%L.

Theorem rngl_min_glb :
  ∀ a b c , (a ≤ b → a ≤ c → a ≤ rngl_min b c)%L.

Theorem rngl_min_glb_lt :
  ∀ a b c , (a < b → a < c → a < rngl_min b c)%L.

Theorem rngl_max_lub :
  ∀ a b c , (a ≤ c → b ≤ c → rngl_max a b ≤ c)%L.

Theorem rngl_max_lub_lt :
  ∀ a b c , (a < c → b < c → rngl_max a b < c)%L.

Definition rngl_compare a b :=
  if (a =? b)%L then Eq
  else if (a ≤? b)%L then Lt else Gt.

Theorem rngl_compare_eq_iff :
  rngl_has_eq_dec_or_order T = true →
  ∀ a b , rngl_compare a b = Eq ↔ a = b.
Theorem rngl_compare_refl :
  rngl_has_eq_dec_or_order T = true →
  ∀ a , rngl_compare a a = Eq.

Theorem rngl_is_totally_ordered_is_ordered :
  rngl_is_totally_ordered T = true → rngl_is_ordered T = true.

Theorem rngl_leb_neg_ltb :
  rngl_is_totally_ordered T = true →
  ∀ a b , (a ≤? b = negb (b <? a))%L.

Theorem rngl_ltb_neg_leb :
  rngl_is_totally_ordered T = true →
  ∀ a b , (a <? b = negb (b ≤? a))%L.

Theorem rngl_not_le :
  rngl_is_totally_ordered T = true →
  ∀ a b , (¬ a ≤ b → a ≠ b ∧ b ≤ a)%L.

Theorem rngl_nle_gt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , (¬ (a ≤ b ) ↔ b < a)%L.

Theorem rngl_nlt_ge_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , (¬ (a < b ) ↔ b ≤ a)%L.

Theorem rngl_leb_gt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , ((a ≤? b ) = false ↔ b < a)%L.

Theorem rngl_ltb_ge_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , ((a <? b ) = false ↔ b ≤ a)%L.

Theorem rngl_min_comm :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_min a b = rngl_min b a.
Theorem rngl_max_comm :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_max a b = rngl_max b a.

Theorem rngl_min_assoc :
  rngl_is_totally_ordered T = true →
  ∀ a b c ,
  rngl_min a (rngl_min b c) = rngl_min (rngl_min a b) c.

Theorem rngl_max_assoc :
  rngl_is_totally_ordered T = true →
  ∀ a b c ,
  rngl_max a (rngl_max b c) = rngl_max (rngl_max a b) c.

Theorem rngl_min_r_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_min a b = b ↔ (b ≤ a)%L.

Theorem rngl_max_l_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_max a b = a ↔ (b ≤ a)%L.
Theorem rngl_max_r_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_max a b = b ↔ (a ≤ b)%L.

Theorem rngl_min_glb_lt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b c , (c < rngl_min a b ↔ c < a ∧ c < b)%L.

Theorem rngl_min_le_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b c , (rngl_min a b ≤ c ↔ a ≤ c ∨ b ≤ c)%L.

Theorem rngl_min_lt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b c , (rngl_min a b < c ↔ a < c ∨ b < c)%L.

Theorem rngl_max_lt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b c , (a < rngl_max b c ↔ a < b ∨ a < c)%L.
Theorem rngl_le_min_l :
  rngl_is_totally_ordered T = true →
  ∀ a b , (rngl_min a b ≤ a)%L.

Theorem rngl_min_le_compat_l :
  rngl_is_totally_ordered T = true →
  ∀ a b c , (b ≤ c → rngl_min a b ≤ rngl_min a c)%L.
Theorem rngl_le_max_r :
  rngl_is_totally_ordered T = true →
  ∀ a b , (b ≤ rngl_max a b)%L.

Theorem rngl_compare_lt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_compare a b = Lt ↔ (a < b)%L.
Theorem rngl_compare_gt_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_compare a b = Gt ↔ (b < a)%L.
Theorem rngl_compare_le_iff :
  rngl_is_totally_ordered T = true →
  ∀ a b , rngl_compare a b ≠ Gt ↔ (a ≤ b)%L.
Definition rngl_signp x := (if 0 ≤? x then 1 else -1)%L.
Definition rngl_sign x := (if x =? 0 then 0 else rngl_signp x)%L.

Theorem rngl_signp_of_pos : ∀ x , (0 ≤ x → rngl_signp x = 1)%L.

Theorem rngl_signp_of_neg :
  rngl_is_ordered T = true →
  ∀ x , (x < 0 → rngl_signp x = -1)%L.

Theorem rngl_sign_of_pos :
  rngl_has_eq_dec_or_order T = true →
  ∀ x , (0 < x → rngl_sign x = 1)%L.

Theorem rngl_sign_of_neg :
  rngl_is_ordered T = true →
  ∀ x , (x < 0 → rngl_sign x = -1)%L.

End a.

Notation "x ?= y" := (rngl_compare x y) : ring_like_scope.

Arguments rngl_compare {T ro} (a b)%_L.
Arguments rngl_eqb_dec {T ro} (a b)%_L.
Arguments rngl_le_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_le_lt_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_leb_dec {T ro} (a b)%_L.
Arguments rngl_lt_le_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_lt_trans {T ro rp} Hor (a b c)%_L.
Arguments rngl_ltb_dec {T ro} (a b)%_L.
Arguments rngl_min {T ro} (a b)%_L.
Arguments rngl_max {T ro} (a b)%_L.
Arguments rngl_signp {T ro} x%_L.
Arguments rngl_sign {T ro} x%_L.

This page has been generated by coqdoc