I've seen an example of the inspect function in my last question Using the value of a computed function for a proof in agda , but I'm still having trouble wrapping my head around that.
Here's a simple example:
Given the function crazy,
crazy : ℕ -> ℕ
crazy 0 = 10
crazy 1 = 0
crazy 2 = 0
crazy 3 = 1
crazy 4 = 0
crazy xxx = xxx
I want to create a safe function such that safe : {nn : ℕ} -> (id nn) ≢ 0 -> Fin (id nn). In other words it will return one number mod crazy, if you give it a proof crazy is 0. (I know that the example is a little contrived and I would probably be better off using the suc in the function signature)
My first solution is
safebad : {nn : ℕ} -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safebad {1} hh with hh refl
... | ()
safebad {2} hh with hh refl
... | ()
safebad {4} hh with hh refl
... | ()
safebad {0} hh = # 0
safebad {3} hh = # 0
safebad {suc (suc (suc (suc (suc _))))} _ = # 0
But this is long and messy. So I tried to emulate the example in Using the value of a computed function for a proof in agda but could only get so far
safegood : (nn : ℕ) -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim ???
... | _ | _ = # 0
inspect uses Hidden to hide a record of the function application in the type signature, I think. This can then be retrieved with reveal.
This is what I think I understand:
Reveal_is_ seems to hold the value of the hidden f, and x; and the result of x applied to f. [_] will result in the proof of that equality.
⊥-elim takes a proof of contradiction and returns a contradiction.
What do I put into ??? for this to work?
You are making it needlessly complicated. inspect is only useful when you need to use the proof that the value before pattern matching is equal to the value after pattern matching. Notice that you have nez in the scope which makes this trivial.
What we really want to do is to reduce the assumption crazy nn ≢ 0 to 0 ≢ 0 which we can easily use to construct a contradiction. How do we get crazy nn to reduce to 0? You have already tried the first option - go through all possible crazy arguments and fish for those that indeed reduce crazy nn to 0. The other option is to simply abstract over the value of crazy nn.
First, the goal type before we use with is Fin (crazy nn) and the type of nez is crazy nn ≢ 0. Now, we abstract over crazy nn:
safegood nn nez with crazy nn
... | w = ?
Notice our goal is now Fin w and nez's type is w ≢ 0, much easier to work with! And finally, we pattern match on w:
safegood nn nez with crazy nn
... | zero = ?
... | suc w = ?
The first goal is now Fin 0 and we have a 0 ≢ 0 as one of our assumptions. This is obviously a nonsense, combining nez with refl gives us a contradiction that can be used by ⊥-elim:
safegood nn nez with crazy nn
... | zero = ⊥-elim (nez refl)
... | suc w = ?
No inspect in sight! In fact, using inspect here is like making a round trip: you reduce crazy nn to 0 in the types, get a proof that crazy nn ≡ 0 and now you need to "unreduce" 0 back to crazy nn so that you can use nez proof.
For the sake of completeness: you can avoid pattern matching on crazy nn to keep the type of the proof nez intact by using the deprecated inspect:
open Deprecated-inspect
renaming (inspect to inspect′)
safegood₂ : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood₂ nn nez with inspect′ (crazy nn)
... | zero with-≡ eq = ⊥-elim (nez eq)
... | suc _ with-≡ eq = ?
Since we abstract over inspect′ (crazy nn), no crazy nn subexpressions will get substituted and nez will keep its original type.
Talking about crazy roundtrips: you could use proof to reconstruct nez's original type; again, this is more of a "might be useful to know" than "use this here":
safegood : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim (subst (λ x → x ≢ 0) (sym proof) nez proof)
... | _ | _ = ?