In my Agda program, I have a small function that checks for string equality (simplified for example):

open import Data.String.Base using (String)
open import Date.String.Properties using (_≈?_)
open import Relation.Nullary.Decidable using (does)

foo : String → String → String
foo a b = if (does (a ≈? b))
          then "Hello"
          else "Bye"

Later in my program, I want to prove something that involves foo. In particular, foo is applied to two equal strings and thus I want to show that does (a ≈? a) evaluates to true and thus foo returns "Hello". So as an intermediate step, I want to prove the reflexivity of foo:

foo-refl : ∀ {a : String} → true ≡ does (a ≈? a)
foo-refl = ?

However, I fail to prove it. When exploring the standard library I see different ways for equality of strings (_≟_, _≈?_, _≈_). Also, I saw proofs for reflexivity for some of these equivalence relations in the standard library, for example Data.String.Properties.≈-refl, but I fail to apply them to prove my theorem above.

So my questions are:

1. Am I using the right/convential kind of equality-check for strings?
2. How to prove my theorem? I guess it is already proven in the standard library but I fail to see it.

Edit

Thanks to @gallai's answer below, I came up with the following solution:

TL;DR: Use _==_ from Data.String.Properties to check equality of strings at runtime.

Long version:

open import Data.Bool using (Bool; true; if_then_else_)
open import Data.String.Base using (String)
open import Data.String.Properties using (_≟_; _==_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable using (yes; isYes)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; ≡-≟-identity)

≟-refl : ∀ {S : String} → (S ≟ S) ≡ yes refl
≟-refl = ≡-≟-identity _≟_ refl

==-refl : ∀ {S : String} → (S == S) ≡ true
==-refl {S} = cong isYes (≟-refl {S})

-- And then use == in the definition of foo.
foo : String → String → String
foo a b = if (a == b)
          then "Hello"
          else "Bye"

To check that I can now make proofs on foo, I tried the following:

_ : "Hello" ≡ foo "gallais" "gallais"
_ = refl

realizing that the proofs of ≟-refl and ==-refl are superfluous. So one can just use _==_ to compare strings during runtime. This was not (and still is not really) clear to me when facing at least five different definitions of string equality in the standard library: _≟_, _≈?_, _≈_, _==_, primStringEquality.

CodePudding user response：

You can use the generic proof defined in Relation.Binary.PropositionalEquality:

module _ (_≟_ : DecidableEquality A) {x y : A} where
  ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq