I was doing a code exercise in Agda from the PLFA, to implement a proof that "the reverse of one list appended to another is the reverse of the second appended to the reverse of the first".
reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
I was able to do the first two induction cases without problems:
reverse-++-distrib {A} [] ys
reverse-++-distrib xs []
but the third step has a "Termination checking failed" error, which I guess means that the inductive step is not done correctly.
reverse-++-distrib {A} (x :: xs) ys =
begin
reverse ((x :: xs) ++ ys)
≡⟨⟩
reverse (x :: (xs ++ ys))
≡⟨⟩
reverse (xs ++ ys) ++ [ x ]
≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
(reverse ys ++ reverse xs) ++ [ x ]
≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
reverse ys ++ (reverse xs ++ [ x ])
≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
(reverse ys) ++ (reverse xs ++ (reverse [ x ]))
**≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩**
(reverse ys) ++ (reverse ([ x ] ++ xs))
≡⟨⟩
(reverse ys) ++ (reverse (x :: ([] ++ xs)))
≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
(reverse ys) ++ (reverse (x :: xs))
∎
The problematic call aparently is this:
reverse-++-distrib {A} (x :: []) xs
To me this looks fine because the length of the first argument is 1, which is smaller than or equal to the length of x :: xs. And it is only equal if xs is the empty list, in which case it should enter in the second pattern matching. So why is agda having problems with this definition?
To me this looks fine because the length of the first argument is 1, which is smaller than or equal to the length of x :: xs. And it is only equal if xs is the empty list, in which case it should enter in the second pattern matching. So why is agda having problems with this definition?
Agda is quite far from being able to guess this sort of argument out of thin air. The termination checker only ensures that the arguments to the function get structurally smaller with each call (once suitably lexicographically ordered), but your function doesn't meet that requirement because x ∷ [] is not structurally smaller than x ∷ xs (it can be equal, as you noticed).
You may think this is restrictive, but it often reveals a more natural way to structure programs and proofs: for example, here, you can work around this by turning reverse-++-distrib [ x ] xs into a separate lemma reverse-∷-distrib x xs : reverse (x ∷ xs) ≡ reverse xs ++ [ x ].
P.S.: your last step is just refl, since [] ++ xs = xs by definition.