How does agda test a function?

Question

I saw an example of a validation function in my last question Using the value of a computed function for proof in agda , but I still have a wrapping problem around me.

Here is a simple example:

For crazy function,

 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, he will return a single number crazy if you give him the proof of crazy 0. (I know this example is a bit far-fetched, and I probably would be better off using suc in the function signature)

My first decision 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 it is long and erratic. So I tried to imitate the example in Using the value of a computed function for proof in agda , but maybe only so far

 safegood : (nn : ℕ) -> (crazy nn) ≢ 0 -> Fin (crazy nn) safegood nn nez with crazy nn | inspect crazy nn ... | 0 | [ proof ] = ⊥-elim ??? ... | _ | _ = # 0 

I think that

verifies the use of Hidden to hide the function application entry in the type signature. This can then be obtained through disclosure.

Here is what I think I understand:

Reveal_is_ seems to preserve the value of hidden f and x ; and the result x applied to f . [_] will lead to the proof of this equality.

⊥-elim accepts the proof of contradiction and returns the contradiction.

What can I add in ??? for this?

Answer 1

You make it uselessly complicated. inspect is only useful when you need to use proof that the value before matching patterns is equal to the value after matching pattern. Note that you have nez in the area that makes this trivial.

What we really want to do is reduce the crazy nn ≢ 0 to 0 ≢ 0 , which we can easily use to construct the contradiction. How do we get crazy nn to decrease to 0 ? You have already tried the first option - go through all possible crazy arguments and catch the fish for those that really reduce crazy nn to 0 . Another option is to simply ignore the crazy nn value.

First, the type of the target before using with is Fin (crazy nn) , and the type of nez is crazy nn ≢ 0 . Now we are abstracting over crazy nn :

 safegood nn nez with crazy nn ... | w = ? 

Please note that our goal is now Fin w and nez type is w ≢ 0 , which is much easier to work with! And finally, we map the pattern to 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 nonsense, combining nez with refl gives us a contradiction that ⊥-elim can use:

 safegood nn nez with crazy nn ... | zero = ⊥-elim (nez refl) ... | suc w = ? 

No inspect in sight! In fact, using inspect here is like a round trip: you reduce crazy nn to 0 in types, get proof that crazy nn ≡ 0 , and now you need to “free” 0 back to crazy nn so you can use nez proof .

---

For completeness: you can avoid matching patterns on crazy nn to keep the nez proof type intact using the outdated 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) , the no crazy nn subexpressions will be replaced, and nez retain its original type.

---

Speaking of crazy rounds: you can use proof to restore nez original type; again, it is more likely to be “useful to know” than to “use it 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) ... | _ | _ = ?