Substituting two different identifiers with the same identifier in Coq - why does this work?

Question

I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever.

To prove

Theorem app_length_cons : forall (X:Type) (l1:list X) (x:X),
                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).

we can first prove

Theorem app_length_cons' : forall (X:Type) (l1 l2:list X) (x:X),
                             length (l1 ++ x :: l2) = S (length (l1 ++ l2)).

which is a straightforward induction,

Proof.
  intros.
  induction l1 as [| h l1'].
  reflexivity.
  simpl.
  rewrite -> IHl1'.
  reflexivity.
Qed.

Then simply

Proof.
  intros.
  apply app_length_cons' with (l1:=l1) (l2:=l1).
Qed.

However, there is something strange going on here - in the induction proof, we are doing induction on l1 and not l2 - and from the proof, it looks like we are assuming l2 doesn't change in the induction case. But when we later apply it with l2:=l1, we are breaking this assumption.

Indeed, if we try to prove

Theorem app_length_cons'' : forall (X:Type) (l1:list X) (x:X),
                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).

use the same method

Proof.
  intros.
  induction l1 as [| h l1'].
  reflexivity.
  simpl.
  -- Can't rewrite use IHl1' : length (l1' ++ x :: l1') = S (length (l1' ++ l1')),
  -- since the goal is S (length (l1' ++ x :: h :: l1')) = S (S (length (l1' ++ h :: l1')))

it looks like the assumption that l2 doesn't change is broken thus the proof won't work.

I'm pretty sure I'm missing something here. Why can we substitute different identifiers with the same identifier?

Answer 1

it looks like we are assuming l2 doesn't change in the induction case. But when we later apply it with l2:=l1, we are breaking this assumption.

No. If we regard l1 to be a value which is repeatedly decreased in the induction proof, note that we let l2 to be equal to the initial value of l1 -- such value will not change in the induction steps. In other words: the value of l1 will decrease, but l2 will always be the initial value of l1.

We can even compare it with recursion in programming:

# pseudocode
def f(x, y):
   if x==0: return baseValue
   use f(x-1, y)
   return something

Just because f(x, y) is defined by induction on x, it does not mean that later on we can't call f(a, a) where both arguments have the same value a.

Answer 2

(1) We are just using this general theorem to prove a special case, we don't change anything here. When we use this coq construction

apply app_length_cons' with (l1:=l1) (l2:=l1).

we just in some sense instantiate this universally quantified formula

$$ \forall l_1, l_2. \mid l_1 \cdot (x :: l_2) \mid~=~succ \mid l_1 \cdot l_2 \mid $$

with $l_2 = l_1$:

$$ \forall l_1. \mid l_1 \cdot (x :: l_1) \mid~=~succ \mid l_1 \cdot l_1 \mid. $$

(2) As for your last proof, it's often harder to prove a special case than a more general one. When you do induction on $l_1$ you get the head $h$ of the list $l_1$ twice. You can easily get rid of the first occurrence of $h$, but the second one is buried deeply inside concatenation.

By the way, you can still do one rewrite if you generalize the induction hypothesis in the variable $x$, but this seems to lead nowhere:

Theorem app_length_cons'' : forall (X:Type) (x:X) (l1:list X),
                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).
Proof.
  intros.
  generalize dependent x.
  induction l1 as [| h l1']; intro.
  reflexivity.
  simpl.
  rewrite IHl1' with (x := h).