How to prove things about primitive strings?

Question

On Idris, it is not possible to perform pattern matching against primitive strings. As such, it is not obvious how to prove things about them. For example, this function may return a proof that the first character of a list of chars is 'a':

f : (l : List Char) -> Maybe (head' l = Just 'a')
f ('a' :: []) = Just Refl
f xs          = Nothing

Which is pretty simple and passes the type checker. If we try to implement the same thing for native strings, though, we'll write something like this:

g : (s : String) -> Maybe (prim__strHead s = 'a')
g s = if prim__strHead s == 'a'
  then Just Refl 
  else Nothing

Which fails to typecheck because the compiler obviously can't conclude prim__strHead s == 'a' just from the fact it passed the prim__strHead s == 'a' test.

What is, thus, the proper way to prove things about primitive strings?

Instead of using Maybe for the proof, use Dec: f : (l : List Char) -> Dec (head' l = Just 'a') f ('a' :: xs) = Yes Refl f [] = No absurd — asandroq
@asandroq any link explaining what is Dec and when/why should I use it? — MaiaVictor

Alexander Gryzlov Alexander Gryzlov · Accepted Answer · 2018-01-05T14:01:10

As suggested on IRC, you could use Data.String.Views.strList to pattern match on strings:

import Data.String.Views

g : (s : String) -> ...
g s with (strList s) 
 g ""            | SNil = ?no
 g (strCons x _) | SCons x _ with (decEq x 'a') 
   g (strCons 'a' _) | SCons 'a' _ | Yes Refl = ?yes
   g (strCons  x  _) | SCons  x  _ | No contra = ?no2

How to prove things about primitive strings?

1 Answers