前回の質問Using the value of a compute function for aproof in agdaでinspect 関数の例を見てきましたが、それでも頭を悩ませています。
簡単な例を次に示します。
関数 を考えるとcrazy、
crazy : ℕ -> ℕ
crazy 0 = 10
crazy 1 = 0
crazy 2 = 0
crazy 3 = 1
crazy 4 = 0
crazy xxx = xxx
safeというような関数を作りたいですsafe : {nn : ℕ} -> (id nn) ≢ 0 -> Fin (id nn)。つまり、crazy が 0 であることを証明すると、1 つの number mod crazy が返されますsuc。
私の最初の解決策は
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
しかし、これは長くて厄介です。だから私は agda での証明のために計算された関数の値を使用する の例をエミュレートしようとしましたが、これまでしか得られませんでした
safegood : (nn : ℕ) -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim ???
... | _ | _ = # 0
inspect は Hidden を使用して、関数適用の記録を型シグネチャに隠していると思います。これは、reveal で取得できます。
これは私が理解していると思うものです：
Reveal_is_hidden f、 andの値を保持しているようxです。xと に適用された結果f。 [_]その等式の証明になります。
⊥-elim矛盾の証明を取り、矛盾を返します。
これが機能するために何を入れ???ますか？