# How to prove that the reversal of the concatenation of two strings is the concatenation of the reversals?

Given languages $L_1$ and $L_2$, how do we prove that $$(L_1L_2)^{\mathrm{rev}} = (L_2^{\mathrm{rev}})(L_1^{\mathrm{rev}})\,,$$ where ${}^{\mathrm{rev}}$ denotes reversal?

I think using mathematical induction, it can be shown true for two languages $L_1$ and $L_2$ of length $1$ each and then do induction using one of the lengths and then repeat with the other length. Is there any other way of proving this in a simpler way without making it too big with induction method?

Well, consider the following "proof" (I'll explain afterwords why the quotation marks):

Let $w=a_1\cdots a_n$ be a word, then we have that

$w\in (L_1L_2)^{\mathrm{rev}}$ iff

$a_n\cdots a_1\in L_1L_2$, iff

there exists $0\le k\le n$ such that $a_n\cdots a_k\in L_1$ and $a_{k-1}\cdots a_1\in L_2$, iff

there exists $0\le k\le n$ such that $a_k\cdots a_n\in L_1^{\mathrm{rev}}$ and $a_{1}\cdots a_ {k-1}\in L_2^{\mathrm{rev}}$, iff

$a_1\cdots a_n\in L_2^{\mathrm{rev}}L_1^{\mathrm{rev}}$ iff

$w\in L_2^{\mathrm{rev}}L_1^{\mathrm{rev}}$

In my opinion, this proof is correct, formal, and would be accepted as a proof of the claim.

However, each "iff" along the way (apart from the last one) actually hides an inductive proof. The point is that each of these inductions is extremely trivial. In fact, even writing $w=a_1\cdots a_n$ actually hides some induction. So you need to ask yourself how "deep" do you want to go into the technicalities.

If you want to prove this claim from basic principles, i.e. from the axioms of set theory, then you need to formalize everything. This would be very painful, but such things are actually useful when we use computer-assisted proofs.

• "However, each "iff" along the way (apart from the last one) actually hides an inductive proof." -- I'm a stickler for rigor, but I don't see it here. What would you want to perform induction over? The way I see it, the proof goes through for arbitrary $n$. – Raphael Aug 24 '16 at 10:34
• Well, for example, the (formal) definition of the reverse operation is inductive. That is, $\sigma'=\sigma$, and $(w\sigma)'=\sigma w'$. Now we can define the reverse of a language, but the claim $a_1\cdots a_n\in L$ iff $a_n\cdots a_1\in L'$ still needs to be proved by induction over $n$. But perhaps I was indeed exaggerating - the second and fourth "iff" are by definition of concatenation, and not by induction. – Shaull Aug 24 '16 at 10:37
• @Shaull You could choose an inductive definition of reversal but why would you want to? I'd much rather choose to define the reversal of $a_1\dots a_k$ to be $a_k\dots a_1$ and be done with it. – David Richerby Aug 24 '16 at 11:20
• @DavidRicherby - Right, but the definition of $a_1\cdots a_k$ as a word, or as an $n$-tuple, is inductive on $n$. That is, a Cartesian product of length $n$ is defined by induction on $n$, so you're just pushing the induction to a lower level. – Shaull Aug 24 '16 at 11:37
• I would even avoid splitting the string into its letters. Observing that for two words $w_1\in L_1$ and $w_2\in L_2$ we have $(w_1w_2)^{rev} = w_2^{rev} w_1^{rev}$ should be enough? – Hendrik Jan Aug 24 '16 at 14:33

I know that we already have an solution to this problem, but the above solution's comments inspired me to write this presentation.

The sequences over a type X are defined to be the free monoid over X. In particular, this means we have a monoid List X with a binary operation denoted _++_, unit denoted [], and singelton embedding x ↦ [x]. ─this is the common notation in the functional programming community.

Since every element of this monoid ─ie every sequence─ is either empty, a singelton, or a catenation, we can define the reverse inductively by

_ʳᵉᵛ : List X → List X
[]ʳᵉᵛ = []
[x]ʳᵉᵛ = [x]
(u ++ v)ʳᵉᵛ = v ʳᵉᵛ ++ u ʳᵉᵛ


Then we can calculate the desideratum as follows:

   (L₁ · L₂)ʳᵉᵛ
=⟨ direct image definition ⟩
{ (u ++ v)ʳᵉᵛ ❙ u ∈ L₁ ∧ v ∈ L₂}
=⟨ definition of _ʳᵉᵛ ⟩
{ v ʳᵉᵛ ++ u ʳᵉᵛ ❙ u ∈ L₁ ∧ v ∈ L₂}
=⟨ dummy renaming ⟩
{ v ʳᵉᵛ ʳᵉᵛ ++ u ʳᵉᵛ ʳᵉᵛ ❙ u ʳᵉᵛ ∈ L₁ ∧ v ʳᵉᵛ ∈ L₂ }
=⟨ ʳᵉᵛ is an involution as can be easily checked ⟩
{ v ++ u ❙ u ʳᵉᵛ ∈ L₁ ∧ v ʳᵉᵛ ∈ L₂ }
=⟨ direct image definition ⟩
{ v ++ u ❙ u ∈ L₁ ʳᵉᵛ ∧ v ∈ L₂ ʳᵉᵛ }
=⟨ symmetry of conjunction ⟩
{ v ++ u ❙ v ∈ L₂ ʳᵉᵛ ∧ u ∈ L₁ ʳᵉᵛ }
=⟨ definition of language catenation ⟩
L₂ ʳᵉᵛ · L₁ ʳᵉᵛ


I just wanted to mention this alternative view of sequences :-)