Intuitively stating that xs is equal to ys is the same as saying that the respective reverse lists are equal to each other.
I'm currently learning Lean 4 and so I set myself the following exercise. I want to prove the following theorem in Lean 4:
theorem rev_eq (xs ys : List α) : (xs = ys) = (reverse xs = reverse ys)
However, I am not sure, whether this theorem can actually be proven in Lean 4. If not, why can it not be proven?
The closest I could get so far is proving the claim under the assumption that xs = ys:
theorem rev_eq' (xs ys : List α) :
xs = ys -> (xs = ys) = (reverse xs = reverse ys) := by
intros h
rw [h]
simp
Maybe, if one could prove that the claim also holds if one assumes that xs is not equal to ys, then the original theorem would follow. I got stuck on that route as well though.
Any ideas?
In Lean, it is usually idiomatic to state the equality of propositions using Iff, which is equivalent under the axiom propext. From there, iff is an inductive type with two sides, one direction that you have proved, and the other direction that follows from induction. (This theorem is still provable without this axiom, fwiw)
But I'd recommend you to do induction xs and induction ys and then look at the goals. Two should be impossible and Lean should show you they are contradictions (or indeed you'll get a that can be simplified to false = false) and two trivially true goals. Make sure to expand the definition of reverse.