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?

Answer 1

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