WIP: Show that Data.Nat.Show.charsInBase is injective (#1258)

Author: umazalakain

CHANGELOG.md

@@ -285,6 +285,7 @@ Other minor additions
 * Added new proofs to `Data.List.Properties`:
   ```agda
   reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys
+  map-injective : Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
   ```
 
 * Added new proofs to `Data.List.Membership.Propositional.Properties`:
@@ -471,7 +472,7 @@ Other minor additions
   ```agda
   splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
   splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
-  inject≤-injective : (n≤m : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m → x ≡ y
+  inject≤-injective : ∀ (n≤m n≤m′ : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
   ```
 
 * Added new proofs to `Data.Vec.Properties`:

src/Data/Digit/Properties.agda

@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of digits and digit expansions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Digit
+import Data.Char.Properties as Charₚ
+open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Properties using (_≤?_)
+open import Data.Fin.Properties using (inject≤-injective)
+open import Data.Product using (_,_; proj₁)
+open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
+import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
+open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
+open import Relation.Nullary.Decidable using (True; from-yes)
+open import Relation.Nullary.Negation using (¬?)
+open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Function using (_∘_)
+
+module Data.Digit.Properties where
+
+digitCharsUnique : Unique digitChars
+digitCharsUnique = from-yes (allPairs? (λ x y → ¬? (x Charₚ.≟ y)) digitChars)
+
+module _ (base : ℕ) where
+  module _ {base≥2 base≥2′ : True (2 ≤? base)} where
+    toDigits-injective : ∀ n m → proj₁ (toDigits base {base≥2} n) ≡ proj₁ (toDigits base {base≥2′} m) → n ≡ m
+    toDigits-injective n m eq with toDigits base {base≥2} n | toDigits base {base≥2′} m
+    toDigits-injective ._ ._ refl | _ , refl | ._ , refl = refl
+
+  module _ {base≤16 base≤16′ : True (base ≤? 16)} where
+    showDigit-injective : (n m : Digit base) → showDigit {base} {base≤16} n ≡ showDigit {base} {base≤16′} m → n ≡ m
+    showDigit-injective n m = inject≤-injective _ _ n m ∘ Uniqueₚ.lookup-injective digitCharsUnique _ _

src/Data/Fin/Properties.agda

@@ -464,10 +464,10 @@ inject≤-idempotent {_} {suc n} {suc k} zero    _   _   _ = refl
 inject≤-idempotent {_} {suc n} {suc k} (suc i) m≤n n≤k _ =
   cong suc (inject≤-idempotent i (ℕₚ.≤-pred m≤n) (ℕₚ.≤-pred n≤k) _)
 
-inject≤-injective : ∀ {n m} (n≤m : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m → x ≡ y
-inject≤-injective (s≤s p) zero zero eq = refl
-inject≤-injective (s≤s p) (suc x) (suc y) eq =
-  cong suc (inject≤-injective p x y (suc-injective eq))
+inject≤-injective : ∀ {n m} (n≤m n≤m′ : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
+inject≤-injective (s≤s p) (s≤s q) zero zero eq = refl
+inject≤-injective (s≤s p) (s≤s q) (suc x) (suc y) eq =
+  cong suc (inject≤-injective p q x y (suc-injective eq))
 
 ------------------------------------------------------------------------
 -- pred

src/Data/List/Properties.agda

@@ -106,6 +106,12 @@ map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-compose []       = refl
 map-compose (x ∷ xs) = cong (_ ∷_) (map-compose xs)
 
+map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
+map-injective finj {[]} {[]} eq = refl
+map-injective finj {x ∷ xs} {y ∷ ys} eq =
+  let fx≡fy , fxs≡fys = ∷-injective eq in
+  cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
+
 ------------------------------------------------------------------------
 -- mapMaybe
 

src/Data/Nat/Show.agda

@@ -38,12 +38,18 @@ show = String.fromList ∘ toDecimalChars
 -- Warning: when compiled the time complexity of `showInBase b n` is
 -- O(n) instead of the expected O(log(n)).
 
+charsInBase : (base : ℕ)
+              {base≥2 : True (2 ≤? base)}
+              {base≤16 : True (base ≤? 16)} →
+              ℕ → List Char
+charsInBase base {base≥2} {base≤16} = map (showDigit {base≤16 = base≤16})
+                                    ∘ reverse
+                                    ∘ proj₁
+                                    ∘ toDigits base {base≥2 = base≥2}
+
 showInBase : (base : ℕ)
              {base≥2 : True (2 ≤? base)}
              {base≤16 : True (base ≤? 16)} →
              ℕ → String
-showInBase base {base≥2} {base≤16} n =
-  String.fromList $
-  map (showDigit {base≤16 = base≤16}) $
-  reverse $
-  proj₁ $ toDigits base {base≥2 = base≥2} n
+showInBase base {base≥2} {base≤16} = String.fromList
+                                   ∘ charsInBase base {base≥2} {base≤16}

src/Data/Nat/Show/Properties.agda

@@ -0,0 +1,26 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of showing natural numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Digit using (showDigit; toDigits)
+open import Data.Digit.Properties using (toDigits-injective; showDigit-injective)
+open import Function using (_∘_)
+import Data.List.Properties as Listₚ
+open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Properties using (_≤?_)
+open import Relation.Nullary.Decidable using (True)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Data.Nat.Show using (charsInBase)
+
+module Data.Nat.Show.Properties where
+
+module _ (base : ℕ) {base≥2 : True (2 ≤? base)} {base≤16 : True (base ≤? 16)} where
+
+  charsInBase-injective : ∀ n m → charsInBase base {base≥2} {base≤16} n ≡ charsInBase base {base≥2} {base≤16} m → n ≡ m
+  charsInBase-injective n m = toDigits-injective base {base≥2} _ _
+                            ∘ Listₚ.reverse-injective
+                            ∘ Listₚ.map-injective (showDigit-injective _ _ _)