としてhttps://homes.cs.washington.edu/~jrw12/InductionExercises.htmlとしてsum
とsum_cont
が同等であることを証明しようとしています。私が手に:Idrisでは、
sum_cont' xs (\ans => plus acc (plus x ans)) = plus (plus acc x) (sum xs)
私は書き換えplusAssociative acc x ans
を適用したいのですが、ans
は上部のスコープではありません:穴todo
が入力している
sum : List Nat -> Nat
sum [] = 0
sum (x :: xs) = x + sum xs
sum_cont' : {a : Type} -> List Nat -> (Nat -> a) -> a
sum_cont' [] k = k 0
sum_cont' (x :: xs) k = sum_cont' xs (\ans => k (x + ans))
sum_cont : List Nat -> Nat
sum_cont l = sum_cont' l (\x => x)
sum_cont_correct' : (xs : List Nat) -> (x : Nat) -> sum_cont' xs (\ans => plus x ans) = plus x (sum xs)
sum_cont_correct' [] acc = Refl
sum_cont_correct' (x :: xs) acc =
rewrite plusAssociative acc x (sum xs) in
?todo
。ラムダの下で書き直しを私がバインドできない変数にどのように適用すればよいですか?
質問How do I prove a "seemingly obvious" fact when relevant types are abstracted by a lambda in Idris?は、いくつかの同様の点に答えるようですが、cong
を使用することを奨励しています。これは内部書き換えを適用するまで外側の部分を同様にすることはできません。
あなたはラムダの下に書き換えることができません:
はは今
sum_cont_correct
補題の証明はちょうどワンライナーです機能的な拡張性の公理(あなたがリンクした答えはそれを非常に詳細に説明している)を仮定すること。しかし、公理やセトイドのような他の機械を使わずに証明を行うことができます。スポイラー警告:[ここ](https://gist.github.com/anton-trunov/0c2d21b770d350646e5f0a4e8a8072f4)は、可能なアプローチを示す要点です。 –ありがとう!それを答えに変えることができますか?私はそれが正しいことだと思う。リンクされた質問が本当に答えないのは、Idrisが機能的な拡張性を備えていない理由です。https://www.reddit.com/r/haskell/comments/3jw3xm/dependent_haskell_vs_idris/cusvunr/それをカバーするようです。 –