CODEWITHSUNDEEP
reverseagdatheorem
JrPtn
JrPtn

Reputation: 83

Agda - Reverse-helper

I'm trying to prove this lema

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

But another function, reverse-helper keeps coming up into my goal and I have no idea how I get rid of it. Any guidance or suggestions?

Upvotes: 0

Views: 343

Answers (2)

Sassa NF
Sassa NF

Reputation: 5406

I think you should start with the different argument.

Since ++ is probably defined with [] ++ a = a, and reverse (x :: xs) = (reverse xs) ++ (x :: nil) it will be better to prove reverse-++ (x :: xs) ys = cong (\xs -> xs ++ (x :: nil)) (reverse-++ xs ys)

Upvotes: 0

Toxaris
Toxaris

Reputation: 7266

I'm assuming that in the implementation of reverse, you call reverse-helper. In that case, you probably want to prove a lemma about reverse-helper that you can call in the lemma about reverse. This is a general thing: If you are proving something about a function with a helper function, you usually need a proof with a helper proof, because the induction structure of the proof usually matches the recursion structure of the function.

Upvotes: 1

Related Questions