Agda-stdlib: Safe proofs of decidable equality for String & Char.

[andreasabel]

The latest master removed Data.String._≟_. I found in Data.String.Unsafe. I'd consider it safe.

[MatthewDaggitt]

If only the safety checker agreed with you :laughing:

In all seriousness though, I agree with you. We need to find a way of finding a way of coming up with useful, safe equality checks for primitives.

[gallais]

We "just" need primitive proofs that primStringToList and primChartoNat are injective
and then we will be able to resurrect Data.Char._≟_ and Data.String._≟_.

The types are fairly simple and we can implement the functions internally by re-using trustMe
so it shouldn't be too much work!

open import Agda.Builtin.String
open import Agda.Builtin.Char

open import Function

import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

import Data.List.Relation.Pointwise as List
import Data.Nat as ℕ

postulate

  primStringToList-injective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b
  primCharToNat-injective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b

char? : Decidable {A = Char} _≡_
char? x y = Dec.map′ (primCharToNat-injective x y) (cong primCharToNat)
          $ primCharToNat x ℕ.≟ primCharToNat y

string? : Decidable {A = String} _≡_
string? x y = Dec.map′ (primStringToList-injective x y) (cong primStringToList)
            $ List.decidable-≡ char? (primStringToList x) (primStringToList y)

[MatthewDaggitt]

I assume it's too late to add these to Agda-2.6.0 as these functions probably count as a feature?

[gallais]

Indeed. We do have safe primEraseEquality though and should be able to make
Data.Nat.Unsafe safe as well as its dependencies.

[nad]

If the K rule is enabled.

[MatthewDaggitt]

Closed with 39c0a10