2017-05-09 10 views
2

としてhttps://homes.cs.washington.edu/~jrw12/InductionExercises.htmlとしてsumsum_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を使用することを奨励しています。これは内部書き換えを適用するまで外側の部分を同様にすることはできません。

+2

あなたはラムダの下に書き換えることができません:

sum_cont_correct' : (k : Nat -> ty) -> (xs : List Nat) -> sum_cont' xs k = k (sum xs) sum_cont_correct' k [] = Refl sum_cont_correct' k (x :: xs) = sum_cont_correct' (k . (x+)) xs 

は今sum_cont_correct補題の証明はちょうどワンライナーです機能的な拡張性の公理(あなたがリンクした答えはそれを非常に詳細に説明している)を仮定すること。しかし、公理やセトイドのような他の機械を使わずに証明を行うことができます。スポイラー警告:[ここ](https://gist.github.com/anton-trunov/0c2d21b770d350646e5f0a4e8a8072f4)は、可能なアプローチを示す要点です。 –

+1

ありがとう!それを答えに変えることができますか?私はそれが正しいことだと思う。リンクされた質問が本当に答えないのは、Idrisが機能的な拡張性を備えていない理由です。https://www.reddit.com/r/haskell/comments/3jw3xm/dependent_haskell_vs_idris/cusvunr/それをカバーするようです。 –

答えて

1

機能的拡張性の公理を引き受けるつもりがない限り、ラムダ下では書き直すことはできません。私の意見では、あなたがリンクした答えがそのことをとてもうまく説明します。

ところで、関連システム - Coqにバインダーの下で書き直しを容易にする機能(戦術)があります(this answerで説明しようとしました)。しかし、私はIdrisでそのアナログを認識していません。

しかし、次のように公理や定型文のような他の機械を使わずに証明を行うことができます。

のは、最初のより一般的な補題を証明してみましょう:あなたが喜んでいる場合を除き

sum_cont_correct : (xs : List Nat) -> sum_cont xs = sum xs 
sum_cont_correct = sum_cont_correct' id 
+1

FWIW、 '(+ x)​​'の代わりに '(x +)'を使うと、あなたは共通性を必要としません。 – user1502040

+0

ありがとう!私は 'sum_cont '(x :: xs)k = sum_cont' xs(k。(x +))'を使っていたはずです。 '...(+ x)​​...'の代わりに –

関連する問題