module Data.Integer where
open import Data.Nat as ℕ
using (ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
import Data.Nat.Show as ℕ
open import Data.Sign as Sign using (Sign) renaming (_*_ to _S*_)
open import Data.Product as Prod
open import Data.String using (String; _++_)
open import Function
open import Data.Sum as Sum
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
infix 8 +_ -_
infixl 7 _*_ _⊓_
infixl 6 _+_ _-_ _⊖_ _⊔_
infix 4 _≤_ _≤?_
data ℤ : Set where
-[1+_] : (n : ℕ) → ℤ
+_ : (n : ℕ) → ℤ
∣_∣ : ℤ → ℕ
∣ + n ∣ = n
∣ -[1+ n ] ∣ = ℕ.suc n
sign : ℤ → Sign
sign (+ _) = Sign.+
sign -[1+ _ ] = Sign.-
show : ℤ → String
show i = showSign (sign i) ++ ℕ.show ∣ i ∣
where
showSign : Sign → String
showSign Sign.- = "-"
showSign Sign.+ = ""
infix 5 _◂_ _◃_
_◃_ : Sign → ℕ → ℤ
_ ◃ ℕ.zero = + ℕ.zero
Sign.+ ◃ n = + n
Sign.- ◃ ℕ.suc n = -[1+ n ]
◃-left-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
◃-left-inverse -[1+ n ] = refl
◃-left-inverse (+ ℕ.zero) = refl
◃-left-inverse (+ ℕ.suc n) = refl
◃-cong : ∀ {i j} → sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j
◃-cong {i} {j} sign-≡ abs-≡ = begin
i ≡⟨ sym $ ◃-left-inverse i ⟩
sign i ◃ ∣ i ∣ ≡⟨ cong₂ _◃_ sign-≡ abs-≡ ⟩
sign j ◃ ∣ j ∣ ≡⟨ ◃-left-inverse j ⟩
j ∎
data SignAbs : ℤ → Set where
_◂_ : (s : Sign) (n : ℕ) → SignAbs (s ◃ n)
signAbs : ∀ i → SignAbs i
signAbs i = PropEq.subst SignAbs (◃-left-inverse i) $
sign i ◂ ∣ i ∣
_≟_ : Decidable {A = ℤ} _≡_
i ≟ j with Sign._≟_ (sign i) (sign j) | ℕ._≟_ ∣ i ∣ ∣ j ∣
i ≟ j | yes sign-≡ | yes abs-≡ = yes (◃-cong sign-≡ abs-≡)
i ≟ j | no sign-≢ | _ = no (sign-≢ ∘ cong sign)
i ≟ j | _ | no abs-≢ = no (abs-≢ ∘ cong ∣_∣)
decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_
-_ : ℤ → ℤ
- (+ ℕ.suc n) = -[1+ n ]
- (+ ℕ.zero) = + ℕ.zero
- -[1+ n ] = + ℕ.suc n
_⊖_ : ℕ → ℕ → ℤ
m ⊖ ℕ.zero = + m
ℕ.zero ⊖ ℕ.suc n = -[1+ n ]
ℕ.suc m ⊖ ℕ.suc n = m ⊖ n
_+_ : ℤ → ℤ → ℤ
-[1+ m ] + -[1+ n ] = -[1+ ℕ.suc (m ℕ+ n) ]
-[1+ m ] + + n = n ⊖ ℕ.suc m
+ m + -[1+ n ] = m ⊖ ℕ.suc n
+ m + + n = + (m ℕ+ n)
_-_ : ℤ → ℤ → ℤ
i - j = i + - j
suc : ℤ → ℤ
suc i = + 1 + i
private
suc-is-lazy⁺ : ∀ n → suc (+ n) ≡ + ℕ.suc n
suc-is-lazy⁺ n = refl
suc-is-lazy⁻ : ∀ n → suc -[1+ ℕ.suc n ] ≡ -[1+ n ]
suc-is-lazy⁻ n = refl
pred : ℤ → ℤ
pred i = - + 1 + i
private
pred-is-lazy⁺ : ∀ n → pred (+ ℕ.suc n) ≡ + n
pred-is-lazy⁺ n = refl
pred-is-lazy⁻ : ∀ n → pred -[1+ n ] ≡ -[1+ ℕ.suc n ]
pred-is-lazy⁻ n = refl
_*_ : ℤ → ℤ → ℤ
i * j = sign i S* sign j ◃ ∣ i ∣ ℕ* ∣ j ∣
_⊔_ : ℤ → ℤ → ℤ
-[1+ m ] ⊔ -[1+ n ] = -[1+ ℕ._⊓_ m n ]
-[1+ m ] ⊔ + n = + n
+ m ⊔ -[1+ n ] = + m
+ m ⊔ + n = + (ℕ._⊔_ m n)
_⊓_ : ℤ → ℤ → ℤ
-[1+ m ] ⊓ -[1+ n ] = -[1+ ℕ._⊔_ m n ]
-[1+ m ] ⊓ + n = -[1+ m ]
+ m ⊓ -[1+ n ] = -[1+ n ]
+ m ⊓ + n = + (ℕ._⊓_ m n)
data _≤_ : ℤ → ℤ → Set where
-≤+ : ∀ {m n} → -[1+ m ] ≤ + n
-≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ]
+≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n
drop‿+≤+ : ∀ {m n} → + m ≤ + n → ℕ._≤_ m n
drop‿+≤+ (+≤+ m≤n) = m≤n
drop‿-≤- : ∀ {m n} → -[1+ m ] ≤ -[1+ n ] → ℕ._≤_ n m
drop‿-≤- (-≤- n≤m) = n≤m
_≤?_ : Decidable _≤_
-[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (ℕ._≤?_ n m)
-[1+ m ] ≤? + n = yes -≤+
+ m ≤? -[1+ n ] = no λ ()
+ m ≤? + n = Dec.map′ +≤+ drop‿+≤+ (ℕ._≤?_ m n)
decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
{ Carrier = ℤ
; _≈_ = _≡_
; _≤_ = _≤_
; isDecTotalOrder = record
{ isTotalOrder = record
{ isPartialOrder = record
{ isPreorder = record
{ isEquivalence = PropEq.isEquivalence
; reflexive = refl′
; trans = trans
}
; antisym = antisym
}
; total = total
}
; _≟_ = _≟_
; _≤?_ = _≤?_
}
}
where
module ℕO = DecTotalOrder ℕ.decTotalOrder
refl′ : _≡_ ⇒ _≤_
refl′ { -[1+ n ]} refl = -≤- ℕO.refl
refl′ {+ n} refl = +≤+ ℕO.refl
trans : Transitive _≤_
trans -≤+ (+≤+ n≤m) = -≤+
trans (-≤- n≤m) -≤+ = -≤+
trans (-≤- n≤m) (-≤- k≤n) = -≤- (ℕO.trans k≤n n≤m)
trans (+≤+ m≤n) (+≤+ n≤k) = +≤+ (ℕO.trans m≤n n≤k)
antisym : Antisymmetric _≡_ _≤_
antisym -≤+ ()
antisym (-≤- n≤m) (-≤- m≤n) = cong -[1+_] $ ℕO.antisym m≤n n≤m
antisym (+≤+ m≤n) (+≤+ n≤m) = cong +_ $ ℕO.antisym m≤n n≤m
total : Total _≤_
total (-[1+ m ]) (-[1+ n ]) = [ inj₂ ∘′ -≤- , inj₁ ∘′ -≤- ]′ $ ℕO.total m n
total (-[1+ m ]) (+ n ) = inj₁ -≤+
total (+ m ) (-[1+ n ]) = inj₂ -≤+
total (+ m ) (+ n ) = [ inj₁ ∘′ +≤+ , inj₂ ∘′ +≤+ ]′ $ ℕO.total m n
poset : Poset _ _ _
poset = DecTotalOrder.poset decTotalOrder
import Relation.Binary.PartialOrderReasoning as POR
module ≤-Reasoning = POR poset
renaming (_≈⟨_⟩_ to _≡⟨_⟩_)