    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Explaining how to use the inspect idiom and elaborating on the way
    -- it is implemented in the standard library.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module README.Inspect where

    open import Data.Nat.Base
    open import Data.Nat.Properties
    open import Data.Product.Base using (_×_; _,_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
    open import Relation.Binary.PropositionalEquality using (inspect; [_])

    ------------------------------------------------------------------------
    -- Using inspect

    -- We start with the definition of a (silly) predicate: `Plus m n p` states
    -- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it
    -- distinguishes two cases: whether `p` is 0 or not.

    Plus-eq : (m n p : ℕ) → Set
    Plus-eq m n zero      = m ≡ 0 × n ≡ 0
    Plus-eq m n p@(suc _) = m + n ≡ p

    -- A sensible lemma to prove of this predicate is that whenever `p` is literally
    -- `m + n` then `Plus m n p` holds. That is to say `∀ m n → Plus m n (m + n)`.
    -- To be able to prove `Plus-eq m n (m + n)`, we need `m + n` to have either
    -- the shape `zero` or `suc _` so that `Plus-eq` may reduce.

    -- We could follow the way `_+_` computes by mimicking the same splitting
    -- strategy, thus forcing `m + n` to reduce:

    plus-eq-+ : ∀ m n → Plus-eq m n (m + n)
    plus-eq-+ zero   zero    = refl , refl
    plus-eq-+ zero   (suc n) = refl
    plus-eq-+ (suc m) n      = refl

    -- Or we could attempt to compute `m + n` first and check whether the result
    -- is `zero` or `suc p`. By using `with m + n` and naming the result `p`,
    -- the goal will become `Plus-eq m n p`. We can further refine this definition
    -- by distinguishing two cases like so:

    -- plus-eq-with : ∀ m n → Plus-eq m n (m + n)
    -- plus-eq-with m n with m + n
    -- ... | zero  = {!!}
    -- ... | suc p = {!!}

    -- The problem however is that we have abolutely lost the connection between the
    -- computation `m + n` and its result `p`. Which makes the two goals unprovable:

    -- 1. `m ≡ 0 × n ≡ 0`, with no assumption whatsoever
    -- 2. `m + n ≡ suc p`, with no assumption either

    -- By using the `with` construct, we have generated an auxiliary function that
    -- looks like this:
    -- `plus-eq-with-aux : ∀ m n p → Plus-eq m n p`
    -- when we would have wanted a more precise type of the form:
    -- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`.

    -- This is where we can use `inspect`. By using `with f x | inspect f x`,
    -- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`.
    -- Splitting on the result of `m + n`, we get two cases:

    -- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero`
    -- 2. `m + n ≡ suc p` under the assumption that `m + n ≡ suc p`

    -- The first one can be discharged using lemmas from Data.Nat.Properties and
    -- the second one is trivial.

    plus-eq-with : ∀ m n → Plus-eq m n (m + n)
    plus-eq-with m n with m + n | inspect (m +_) n
    ... | zero  | [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
    ... | suc p | [ m+n≡1+p ] = m+n≡1+p

    ------------------------------------------------------------------------
    -- Understanding the implementation of inspect

    -- So why is it that we have to go through the record type `Reveal_·_is_`
    -- and the ̀inspect` function? The fact is: we don't have to if we write
    -- our own auxiliary lemma:

    plus-eq-aux : ∀ m n → Plus-eq m n (m + n)
    plus-eq-aux m n = aux m n (m + n) refl where

      aux : ∀ m n p → m + n ≡ p → Plus-eq m n p
      aux m n zero    m+n≡0   = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
      aux m n (suc p) m+n≡1+p = m+n≡1+p

    -- The problem is that when we write ̀with f x | pr`, `with` decides to call `y`
    -- the result `f x` and to replace *all* of the occurences of `f x` in the type
    -- of `pr` with `y`. That is to say that if we were to write:

    -- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n)
    -- plus-eq-naïve m n with m + n | refl {x = m + n}
    -- ... | p | eq = {!!}

    -- then `with` would abstract `m + n` as `p` on *both* sides of the equality
    -- proven by `refl` thus giving us the following goal with an extra, useless,
    -- assumption:

    -- 1. `Plus-eq m n p` under the assumption that `p ≡ p`

    -- So how does `inspect` work? The standard library uses a more general version
    -- of the following type and function:

    record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where
      constructor [_]
      field eq : f x ≡ y

    my-inspect : ∀ f n → MyReveal f · n is (f n)
    my-inspect f n = [ refl ]

    -- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we
    -- write `with f n | inspect f n`, the only `f n` that can be abstracted in the
    -- type of `inspect f n` is the third argument to `Reveal_·_is_`.

    -- That is to say that the auxiliary definition generated looks like this:

    plus-eq-reveal : ∀ m n → Plus-eq m n (m + n)
    plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where

      aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p
      aux m n zero    [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
      aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p

    -- At the cost of having to unwrap the constructor `[_]` around the equality
    -- we care about, we can keep relying on `with` and avoid having to roll out
    -- handwritten auxiliary definitions.