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?