Skip to content

Rationals.Negation

Andrew Sneap, January-March 2021

In this file I define negation of real numbers.


{-# OPTIONS --safe --without-K --lossy-unification #-}

open import MLTT.Spartan renaming (_+_ to _βˆ”_)

open import Integers.Type
open import Integers.Multiplication renaming (_*_ to _β„€*_)
open import Integers.Negation renaming (-_ to β„€-_)
open import Rationals.Fractions
open import Rationals.FractionsOperations renaming (-_ to 𝔽-_ ; _+_ to _𝔽+_ ; _*_ to _𝔽*_)
open import Rationals.Type
open import Rationals.Addition
open import Rationals.Multiplication

module Rationals.Negation where

-_ : β„š β†’ β„š
- ((x , a) , p) = toβ„š (𝔽- (x , a))

infix 32 -_

_-_ : β„š β†’ β„š β†’ β„š
p - q = p + (- q)

infixl 32 _-_

β„š-minus-zero-is-zero : 0β„š ＝ - 0β„š
β„š-minus-zero-is-zero = refl

toβ„š-neg : ((x , a) : 𝔽) β†’ (- toβ„š (x , a)) ＝ toβ„š (𝔽- (x , a))
toβ„š-neg (x , a) = equivβ†’equality (β„€- x' , a') (𝔽- (x , a)) Ξ³
 where
  x'  = numβ„š (x , a)
  a'  = dnomβ„š (x , a)
  pa  = (pos ∘ succ) a
  pa' = (pos ∘ succ) a'

  Ξ³ : (β„€- x' , a') β‰ˆ (𝔽- (x , a))
  Ξ³ = (β„€- x') β„€* pa ＝⟨ negation-dist-over-mult' x' pa    ⟩
      β„€- x' β„€* pa   ＝⟨ ap β„€-_ (β‰ˆ-toβ„š (x , a) ⁻¹)         ⟩
      β„€- x β„€* pa'   ＝⟨ negation-dist-over-mult' x pa' ⁻¹ ⟩
      (β„€- x) β„€* pa' ∎

β„š-minus-dist : (p q : β„š) β†’ (- p) + (- q) ＝ - (p + q)
β„š-minus-dist ((x , a) , p) ((y , b) , q) = Ξ³
 where
  iiβ‚β‚š : (β„€- x , a) 𝔽+ (β„€- y , b) β‰ˆ (𝔽- ((x , a) 𝔽+ (y , b)))
  iiβ‚β‚š = 𝔽-minus-dist (x , a) (y , b)

  i   = toβ„š-+ (β„€- x , a) (β„€- y , b) ⁻¹
  ii  = equivβ†’equality ((β„€- x , a) 𝔽+ (β„€- y , b)) (𝔽- ((x , a) 𝔽+ (y , b))) iiβ‚β‚š
  iii = toβ„š-neg ((x , a) 𝔽+ (y , b)) ⁻¹

  γ : (- ((x , a) , p)) - ((y , b) , q) ＝ - (((x , a) , p) + ((y , b) , q))
  γ = (- ((x , a) , p)) - ((y , b) , q) ＝⟨refl⟩
      toβ„š (β„€- x , a) + toβ„š (β„€- y , b)   ＝⟨ i    ⟩
      toβ„š ((β„€- x , a) 𝔽+ (β„€- y , b))    ＝⟨ ii   ⟩
      toβ„š (𝔽- ((x , a) 𝔽+ (y , b)))     ＝⟨ iii  ⟩
      - toβ„š ((x , a) 𝔽+ (y , b))        ＝⟨refl⟩
      - (((x , a) , p) + ((y , b) , q)) ∎

β„š-inverse-sum-to-zero : (q : β„š) β†’ q - q ＝ 0β„š
β„š-inverse-sum-to-zero ((x , a) , p) = Ξ³
 where
  I : ((x , a) 𝔽+ (𝔽- (x , a))) β‰ˆ (pos 0 , 0)
    β†’ toβ„š ((x , a) 𝔽+ (𝔽- (x , a))) ＝ toβ„š (pos 0 , 0)
  I = equivβ†’equality ((x , a) 𝔽+ (𝔽- (x , a))) (pos 0 , 0)

  Ξ³ : ((x , a) , p) - ((x , a) , p) ＝ 0β„š
  γ = ((x , a) , p) - ((x , a) , p)  ＝⟨ i   ⟩
      toβ„š (x , a) - toβ„š (x , a)      ＝⟨ ii  ⟩
      toβ„š (x , a) + toβ„š (𝔽- (x , a)) ＝⟨ iii ⟩
      toβ„š ((x , a) 𝔽+ (𝔽- (x , a)))  ＝⟨ iv  ⟩
      0β„š ∎
   where
    i   = ap (Ξ» z β†’ z - z) (toβ„š-to𝔽 ((x , a) , p))
    ii  = ap (toβ„š (x , a) +_) (toβ„š-neg (x , a))
    iii = toβ„š-+ (x , a) (𝔽- (x , a)) ⁻¹
    iv  = I (𝔽+-inverse' (x , a))

β„š-inverse-sum-to-zero' : (q : β„š) β†’ (- q) + q ＝ 0β„š
β„š-inverse-sum-to-zero' q = β„š+-comm (- q) q βˆ™ β„š-inverse-sum-to-zero q

β„š+-inverse : (q : β„š) β†’ Ξ£ q' κž‰ β„š , q + q' ＝ 0β„š
β„š+-inverse q = (- q) , (β„š-inverse-sum-to-zero q)

β„š+-inverse' : (q : β„š) β†’ Ξ£ q' κž‰ β„š , q' + q ＝ 0β„š
β„š+-inverse' q = f (β„š+-inverse q)
  where
   f : Ξ£ q' κž‰ β„š , q + q' ＝ 0β„š β†’ Ξ£ q' κž‰ β„š , q' + q ＝ 0β„š
   f (q' , e) = q' , (β„š+-comm q' q βˆ™ e)

β„š-minus-minus : (p : β„š) β†’ p ＝ - (- p)
β„š-minus-minus ((x , a) , Ξ±) = Ξ³
 where
  γ : ((x , a) , α) ＝ - (- ((x , a) , α))
  γ = ((x , a) , α)         ＝⟨ i    ⟩
      toβ„š (x , a)           ＝⟨ ii   ⟩
      toβ„š (β„€- (β„€- x) , a)   ＝⟨refl⟩
      toβ„š (𝔽- (𝔽- (x , a))) ＝⟨ iii  ⟩
      - toβ„š (𝔽- (x , a))    ＝⟨ iv   ⟩
      - (- toβ„š (x , a))     ＝⟨ v    ⟩
      - (- ((x , a) , α))   ∎
   where
    i   = toβ„š-to𝔽 ((x , a) , Ξ±)
    ii  = ap (Ξ» z β†’ toβ„š (z , a)) (minus-minus-is-plus x ⁻¹)
    iii = toβ„š-neg (𝔽- (x , a)) ⁻¹
    iv  = ap -_ (toβ„š-neg (x , a) ⁻¹)
    v   = ap (-_ ∘ -_) (toβ„š-to𝔽 ((x , a) , Ξ±) ⁻¹)

β„š-minus-dist' : (p q : β„š) β†’ - (p - q) ＝ q - p
β„š-minus-dist' p q = Ξ³
 where
  γ : - (p - q) ＝ q - p
  Ξ³ = - (p - q)     ＝⟨ β„š-minus-dist p (- q) ⁻¹            ⟩
      (- p) - (- q) ＝⟨ ap ((- p) +_) (β„š-minus-minus q ⁻¹) ⟩
      (- p) + q     ＝⟨ β„š+-comm (- p) q                    ⟩
      q - p         ∎

β„š-minus-dist'' : (p q : β„š) β†’ p - q ＝ - (q - p)
β„š-minus-dist'' p q = β„š-minus-dist' q p ⁻¹

β„š-add-zero : (x y z : β„š) β†’ (x + y) ＝ (x - z) + (z + y)
β„š-add-zero x y z = Ξ³
 where
  i   = ap (_+ y) (β„š-zero-right-neutral x ⁻¹)
  ii  = ap (Ξ» k β†’ (x + k) + y) (β„š-inverse-sum-to-zero' z ⁻¹)
  iii = ap (_+ y) (β„š+-assoc x (- z) z ⁻¹)
  iv  = β„š+-assoc (x - z) z y

  γ : (x + y) ＝ (x - z) + (z + y)
  γ = (x + y)             ＝⟨ i   ⟩
      (x + 0β„š) + y        ＝⟨ ii  ⟩
      x + ((- z) + z) + y ＝⟨ iii ⟩
      x + (- z) + z + y   ＝⟨ iv  ⟩
      (x - z) + (z + y)   ∎

β„š-negation-dist-over-mult : (p q : β„š) β†’ (- p) * q ＝ - (p * q)
β„š-negation-dist-over-mult ((x , a) , Ξ±) ((y , b) , Ξ²) = Ξ³
 where
  I : ((𝔽- (x , a)) 𝔽* (y , b)) β‰ˆ (𝔽- ((x , a) 𝔽* (y , b)))
    β†’ toβ„š ((𝔽- (x , a)) 𝔽* (y , b)) ＝ toβ„š (𝔽- ((x , a) 𝔽* (y , b)))
  I = equivβ†’equality ((𝔽- (x , a)) 𝔽* (y , b)) (𝔽- ((x , a) 𝔽* (y , b)))

  i   = ap (toβ„š (𝔽- (x , a)) *_) (toβ„š-to𝔽 ((y , b) , Ξ²))
  ii  = toβ„š-* (𝔽- (x , a)) (y , b) ⁻¹
  iii = I (𝔽-subtraction-dist-over-mult (x , a) (y , b))
  iv  = toβ„š-neg ((x , a) 𝔽* (y , b)) ⁻¹

  γ : (- ((x , a) , α)) * ((y , b) , β) ＝ - ((x , a) , α) * ((y , b) , β)
  γ = (- ((x , a) , α)) * ((y , b) , β) ＝⟨refl⟩
      toβ„š (𝔽- (x , a)) * ((y , b) , Ξ²)  ＝⟨ i    ⟩
      toβ„š (𝔽- (x , a)) * toβ„š (y , b)    ＝⟨ ii   ⟩
      toβ„š ((𝔽- (x , a)) 𝔽* (y , b))     ＝⟨ iii  ⟩
      toβ„š (𝔽- ((x , a) 𝔽* (y , b)))     ＝⟨ iv   ⟩
      - toβ„š ((x , a) 𝔽* (y , b))        ＝⟨refl⟩
      - ((x , a) , α) * ((y , b) , β)   ∎

β„š-negation-dist-over-mult' : (p q : β„š) β†’ p * (- q) ＝ - (p * q)
β„š-negation-dist-over-mult' p q = Ξ³
 where
  γ : p * (- q) ＝ - p * q
  Ξ³ = p * (- q) ＝⟨ β„š*-comm p (- q)               ⟩
      (- q) * p ＝⟨ β„š-negation-dist-over-mult q p ⟩
      - q * p   ＝⟨ ap -_ (β„š*-comm q p)           ⟩
      - p * q   ∎

β„š-negation-dist-over-mult'' : (p q : β„š) β†’ p * (- q) ＝ (- p) * q
β„š-negation-dist-over-mult'' p q = Ξ³
 where
  γ : p * (- q) ＝ (- p) * q
  Ξ³ = p * (- q) ＝⟨ β„š-negation-dist-over-mult' p q   ⟩
      - p * q   ＝⟨ β„š-negation-dist-over-mult p q ⁻¹ ⟩
      (- p) * q ∎

toβ„š-subtraction : (p q : 𝔽) β†’ toβ„š p - toβ„š q ＝ toβ„š (p 𝔽+ (𝔽- q))
toβ„š-subtraction p q = Ξ³
 where
  Ξ³ : toβ„š p - toβ„š q ＝ toβ„š (p 𝔽+ (𝔽- q))
  Ξ³ = toβ„š p - toβ„š q      ＝⟨ ap (toβ„š p +_) (toβ„š-neg q) ⟩
      toβ„š p + toβ„š (𝔽- q) ＝⟨ toβ„š-+ p (𝔽- q) ⁻¹         ⟩
      toβ„š (p 𝔽+ (𝔽- q))  ∎

β„š-inverse-intro : (p q : β„š) β†’ p ＝ p + (q - q)
β„š-inverse-intro p q = p           ＝⟨ β„š-zero-right-neutral p ⁻¹              ⟩
                      p + 0β„š      ＝⟨ ap (p +_) (β„š-inverse-sum-to-zero q ⁻¹) ⟩
                      p + (q - q) ∎

β„š-inverse-intro'' : (p q : β„š) β†’ p ＝ p + q - q
β„š-inverse-intro'' p q = β„š-inverse-intro p q βˆ™ β„š+-assoc p q (- q) ⁻¹

β„š-inverse-intro' : (p q : β„š) β†’ p ＝ (q - q) + p
β„š-inverse-intro' p q = β„š-inverse-intro p q βˆ™ β„š+-comm p (q - q)

β„š-inverse-intro''' : (p q : β„š) β†’ p ＝ p + ((- q) + q)
β„š-inverse-intro''' p q = β„š-inverse-intro p q βˆ™ ap (p +_) (β„š+-comm q (- q))

β„š-inverse-intro'''' : (p q : β„š) β†’ p ＝ p - q + q
β„š-inverse-intro'''' p q = β„š-inverse-intro''' p q βˆ™ β„š+-assoc p (- q) q ⁻¹

1-2/3 : 1β„š - 2/3 ＝ 1/3
1-2/3 = refl

1-1/3 : 1β„š - 1/3 ＝ 2/3
1-1/3 = refl

1-2/5＝3/5 : 1β„š - 2/5 ＝ 3/5
1-2/5＝3/5 = refl

1-1/2 : 1β„š - 1/2 ＝ 1/2
1-1/2 = refl

1/2-1 : 1/2 - 1β„š ＝ - 1/2
1/2-1 = refl

β„š-minus-half : (p : β„š) β†’ p - 1/2 * p ＝ 1/2 * p
β„š-minus-half p
 = p - 1/2 * p          ＝⟨ ap (_- 1/2 * p) (β„š-mult-left-id p ⁻¹)               ⟩
   1β„š * p - 1/2 * p     ＝⟨ ap (1β„š * p +_) (β„š-negation-dist-over-mult 1/2 p ⁻¹) ⟩
   1β„š * p + (- 1/2) * p ＝⟨ β„š-distributivity' p 1β„š (- 1/2) ⁻¹                   ⟩
   (1β„š - 1/2) * p       ＝⟨ refl                                                ⟩
   1/2 * p              ∎

β„š+-right-cancellable : (p q r : β„š) β†’ p + r ＝ q + r β†’ p ＝ q
β„š+-right-cancellable p q r e = Ξ³
 where
  γ : p ＝ q
  Ξ³ = p         ＝⟨ β„š-inverse-intro'' p r    ⟩
      p + r - r ＝⟨ ap (_- r) e              ⟩
      q + r - r ＝⟨ β„š-inverse-intro'' q r ⁻¹ ⟩
      q         ∎

β„š-add-zero-twice'' : (p q r : β„š) β†’ p ＝ p + q + r - q - r
β„š-add-zero-twice'' p q r = Ξ³
 where
  γ : p ＝ p + q + r - q - r
  Ξ³ = p                   ＝⟨ β„š-inverse-intro'' p q                        ⟩
      p + q - q           ＝⟨ ap (Ξ» β–  β†’ p + β–  - q) (β„š-inverse-intro'' q r) ⟩
      p + (q + r - r) - q ＝⟨ ap (_- q) (β„š+-assoc p (q + r) (- r) ⁻¹)      ⟩
      p + (q + r) - r - q ＝⟨ ap (Ξ» β–  β†’ β–  - r - q) (β„š+-assoc p q r ⁻¹)     ⟩
      p + q + r - r - q   ＝⟨ β„š+-rearrange (p + q + r) (- q) (- r) ⁻¹      ⟩
      p + q + r - q - r   ∎

β„š-add-zero-twice''' : (p q r : β„š) β†’ p ＝ p - q - r + q + r
β„š-add-zero-twice''' p q r = Ξ³
 where
  γ : p ＝ p - q - r + q + r
  Ξ³ = p                         ＝⟨ β„š-add-zero-twice'' p q r                    ⟩
      p + q + r - q - r         ＝⟨ β„š+-assoc (p + q + r) (- q) (- r)            ⟩
      p + q + r + ((- q) - r)   ＝⟨ ap (_+ ((- q) - r)) (β„š+-assoc p q r)        ⟩
      p + (q + r) + ((- q) - r) ＝⟨ β„š+-rearrange p (q + r) ((- q) - r)          ⟩
      p + ((- q) - r) + (q + r) ＝⟨ ap (_+ (q + r)) (β„š+-assoc p (- q) (- r) ⁻¹) ⟩
      p - q - r + (q + r)       ＝⟨ β„š+-assoc (p - q - r) q r ⁻¹                 ⟩
      p - q - r + q + r         ∎

β„š-add-zero-twice : (p q : β„š) β†’ p ＝ p - q - q + q + q
β„š-add-zero-twice p q = β„š-add-zero-twice''' p q q

β„š-add-zero-twice' : (p q : β„š) β†’ p ＝ p + q + q - q - q
β„š-add-zero-twice' p q = β„š-add-zero-twice'' p q q