Агда - обратный помощник

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) =  {!!}

Но другая функция, обратный помощник, продолжает приближаться к моей цели, и я понятия не имею, как мне от нее избавиться. Любое руководство или предложения?

Answer 1

Я предполагаю, что при реализации reverse, ты звонишь reverse-helper, В этом случае вы, вероятно, хотите доказать лемму о reverse-helper что вы можете назвать в лемме о reverse, Это общая вещь: если вы доказываете что-то о функции с помощью вспомогательной функции, вам обычно требуется доказательство с вспомогательным доказательством, потому что индукционная структура доказательства обычно совпадает с рекурсивной структурой функции.

Answer 2

Я думаю, что вы должны начать с другого аргумента.

поскольку ++ вероятно, определяется с [] ++ a = a, а также reverse (x :: xs) = (reverse xs) ++ (x :: nil) будет лучше доказать reverse-++ (x :: xs) ys = cong (\xs -> xs ++ (x :: nil)) (reverse-++ xs ys)