How does one use the with inspect in Agda?

Question

I'm trying to reproduce a very simple coq proof from Programming foundations in agda, and was told I need to use the with inspect to prove a contradction from the pattern match on the (bool) decideablity of a string with itself. I'm getting the below error, and the documentation doesn't even give a proper program using with with inspect. Why is this type inference incorrect, and how can I resolve my error?

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  = {!!}

The (s == s) is highlighted red and yields the following error

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

Jesper Jesper · Accepted Answer · 2020-04-10T07:46:04

The inspect function in the standard library has the following type:

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

As you can see, it takes two explicit arguments: a function f and a value x. The user manual has a section on how to use the inspect idiom, specifically the second example uses essentially the same definition of inspect as the standard library.

How does one use the with inspect in Agda?

2 Answers