The positive, negative, nonnegative and nonpositive integers

Content created by Fredrik Bakke and malarbol.

Created on 2024-03-28.
Last modified on 2024-04-09.

module elementary-number-theory.positive-and-negative-integers where
Imports 
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.negative-integers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.nonpositive-integers
open import elementary-number-theory.nonzero-integers
open import elementary-number-theory.positive-integers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.negated-equality
open import foundation.negation
open import foundation.unit-type

Idea

In this file, we outline basic relations between negative, nonpositive, nonnegative, and positive integers.

Properties

The only nonnegative and nonpositive integer is zero

is-zero-is-nonnegative-is-nonpositive-ℤ :
  {x : ℤ} → is-nonnegative-ℤ x → is-nonpositive-ℤ x → is-zero-ℤ x
is-zero-is-nonnegative-is-nonpositive-ℤ {inr (inl x)} H K = refl

No integer is both positive and negative

is-not-negative-and-positive-ℤ : (x : ℤ) → ¬ (is-negative-ℤ x × is-positive-ℤ x)
is-not-negative-and-positive-ℤ (inl x) (H , K) = K
is-not-negative-and-positive-ℤ (inr x) (H , K) = H

Dichotomies

A nonzero integer is either negative or positive

decide-sign-nonzero-ℤ :
  {x : ℤ} → x ≠ zero-ℤ → is-negative-ℤ x + is-positive-ℤ x
decide-sign-nonzero-ℤ {inl x} H = inl star
decide-sign-nonzero-ℤ {inr (inl x)} H = ex-falso (H refl)
decide-sign-nonzero-ℤ {inr (inr x)} H = inr star

An integer is either positive or nonpositive

decide-is-positive-is-nonpositive-ℤ :
  {x : ℤ} → is-positive-ℤ x + is-nonpositive-ℤ x
decide-is-positive-is-nonpositive-ℤ {inl x} = inr star
decide-is-positive-is-nonpositive-ℤ {inr (inl x)} = inr star
decide-is-positive-is-nonpositive-ℤ {inr (inr x)} = inl star

An integer is either negative or nonnegative

decide-is-negative-is-nonnegative-ℤ :
  {x : ℤ} → is-negative-ℤ x + is-nonnegative-ℤ x
decide-is-negative-is-nonnegative-ℤ {inl x} = inl star
decide-is-negative-is-nonnegative-ℤ {inr x} = inr star

An integer or its negative is nonnegative

decide-is-nonnegative-is-nonnegative-neg-ℤ :
  {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x))
decide-is-nonnegative-is-nonnegative-neg-ℤ {inl x} = inr star
decide-is-nonnegative-is-nonnegative-neg-ℤ {inr x} = inl star

An integer or its negative is nonpositive

decide-is-nonpositive-is-nonpositive-neg-ℤ :
  {x : ℤ} → (is-nonpositive-ℤ x) + (is-nonpositive-ℤ (neg-ℤ x))
decide-is-nonpositive-is-nonpositive-neg-ℤ {inl x} = inl star
decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inl x)} = inl star
decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inr x)} = inr star

Positive integers are nonnegative

is-nonnegative-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ x
is-nonnegative-is-positive-ℤ {inr (inr x)} H = H

nonnegative-positive-ℤ : positive-ℤ → nonnegative-ℤ
nonnegative-positive-ℤ (x , H) = (x , is-nonnegative-is-positive-ℤ H)

Negative integers are nonpositive

is-nonpositive-is-negative-ℤ : {x : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ x
is-nonpositive-is-negative-ℤ {inl x} H = H

nonpositive-negative-ℤ : negative-ℤ → nonpositive-ℤ
nonpositive-negative-ℤ (x , H) = (x , is-nonpositive-is-negative-ℤ H)

Determining the sign of the successor of an integer

The successor of a nonnegative integer is positive

is-positive-succ-is-nonnegative-ℤ :
  {x : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ (succ-ℤ x)
is-positive-succ-is-nonnegative-ℤ {inr (inl x)} H = H
is-positive-succ-is-nonnegative-ℤ {inr (inr x)} H = H

The successor of a negative integer is nonpositive

is-nonpositive-succ-is-negative-ℤ :
  {x : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ (succ-ℤ x)
is-nonpositive-succ-is-negative-ℤ {inl zero-ℕ} H = H
is-nonpositive-succ-is-negative-ℤ {inl (succ-ℕ x)} H = H

Determining the sign of the predecessor of an integer

The predecessor of a positive integer is nonnegative

is-nonnegative-pred-is-positive-ℤ :
  {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ (pred-ℤ x)
is-nonnegative-pred-is-positive-ℤ {inr (inr zero-ℕ)} H = H
is-nonnegative-pred-is-positive-ℤ {inr (inr (succ-ℕ x))} H = H

The predecessor of a nonpositive integer is negative

is-negative-pred-is-nonpositive-ℤ :
  {x : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ (pred-ℤ x)
is-negative-pred-is-nonpositive-ℤ {inl x} H = H
is-negative-pred-is-nonpositive-ℤ {inr (inl x)} H = H

Determining the sign of the negative of an integer

The negative of a nonnegative integer is nonpositive

is-nonpositive-neg-is-nonnegative-ℤ :
  {x : ℤ} → is-nonnegative-ℤ x → is-nonpositive-ℤ (neg-ℤ x)
is-nonpositive-neg-is-nonnegative-ℤ {inr (inl x)} H = H
is-nonpositive-neg-is-nonnegative-ℤ {inr (inr x)} H = H

neg-nonnegative-ℤ : nonnegative-ℤ → nonpositive-ℤ
neg-nonnegative-ℤ (x , H) = neg-ℤ x , is-nonpositive-neg-is-nonnegative-ℤ H

The negative of a nonpositive integer is nonnegative

is-nonnegative-neg-is-nonpositive-ℤ :
  {x : ℤ} → is-nonpositive-ℤ x → is-nonnegative-ℤ (neg-ℤ x)
is-nonnegative-neg-is-nonpositive-ℤ {inl x} H = H
is-nonnegative-neg-is-nonpositive-ℤ {inr (inl x)} H = H

neg-nonpositive-ℤ : nonpositive-ℤ → nonnegative-ℤ
neg-nonpositive-ℤ (x , H) = neg-ℤ x , is-nonnegative-neg-is-nonpositive-ℤ H

The negative of a positive integer is negative

is-negative-neg-is-positive-ℤ :
  {x : ℤ} → is-positive-ℤ x → is-negative-ℤ (neg-ℤ x)
is-negative-neg-is-positive-ℤ {inr (inr x)} H = H

neg-positive-ℤ : positive-ℤ → negative-ℤ
neg-positive-ℤ (x , H) = (neg-ℤ x , is-negative-neg-is-positive-ℤ H)

The negative of a negative integer is positive

is-positive-neg-is-negative-ℤ :
  {x : ℤ} → is-negative-ℤ x → is-positive-ℤ (neg-ℤ x)
is-positive-neg-is-negative-ℤ {inl x} H = H

neg-negative-ℤ : negative-ℤ → positive-ℤ
neg-negative-ℤ (x , H) = (neg-ℤ x , is-positive-neg-is-negative-ℤ H)

Negated properties

Nonpositivity is negated positivity

is-not-positive-is-nonpositive-ℤ :
  {x : ℤ} → is-nonpositive-ℤ x → ¬ (is-positive-ℤ x)
is-not-positive-is-nonpositive-ℤ {inr (inl x)} _ q = q
is-not-positive-is-nonpositive-ℤ {inr (inr x)} p _ = p

is-nonpositive-is-not-positive-ℤ :
  {x : ℤ} → ¬ (is-positive-ℤ x) → is-nonpositive-ℤ x
is-nonpositive-is-not-positive-ℤ {x} H =
  rec-coproduct
    ( λ K → ex-falso (H K))
    ( id)
    ( decide-is-positive-is-nonpositive-ℤ)

Nonnegativity is negated negativity

is-not-negative-is-nonnegative-ℤ :
  {x : ℤ} → is-nonnegative-ℤ x → ¬ (is-negative-ℤ x)
is-not-negative-is-nonnegative-ℤ {x} H K =
  is-not-positive-is-nonpositive-ℤ
    ( is-nonpositive-neg-is-nonnegative-ℤ H)
    ( is-positive-neg-is-negative-ℤ K)

is-nonnegative-is-not-negative-ℤ :
  {x : ℤ} → ¬ (is-negative-ℤ x) → is-nonnegative-ℤ x
is-nonnegative-is-not-negative-ℤ {x} H =
  rec-coproduct
    ( λ K → ex-falso (H K))
    ( id)
    ( decide-is-negative-is-nonnegative-ℤ)

Recent changes