Attempt at the INT construction

src/Data/Integer/IntConstruction.agda

@@ -0,0 +1,77 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Construction of integers as a pair of naturals
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction where
+
+open import Data.Nat.Base as ℕ using (ℕ)
+open import Function.Base using (flip)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+infixl 6 _⊖_
+
+record ℤ : Set where
+  constructor _⊖_
+  field
+    minuend : ℕ
+    subtrahend : ℕ
+
+infix 4 _≃_ _≤_ _≥_ _<_ _>_
+
+record _≃_ (i j : ℤ) : Set where
+  constructor mk≃
+  field
+    eq : ℤ.minuend i ℕ.+ ℤ.subtrahend j ≡ ℤ.minuend j ℕ.+ ℤ.subtrahend i
+
+_≤_ : Rel ℤ _
+(a ⊖ b) ≤ (c ⊖ d) = a ℕ.+ d ℕ.≤ c ℕ.+ b
+
+_≥_ : Rel ℤ _
+_≥_ = flip _≤_
+
+_<_ : Rel ℤ _
+(a ⊖ b) < (c ⊖ d) = a ℕ.+ d ℕ.< c ℕ.+ b
+
+_>_ : Rel ℤ _
+_>_ = flip _<_
+
+suc : ℤ → ℤ
+suc (a ⊖ b) = ℕ.suc a ⊖ b
+
+pred : ℤ → ℤ
+pred (a ⊖ b) = a ⊖ ℕ.suc b
+
+0ℤ : ℤ
+0ℤ = 0 ⊖ 0
+
+1ℤ : ℤ
+1ℤ = 1 ⊖ 0
+
+infixl 6 _+_
+_+_ : ℤ → ℤ → ℤ
+(a ⊖ b) + (c ⊖ d) = (a ℕ.+ c) ⊖ (b ℕ.+ d)
+
+infixl 7 _*_
+_*_ : ℤ → ℤ → ℤ
+(a ⊖ b) * (c ⊖ d) = (a ℕ.* c ℕ.+ b ℕ.* d) ⊖ (a ℕ.* d ℕ.+ b ℕ.* c)
+
+infix 8 -_
+-_ : ℤ → ℤ
+- (a ⊖ b) = b ⊖ a
+
+infix 8 ⁻_ ⁺_
+
+⁺_ : ℕ → ℤ
+⁺ n = n ⊖ 0
+
+⁻_ : ℕ → ℤ
+⁻ n = 0 ⊖ n
+
+∣_∣ : ℤ → ℕ
+∣ a ⊖ b ∣ = ℕ.∣ a - b ∣′
+

src/Data/Integer/IntConstruction/DivMod.agda

@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Division with remainder for integers constructed as a pair of naturals
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction.DivMod where
+
+open import Data.Fin.Base as Fin using (Fin)
+import Data.Fin.Properties as Fin
+open import Data.Integer.IntConstruction
+open import Data.Integer.IntConstruction.Properties
+open import Data.Nat.Base as ℕ using (ℕ)
+import Data.Nat.Properties as ℕ
+import Data.Nat.DivMod as ℕ
+open import Function.Base
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary.Decidable
+
+-- should the divisor also be an integer?
+record DivMod (dividend : ℤ) (divisor : ℕ) : Set where
+  field
+    quotient : ℤ
+    remainder : ℕ
+    remainder<divisor : remainder ℕ.< divisor
+    property : dividend ≃ ⁺ remainder + quotient * ⁺ divisor
+
+divMod : ∀ i n .{{_ : ℕ.NonZero n}} → DivMod i n
+divMod (a ⊖ b) n = record
+  { quotient = quotient
+  ; remainder<divisor = remainder<n
+  ; property = property
+  }
+  where
+    open ≡-Reasoning
+
+  -- either the actual quotient or one above it
+    quotient′ : ℤ
+    quotient′ = (a ℕ./ n) ⊖ (b ℕ./ n)
+
+    remainder′ : ℤ
+    remainder′ = (a ℕ.% n) ⊖ (b ℕ.% n)
+
+    property′ : a ⊖ b ≃ remainder′ + quotient′ * ⁺ n
+    property′ = mk≃ $ cong₂ ℕ._+_ left right
+      where
+        left : a ≡ a ℕ.% n ℕ.+ (a ℕ./ n ℕ.* n ℕ.+ b ℕ./ n ℕ.* 0)
+        left = begin
+          a                                             ≡⟨ ℕ.m≡m%n+[m/n]*n a n ⟩
+          a ℕ.% n ℕ.+ a ℕ./ n ℕ.* n                     ≡⟨ cong (a ℕ.% n ℕ.+_) (ℕ.+-identityʳ (a ℕ./ n ℕ.* n)) ⟨
+          a ℕ.% n ℕ.+ (a ℕ./ n ℕ.* n ℕ.+ 0)             ≡⟨ cong (λ z → a ℕ.% n ℕ.+ (a ℕ./ n ℕ.* n ℕ.+ z)) (ℕ.*-zeroʳ (b ℕ./ n)) ⟨
+          a ℕ.% n ℕ.+ (a ℕ./ n ℕ.* n ℕ.+ b ℕ./ n ℕ.* 0) ∎
+
+        right : b ℕ.% n ℕ.+ (a ℕ./ n ℕ.* 0 ℕ.+ b ℕ./ n ℕ.* n) ≡ b
+        right = begin
+          b ℕ.% n ℕ.+ (a ℕ./ n ℕ.* 0 ℕ.+ b ℕ./ n ℕ.* n) ≡⟨ cong (λ z → b ℕ.% n ℕ.+ (z ℕ.+ b ℕ./ n ℕ.* n)) (ℕ.*-zeroʳ (a ℕ./ n)) ⟩
+          b ℕ.% n ℕ.+ (0 ℕ.+ b ℕ./ n ℕ.* n)             ≡⟨ cong (b ℕ.% n ℕ.+_) (ℕ.+-identityˡ (b ℕ./ n ℕ.* n)) ⟩
+          b ℕ.% n ℕ.+ b ℕ./ n ℕ.* n                     ≡⟨ ℕ.m≡m%n+[m/n]*n b n ⟨
+          b                                             ∎
+
+    quotient : ℤ
+    quotient with b ℕ.% n ℕ.≤? a ℕ.% n
+    ... | yes _ = quotient′
+    ... | no _ = pred quotient′
+
+    remainder : ℕ
+    remainder with b ℕ.% n ℕ.≤? a ℕ.% n
+    ... | yes _ = a ℕ.% n ℕ.∸ b ℕ.% n
+    ... | no _ = n ℕ.∸ (b ℕ.% n ℕ.∸ a ℕ.% n)
+
+    remainder<n : remainder ℕ.< n
+    remainder<n with b ℕ.% n ℕ.≤? a ℕ.% n
+    ... | yes _ = ℕ.≤-<-trans (ℕ.m∸n≤m (a ℕ.% n) (b ℕ.% n)) (ℕ.m%n<n a n)
+    ... | no b%n≰a%n = ℕ.∸-monoʳ-< {o = 0} (ℕ.m<n⇒0<n∸m (ℕ.≰⇒> b%n≰a%n)) (ℕ.≤-trans (ℕ.m∸n≤m (b ℕ.% n) (a ℕ.% n)) (ℕ.<⇒≤ (ℕ.m%n<n b n)))
+
+    property : a ⊖ b ≃ ⁺ remainder + quotient * ⁺ n
+    property with b ℕ.% n ℕ.≤? a ℕ.% n
+    ... | yes p = ≃-trans property′ (+-cong rem-prop ≃-refl)
+      where
+        rem-prop : remainder′ ≃ ⁺ (a ℕ.% n ℕ.∸ b ℕ.% n)
+        rem-prop = mk≃ $ begin
+          a ℕ.% n ℕ.+ 0                   ≡⟨ ℕ.+-identityʳ (a ℕ.% n) ⟩
+          a ℕ.% n                         ≡⟨ ℕ.m∸n+n≡m p ⟨
+          a ℕ.% n ℕ.∸ b ℕ.% n ℕ.+ b ℕ.% n ∎
+    ... | no b%n≰a%n = ≃-trans property′ $ mk≃ $ begin
+      (w ℕ.+ x) ℕ.+ (y ℕ.+ (n ℕ.+ z))                 ≡⟨ cong ((w ℕ.+ x) ℕ.+_) (ℕ.+-assoc y n z) ⟨
+      (w ℕ.+ x) ℕ.+ ((y ℕ.+ n) ℕ.+ z)                 ≡⟨ cong (λ k → (w ℕ.+ x) ℕ.+ (k ℕ.+ z)) (ℕ.+-comm y n) ⟩
+      (w ℕ.+ x) ℕ.+ ((n ℕ.+ y) ℕ.+ z)                 ≡⟨ cong ((w ℕ.+ x) ℕ.+_) (ℕ.+-assoc n y z) ⟩
+      (w ℕ.+ x) ℕ.+ (n ℕ.+ (y ℕ.+ z))                 ≡⟨ ℕ.+-assoc (w ℕ.+ x) n (y ℕ.+ z) ⟨
+      ((w ℕ.+ x) ℕ.+ n) ℕ.+ (y ℕ.+ z)                 ≡⟨ cong (ℕ._+ (y ℕ.+ z)) (ℕ.+-comm (w ℕ.+ x) n) ⟩
+      (n ℕ.+ (w ℕ.+ x)) ℕ.+ (y ℕ.+ z)                 ≡⟨ cong (ℕ._+ (y ℕ.+ z)) (ℕ.+-assoc n w x) ⟨
+      ((n ℕ.+ w) ℕ.+ x) ℕ.+ (y ℕ.+ z)                 ≡⟨ cong (λ k → ((n ℕ.+ k) ℕ.+ x) ℕ.+ (y ℕ.+ z)) (ℕ.m∸[m∸n]≡n (ℕ.≰⇒≥ b%n≰a%n)) ⟨
+      ((n ℕ.+ (v ℕ.∸ (v ℕ.∸ w))) ℕ.+ x) ℕ.+ (y ℕ.+ z) ≡⟨ cong (λ k → (k ℕ.+ x) ℕ.+ (y ℕ.+ z)) (ℕ.+-∸-assoc n (ℕ.m∸n≤m v w)) ⟨
+      (((n ℕ.+ v) ℕ.∸ (v ℕ.∸ w)) ℕ.+ x) ℕ.+ (y ℕ.+ z) ≡⟨ cong (λ k → (k ℕ.+ x) ℕ.+ (y ℕ.+ z)) (ℕ.+-∸-comm v (ℕ.≤-trans (ℕ.m∸n≤m v w) (ℕ.<⇒≤ (ℕ.m%n<n b n)))) ⟩
+      (((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ v) ℕ.+ x) ℕ.+ (y ℕ.+ z) ≡⟨ cong (ℕ._+ (y ℕ.+ z)) (ℕ.+-assoc (n ℕ.∸ (v ℕ.∸ w)) v x) ⟩
+      ((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ (v ℕ.+ x)) ℕ.+ (y ℕ.+ z) ≡⟨ cong (λ k → ((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ k) ℕ.+ (y ℕ.+ z)) (ℕ.+-comm v x) ⟩
+      ((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ (x ℕ.+ v)) ℕ.+ (y ℕ.+ z) ≡⟨ cong (ℕ._+ (y ℕ.+ z)) (ℕ.+-assoc (n ℕ.∸ (v ℕ.∸ w)) x v) ⟨
+      (((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ x) ℕ.+ v) ℕ.+ (y ℕ.+ z) ≡⟨ ℕ.+-assoc (n ℕ.∸ (v ℕ.∸ w) ℕ.+ x) v (y ℕ.+ z) ⟩
+      ((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ x) ℕ.+ (v ℕ.+ (y ℕ.+ z)) ∎
+      where
+        w = a ℕ.% n
+        x = a ℕ./ n ℕ.* n ℕ.+ b ℕ./ n ℕ.* 0
+        y = a ℕ./ n ℕ.* 0
+        z = b ℕ./ n ℕ.* n
+        v = b ℕ.% n

src/Data/Integer/IntConstruction/IntProperties.agda

@@ -0,0 +1,72 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- To be merged into Data.Integer.Properties before merging!
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Data.Integer.IntConstruction.IntProperties where
+
+open import Data.Integer.Base
+open import Data.Integer.IntConstruction as INT using (_≃_; mk≃)
+open import Data.Integer.IntConstruction.Tmp
+open import Data.Integer.Properties
+import Data.Nat.Base as ℕ
+open import Data.Product.Base
+open import Function.Base
+open import Relation.Binary.PropositionalEquality
+
+fromINT-cong : ∀ {i j} → i ≃ j → fromINT i ≡ fromINT j
+fromINT-cong {a INT.⊖ b} {c INT.⊖ d} (mk≃ a+d≡c+b) = begin
+  a ⊖ b                       ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b                   ≡⟨ cong (_- + b) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) - + b            ≡⟨ cong (λ z → (+ a + z) - + b) (+-inverseʳ (+ d)) ⟨
+  (+ a + (+ d - + d)) - + b   ≡⟨ cong (_- + b) (+-assoc (+ a) (+ d) (- + d)) ⟨
+  (+ (a ℕ.+ d) - + d) - + b   ≡⟨ cong (λ z → (+ z - + d) - + b) a+d≡c+b ⟩
+  (+ (c ℕ.+ b) - + d) - + b   ≡⟨ cong (_- + b) (+-assoc (+ c) (+ b) (- + d)) ⟩
+  (+ c + (+ b - + d)) - + b   ≡⟨ cong (λ z → (+ c + z) - + b) (+-comm (+ b) (- + d)) ⟩
+  (+ c + (- + d + + b)) - + b ≡⟨ cong (_- + b) (+-assoc (+ c) (- + d) (+ b)) ⟨
+  ((+ c - + d) + + b) - + b   ≡⟨ +-assoc (+ c - + d) (+ b) (- + b) ⟩
+  (+ c - + d) + (+ b - + b)   ≡⟨ cong₂ _+_ (m-n≡m⊖n c d) (+-inverseʳ (+ b)) ⟩
+  c ⊖ d + 0ℤ                  ≡⟨ +-identityʳ (c ⊖ d) ⟩
+  c ⊖ d                       ∎
+  where open ≡-Reasoning
+
+fromINT-injective : ∀ {i j} → fromINT i ≡ fromINT j → i ≃ j
+fromINT-injective {a INT.⊖ b} {c INT.⊖ d} a⊖b≡c⊖d = mk≃ $ +-injective $ begin
+  + a + + d                   ≡⟨ cong (_+ + d) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) + + d            ≡⟨ cong (λ z → (+ a + z) + + d) (+-inverseˡ (+ b)) ⟨
+  (+ a + (- + b + + b)) + + d ≡⟨ cong (_+ + d) (+-assoc (+ a) (- + b) (+ b)) ⟨
+  ((+ a - + b) + + b) + + d   ≡⟨ cong (λ z → (z + + b) + + d) (m-n≡m⊖n a b) ⟩
+  (a ⊖ b + + b) + + d         ≡⟨ cong (λ z → (z + + b) + + d) a⊖b≡c⊖d ⟩
+  (c ⊖ d + + b) + + d         ≡⟨ cong (λ z → (z + + b) + + d) (m-n≡m⊖n c d) ⟨
+  ((+ c - + d) + + b) + + d   ≡⟨ cong (_+ + d) (+-assoc (+ c) (- + d) (+ b)) ⟩
+  (+ c + (- + d + + b)) + + d ≡⟨ cong (λ z → (+ c + z) + + d) (+-comm (- + d) (+ b)) ⟩
+  (+ c + (+ b - + d)) + + d   ≡⟨ cong (_+ + d) (+-assoc (+ c) (+ b) (- + d)) ⟨
+  ((+ c + + b) - + d) + + d   ≡⟨ +-assoc (+ c + + b) (- + d) (+ d) ⟩
+  (+ c + + b) + (- + d + + d) ≡⟨ cong (_+_ (+ c + + b)) (+-inverseˡ (+ d)) ⟩
+  (+ c + + b) + 0ℤ            ≡⟨ +-identityʳ (+ c + + b) ⟩
+  + c + + b                   ∎
+  where open ≡-Reasoning
+
+fromINT-surjective : ∀ j → ∃[ i ] ∀ {z} → z ≃ i → fromINT z ≡ j
+fromINT-surjective j .proj₁ = toINT j
+fromINT-surjective (+ n) .proj₂ {a INT.⊖ b} (mk≃ a+0≡n+b) = begin
+  a ⊖ b             ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b         ≡⟨ cong (_- + b) (+-identityʳ (+ a)) ⟨
+  (+ a + 0ℤ) - + b  ≡⟨ cong (λ z → + z - + b) a+0≡n+b ⟩
+  (+ n + + b) - + b ≡⟨ +-assoc (+ n) (+ b) (- + b) ⟩
+  + n + (+ b - + b) ≡⟨ cong (_+_ (+ n)) (+-inverseʳ (+ b)) ⟩
+  + n + 0ℤ          ≡⟨ +-identityʳ (+ n) ⟩
+  + n               ∎
+  where open ≡-Reasoning
+fromINT-surjective (-[1+ n ]) .proj₂ {a INT.⊖ b} (mk≃ a+sn≡b) = begin
+  a ⊖ b                     ≡⟨ m-n≡m⊖n a b ⟨
+  + a - + b                 ≡⟨ cong (λ z → + a - + z) a+sn≡b ⟨
+  + a - (+ a + + ℕ.suc n)   ≡⟨ cong (_+_ (+ a)) (neg-distrib-+ (+ a) (+ ℕ.suc n)) ⟩
+  + a + (- + a - + ℕ.suc n) ≡⟨ +-assoc (+ a) (- + a) (- + ℕ.suc n) ⟨
+  (+ a - + a) - + ℕ.suc n   ≡⟨ cong (_- + ℕ.suc n) (+-inverseʳ (+ a)) ⟩
+  0ℤ - + ℕ.suc n            ≡⟨ +-identityˡ (- + ℕ.suc n) ⟩
+  -[1+ n ]                  ∎
+  where open ≡-Reasoning