如何在 Agda 中使用 with inspect ？答案

【问题标题】：How does one use the with inspect in Agda?如何在 Agda 中使用 with inspect ？
【发布时间】：2020-04-09 23:41:11
【问题描述】：

我正在尝试从 Agda 中的 Programming Foundations 中重现一个非常简单的 coq 证明，并被告知我需要使用 with inspect 来证明与字符串自身的 (bool) 可判定性上的模式匹配的矛盾。我收到以下错误，文档甚至没有给出使用 with inspect 的正确程序。为什么这种类型推断不正确，我该如何解决我的错误？

module Maps where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst; trans; sym; inspect)
open import Data.String using (_++_; _==_; _≟_; String)
open import Data.Bool using (T; Bool; true; false; if_then_else_)

-- Coq-- Theorem eqb_string_refl : forall s : string, true = eqb_string s s.
eqbstringrefl' : (s : String) →  true ≡ (s == s)
eqbstringrefl' s with inspect (s == s) 
... | false with≡ eq = {!!}
... | true with≡ eq  = {!!}

(s == s) 以红色突出显示并产生以下错误

Bool !=< (x : _A_70) → _B_71 x of type Set
when checking that the inferred type of an application
Bool
matches the expected type
(x : _A_70) → _B_71 x

【问题讨论】：

标签： pattern-matching coq type-inference agda

【解决方案1】：

标准库中的inspect函数有以下类型：

inspect : ∀ {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x

如您所见，它有两个显式参数：一个函数f 和一个值x。 user manual 有一节介绍如何使用检查习语，特别是第二个示例使用与标准库基本相同的 inspect 定义。

【讨论】：

【解决方案2】：

标准库有一个README dealing with the inspect idiom。

【讨论】：