[ new ] postulate length-tail lemma (#1366)

Author: gallais

CHANGELOG.md

@@ -288,3 +288,15 @@ Other minor additions
   ```
 
 * Added infix declarations to `Data.Product.∃-syntax` and `Data.Product.∄-syntax`.
+
+* Added new functions to `Data.String.Base`:
+  ```
+  uncons : String → Maybe (Char × String)
+  head   : String → Maybe Char
+  tail   : String → Maybe String
+  ```
+
+* Added new property to `Data.String.Unsafe`:
+  ```agda
+  length-tail : length s ≡ maybe′ (suc ∘′ length) zero (tail s)
+  ```

src/Data/String/Base.agda

@@ -11,7 +11,9 @@ module Data.String.Base where
 open import Level using (zero)
 open import Data.Bool.Base using (true; false)
 open import Data.Bool.Properties using (T?)
+open import Data.Maybe.Base as Maybe using (Maybe)
 open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉; _⊔_)
+open import Data.Product using (proj₁; proj₂)
 open import Data.List.Base as List using (List; [_])
 open import Data.List.NonEmpty as NE using (List⁺)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise)
@@ -60,6 +62,14 @@ _<_ = Lex-< Char._≈_ Char._<_ on toList
 ------------------------------------------------------------------------
 -- Operations
 
+-- List-like operations
+
+head : String → Maybe Char
+head = Maybe.map proj₁ ∘′ uncons
+
+tail : String → Maybe String
+tail = Maybe.map proj₂ ∘′ uncons
+
 -- Additional conversion functions
 
 fromChar : Char → String

src/Data/String/Unsafe.agda

@@ -10,12 +10,21 @@ module Data.String.Unsafe where
 
 import Data.List.Base as List
 import Data.List.Properties as Listₚ
-open import Data.Nat.Base using (_+_)
+open import Data.Maybe.Base using (maybe′)
+open import Data.Nat.Base using (zero; suc; _+_)
+open import Data.Product using (proj₂)
 open import Data.String.Base
+open import Function.Base using (_∘′_)
 
 open import Relation.Binary.PropositionalEquality; open ≡-Reasoning
 open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)
 
+------------------------------------------------------------------------
+-- Properties of tail
+
+length-tail : ∀ s → length s ≡ maybe′ (suc ∘′ length) zero (tail s)
+length-tail s = trustMe
+
 ------------------------------------------------------------------------
 -- Properties of conversion functions