Added a properties file for Data.Bin

CHANGELOG.md

@@ -8,21 +8,32 @@ Important changes since 0.13:
 Non-backwards compatible changes
 --------------------------------
 
+* Added new module `Data.Bin.Properties` and moved `strictTotalOrder` and
+  `decSetoid` from `Data.Bin` to `<-strictTotalOrder` and `≡-decSetoid`
+  in `Data.Bin.Properties`.
+
+  Reasons:
+
+  1. `Data.Bin` was becoming too large.
+  2. Better conforms to library conventions for other numeric datatypes.
+
 * Moved `decTotalOrder` in `Data.Nat` to `≤-decTotalOrder` in
   `Data.Nat.Properties`.
 
   Reasons:
-          1. Its old location didn't conform to the library's conventions.
-          2. Its old location was causing dependency cyles when trying to
-             add new ordering properties to `Data.Nat.Properties`.
+
+  1. Its old location was causing dependency cyles when trying to add new ordering
+         properties to `Data.Nat.Properties`.
+  2. Better conforms to library conventions.
 
 * Moved module `≤-Reasoning` from `Data.Nat` to `Data.Nat.Properties`
 
 * Moved `¬∀⟶∃¬` from `Relation.Nullary.Negation` to `Data.Fin.Dec`.
 
   Reasons:
-          1. Its old location was causing dependency cyles to form between
-             `Data.Fin.Dec`, `Relation.Nullary.Negation` and `Data.Fin`.
+
+  1. Its old location was causing dependency cyles to form between `Data.Fin.Dec`,
+         `Relation.Nullary.Negation` and `Data.Fin`.
 
 * Moved existing contents of `Data.List.Any.Membership` to
   `Data.List.Any.Membership.Propositional.Properties` and moved internal modules
@@ -31,21 +42,23 @@ Non-backwards compatible changes
   respectively.
 
   Reasons:
-          1. Improves the ease of importing and opening the membership modules
-          2. Allows the creation of a new file `Data.List.Any.Membership.Properties`
-             for setoid membership properties.
+
+  1. Improves the ease of importing and opening the membership modules.
+  2. Allows the creation of a new file `Data.List.Any.Membership.Properties`
+     for setoid membership properties.
 
 * The well-founded relation proofs for the `_<′_` relation have been renamed
   from `<-Rec` and `<-well-founded` to `<′-Rec` and `<′-well-founded`
   respectively. The original names `<-Rec` and `<-well-founded` now refer to new
   corresponding proofs for `_<_`.
 
   Reasons:
-          1. The old names were confusing for newcomers to the library as they
-             would assume `<-wellfounded` referred to the standard `_<_` relation.
-          2. Without renaming the existing proofs, there was no way of adding
-             wellfoundedness proofs for the `_<_` relation without increasing the
-             confusion.
+
+  1. The old names were confusing for newcomers to the library as they
+     would assume `<-wellfounded` referred to the standard `_<_` relation.
+  2. Without renaming the existing proofs, there was no way of adding
+     wellfoundedness proofs for the `_<_` relation without increasing the
+     confusion.
 
 * Changed the implementation of `map` and `zipWith` in `Data.Vec` to use native
   (pattern-matching) definitions. Previously they were defined using the
@@ -54,21 +67,24 @@ Non-backwards compatible changes
   in `Data.Vec.Properties`.
 
   Reasons:
-          1. Better printing of goals involving `map` or `zipWith`.
-          2. It has been argued that `zipWith` is fundamental than `_⊛_`.
+
+  1. Better printing of goals involving `map` or `zipWith`.
+  2. It has been argued that `zipWith` is fundamental than `_⊛_`.
 
 * Changed the implementation of `All₂` in `Data.Vec.All` to a native datatype.
 
   Reasons:
-          1. Improves pattern matching on terms
-          2. The new datatype is more generic with respect to types and levels.
+
+  1. Improves pattern matching on terms.
+  2. The new datatype is more generic with respect to types and levels.
 
 * Changed the implementation of `downFrom` in `Data.List` to a native
   (pattern-matching) definition. Previously it was defined using a private
   internal module.
 
   Reasons:
-          1.  Improves pattern matching.
+
+  1.  Improves pattern matching on terms.
 
 Deprecated features
 -------------------
@@ -184,6 +200,25 @@ Backwards compatible changes
   ∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_
   ```
 
+* Added proofs to `Data.Bin.Properties`:
+  ```agda
+  1#-injective         : as 1# ≡ bs 1# → as ≡ bs
+  _≟_                  : Decidable {A = Bin} _≡_
+  ≡-isDecEquivalence   : IsDecEquivalence _≡_
+  ≡-decSetoid          : DecSetoid _ _
+
+  <-trans              : Transitive _<_
+  <-asym               : Asymmetric _<_
+  <-irrefl             : Irreflexive _≡_ _<_
+  <-cmp                : Trichotomous _≡_ _<_
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+
+  <⇒≢                  : a < b → a ≢ b
+  1<[23]               : [] 1# < (b ∷ []) 1#
+  1<2+                 : [] 1# < (b ∷ bs) 1#
+  0<1+                 : 0# < bs 1#
+  ```
+
 * Added functions to `Data.Fin`:
   ```agda
   punchIn  i j ≈ if j≥i then j+1 else j

src/Data/Bin.agda

@@ -8,23 +8,17 @@ module Data.Bin where
 
 open import Data.Nat as Nat
   using (ℕ; zero; z≤n; s≤s) renaming (suc to 1+_)
-import Data.Nat.Properties as NP
-open NP.≤-Reasoning
 open import Data.Digit
 open import Data.Fin as Fin using (Fin; zero) renaming (suc to 1+_)
 open import Data.Fin.Properties as FP using (_+′_)
 open import Data.List.Base as List hiding (downFrom)
 open import Function
-open import Data.Product
-open import Algebra
+open import Data.Product using (uncurry; _,_; _×_)
 open import Relation.Binary
-open import Relation.Binary.Consequences
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
-private
-  module BitOrd = StrictTotalOrder (FP.strictTotalOrder 2)
 
 ------------------------------------------------------------------------
 -- The type
@@ -93,110 +87,15 @@ fromℕ : ℕ → Bin
 fromℕ n = fromBits $ ntoBits n
 
 ------------------------------------------------------------------------
--- (Bin, _≡_, _<_) is a strict total order
+-- Order relation.
 
-infix 4 _<_
+-- Wrapped so that the parameters can be inferred.
 
--- Order relation. Wrapped so that the parameters can be inferred.
+infix 4 _<_
 
 data _<_ (b₁ b₂ : Bin) : Set where
   less : (lt : (Nat._<_ on toℕ) b₁ b₂) → b₁ < b₂
 
-private
-  <-trans : Transitive _<_
-  <-trans (less lt₁) (less lt₂) = less (NP.<-trans lt₁ lt₂)
-
-  asym : ∀ {b₁ b₂} → b₁ < b₂ → ¬ b₂ < b₁
-  asym {b₁} {b₂} (less lt) (less gt) = tri⟶asym cmp lt gt
-    where cmp = StrictTotalOrder.compare NP.strictTotalOrder
-
-  irr : ∀ {b₁ b₂} → b₁ < b₂ → b₁ ≢ b₂
-  irr lt eq = asym⟶irr (PropEq.resp₂ _<_) sym asym eq lt
-
-  irr′ : ∀ {b} → ¬ b < b
-  irr′ lt = irr lt refl
-
-  ∷∙ : ∀ {b₁ b₂ bs₁ bs₂} →
-       bs₁ 1# < bs₂ 1# → (b₁ ∷ bs₁) 1# < (b₂ ∷ bs₂) 1#
-  ∷∙ {b₁} {b₂} {bs₁} {bs₂} (less lt) = less (begin
-      1 + (m₁ + n₁ * 2)  ≤⟨ +-mono-≤ (≤-refl {x = 1})
-                              (+-mono-≤ (≤-pred (FP.bounded b₁)) ≤-refl) ⟩
-      1 + (1  + n₁ * 2)  ≡⟨ refl ⟩
-            suc n₁ * 2   ≤⟨ *-mono-≤ lt ≤-refl ⟩
-                n₂ * 2   ≤⟨ n≤m+n m₂ (n₂ * 2) ⟩
-           m₂ + n₂ * 2   ∎
-    )
-    where
-    open Nat; open NP
-    m₁ = Fin.toℕ b₁;   m₂ = Fin.toℕ b₂
-    n₁ = toℕ (bs₁ 1#); n₂ = toℕ (bs₂ 1#)
-
-  ∙∷ : ∀ {b₁ b₂ bs} →
-       Fin._<_ b₁ b₂ → (b₁ ∷ bs) 1# < (b₂ ∷ bs) 1#
-  ∙∷ {b₁} {b₂} {bs} lt = less (begin
-    1 + (m₁  + n * 2)  ≡⟨ sym (+-assoc 1 m₁ (n * 2)) ⟩
-    (1 + m₁) + n * 2   ≤⟨ +-mono-≤ lt ≤-refl ⟩
-         m₂  + n * 2   ∎)
-    where
-    open Nat; open NP
-    m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂; n = toℕ (bs 1#)
-
-  1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
-  1<[23] {b} = less (NP.n≤m+n (Fin.toℕ b) 2)
-
-  1<2+ : ∀ {bs b} → [] 1# < (b ∷ bs) 1#
-  1<2+ {[]}     = 1<[23]
-  1<2+ {b ∷ bs} = <-trans 1<[23] (∷∙ {b₁ = b} (1<2+ {bs}))
-
-  0<1 : 0# < [] 1#
-  0<1 = less (s≤s z≤n)
-
-  0<+ : ∀ {bs} → 0# < bs 1#
-  0<+ {[]}     = 0<1
-  0<+ {b ∷ bs} = <-trans 0<1 1<2+
-
-  compare⁺ : Trichotomous (_≡_ on _1#) (_<_ on _1#)
-  compare⁺ []         []         = tri≈ irr′ refl irr′
-  compare⁺ []         (b ∷ bs)   = tri<       1<2+  (irr 1<2+) (asym 1<2+)
-  compare⁺ (b ∷ bs)   []         = tri> (asym 1<2+) (irr 1<2+ ∘ sym) 1<2+
-  compare⁺ (b₁ ∷ bs₁) (b₂ ∷ bs₂) with compare⁺ bs₁ bs₂
-  ... | tri<  lt ¬eq ¬gt = tri<       (∷∙ lt)  (irr (∷∙ lt)) (asym (∷∙ lt))
-  ... | tri> ¬lt ¬eq  gt = tri> (asym (∷∙ gt)) (irr (∷∙ gt) ∘ sym) (∷∙ gt)
-  compare⁺ (b₁ ∷ bs) (b₂ ∷ .bs) | tri≈ ¬lt refl ¬gt with BitOrd.compare b₁ b₂
-  compare⁺ (b  ∷ bs) (.b ∷ .bs) | tri≈ ¬lt refl ¬gt | tri≈ ¬lt′ refl ¬gt′ =
-    tri≈ irr′ refl irr′
-  ... | tri<  lt′ ¬eq ¬gt′ = tri<       (∙∷ lt′)  (irr (∙∷ lt′)) (asym (∙∷ lt′))
-  ... | tri> ¬lt′ ¬eq  gt′ = tri> (asym (∙∷ gt′)) (irr (∙∷ gt′) ∘ sym) (∙∷ gt′)
-
-  compare : Trichotomous _≡_ _<_
-  compare 0#       0#       = tri≈ irr′ refl irr′
-  compare 0#       (bs₂ 1#) = tri<       0<+  (irr 0<+) (asym 0<+)
-  compare (bs₁ 1#) 0#       = tri> (asym 0<+) (irr 0<+ ∘ sym) 0<+
-  compare (bs₁ 1#) (bs₂ 1#) = compare⁺ bs₁ bs₂
-
-strictTotalOrder : StrictTotalOrder _ _ _
-strictTotalOrder = record
-  { Carrier            = Bin
-  ; _≈_                = _≡_
-  ; _<_                = _<_
-  ; isStrictTotalOrder = record
-    { isEquivalence = PropEq.isEquivalence
-    ; trans         = <-trans
-    ; compare       = compare
-    }
-  }
-
-------------------------------------------------------------------------
--- (Bin, _≡_) is a decidable setoid
-
-decSetoid : DecSetoid _ _
-decSetoid = StrictTotalOrder.decSetoid strictTotalOrder
-
-infix 4 _≟_
-
-_≟_ : Decidable {A = Bin} _≡_
-_≟_ = DecSetoid._≟_ decSetoid
-
 ------------------------------------------------------------------------
 -- Arithmetic