在 Agda 证明中应用字符串等价的自反性

问：

在我的 Agda 程序中，我有一个小函数来检查字符串是否相等（例如简化）：

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"

在我的程序的后面，我想证明一些涉及.特别是，应用于两个相等的字符串，因此我想表明它的计算结果为 ，从而返回 。因此，作为中间步骤，我想证明以下的自反性：foofoodoes (a ≈? a)truefoo"Hello"foo

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

但是，我未能证明这一点。在探索标准库时，我看到了字符串相等的不同方式（、、）。 此外，例如，我在标准库中看到了其中一些等价关系的自反性证明，但我未能应用它们来证明我上面的定理。_≟__≈?__≈_Data.String.Properties.≈-refl

所以我的问题是：

1. 我是否对字符串使用了正确/常规的相等性检查？
2. 如何证明我的定理？我想它已经在标准库中得到了证明，但我没有看到它。

编辑

多亏了@gallai下面的回答，我想出了以下解决方案：

TL;DR：使用 from 在运行时检查字符串的相等性。_==_Data.String.Properties

长版：

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"

为了检查我现在可以进行证明，我尝试了以下方法：foo

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

意识到 和 的证明是多余的。因此，可以在运行时用于比较字符串。在标准库中面对至少五个不同的字符串相等定义时，我并不清楚（现在仍然不清楚）：、、、、。≟-refl==-refl_==__≟__≈?__≈__==_primStringEquality