私は最近、この質問をしました: 型で使用される agda 命題 -- それはどういう意味ですか? 型を暗黙的にして実際のコンパイル時エラーを取得する方法について、非常によく考えられた回答を受け取りました。
ただし、依存型で値を作成する方法はまだ不明です。
検討：
div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()
ここで、N は自然数で、偶数は次の命題です。
even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where
次のように関数を書きたいとします。
f : N -> N
f n = if even n then div n else div (succ n)
このようなことを自分のやりたいように行う方法がわかりません... 私の目には、(not (even n)) \to even (succ n) という証拠を持つことが最善の方法です。これをagdaで表現する方法がよくわかりません。私は書くことができます
g : (n:N) -> (even n) -> (even (succ n)) -> N
g n p q = if evenB n then (div n p) else (div (succ n) q)
これから、次のようなことができます。
g 5 _ _
通常の形式に評価して...答えを得る。f と書きたい場合は、次のようにします。
f n = g n ? ?
fn = gn { }1 { }2 ここで、?1 = 偶数 n、?2 = 偶数 (成功 n) です。次に、f Five などを実行して、正規形に評価できます。なぜこれが有効なのかよくわかりません...この方法で定義された f に関する詳細情報をagdaに伝える方法はありますか。?1 が失敗した場合 ?2 が成功することを確実に伝えることができるので、f の評価は常に意味があることを agda に伝えることができますか?
g は、n が偶数であるという証明、(succ n) が偶数であるという証明を取り、数値を返す関数として g を解釈します。（これはこれを読む正しい方法ですか？または誰かがこれを読むためのより良い方法を提案できますか？）上記の型がどのようにチェックするかを正確に（またはより正確に）理解したいと思っています。それは誘導を使用しますか? (evenB n) を p : even n と接続しますか?? などなど、わかっているので今のところ戸惑っています。
if evenB n then (div n q) else (whatever)
if evenB n then div (succ n) q else div n p
間違っています。最初に理由を理解しました - q は succ n のためのものなので、一致しません。しかし、2 番目は失敗し、その理由はもっと不可解で、Agda は私が想像していたよりも強力なようです...
これは、私がその方法を理解できれば（それが理にかなっている場合）、本当に好きな最初のステップです。
g : (n : N) -> (even n) -> N
g n p = if evenB n then (div n p) else (div (succ n) (odd p))
ここで、奇数 p は、偶数 n がばかげている場合、成功数 n が偶数であることの証明です。これには、依存型の値を操作できる必要があると思います。
最終的には、次のように書けるようになりたいと思っています。
g : N -> N
g n =
let p = proofthat n is even
in
if evenB n then div n p else (div (succ n) (odd p))
または、それらの線に沿った何か。あるいは
g : N -> N
g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q
プログラムで使用できるように、依存型に対応する証明を作成する方法を知りたいです。助言がありますか？