reverse - Agda - リバースヘルパー

Question

私はこのレマを証明しようとしています

reverse-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 :  A) → reverse (l1 ++ l2) ≡ (reverse l2) ++ (reverse l1)     
reverse-++ [] [] = refl
reverse-++ l1  [] rewrite ++[] l1 = refl
reverse-++ l1 (x :: xs) =  {!!}

しかし、別の関数である reverse-helper が目標に到達し続けており、それを取り除く方法がわかりません。ガイダンスや提案はありますか？

Answer 1

reverseの実装では、 を呼び出すと想定していますreverse-helper。reverse-helperその場合、補題 aboutで呼び出すことができる補題 about を証明したいと思うでしょうreverse。これは一般的なことです。ヘルパー関数を使用して関数について何かを証明する場合、通常、ヘルパー証明を使用した証明が必要になります。証明の帰納構造は通常、関数の再帰構造と一致するからです。

Answer 2

別の議論から始めるべきだと思います。

++はおそらく で定義されて[] ++ a = aいるためreverse (x :: xs) = (reverse xs) ++ (x :: nil)、証明したほうがよいでしょう。reverse-++ (x :: xs) ys = cong (\xs -> xs ++ (x :: nil)) (reverse-++ xs ys)