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

问题背景 #

我在Agda程序中定义了一个用于检查字符串相等性的简化函数foo：

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"

后续需要对涉及foo的逻辑进行证明：当传入两个相等的字符串时，需证明does (a ≈? a)求值为true，进而foo返回"Hello"，因此需要完成中间引理的证明：

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

但我无法完成该证明。标准库中存在多种字符串相等性定义（_≟_、_≈?_、_≈_），也能找到部分等价关系的自反性证明（如Data.String.Properties.≈-refl），但不知如何应用到我的定理中。

我的问题：

• 我使用的字符串相等检查是否为正确/常规的方式？
• 如何证明该定理？推测标准库中已有相关证明，但我未找到。

已获得的解决方案（编辑补充） #

TL;DR #

使用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})

-- 随后在foo定义中使用==
foo : String → String → String
foo a b = if (a == b)
          then "Hello"
          else "Bye"

为验证证明可行性，我尝试了以下代码：

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

发现≟-refl和==-refl的证明其实多余，直接使用_==_即可在运行时比较字符串。但面对标准库中至少5种字符串相等性定义（_≟_、_≈?_、_≈_、_==_、primStringEquality），我仍不清楚它们的适用场景。

内容的提问来源于stack exchange，提问作者PaulProgrammerNoob