Coq: goal variable not transformed by induction when appearing on left side of arrow

Question

I am trying to prove the following theorem by induction over l. It's an easy theorem on paper, however when I try to prove it in Coq I am not getting the induction goal I would expect.

Theorem nodup_app__disjoint: forall {X: Type} (l: list X),
  (forall l1 l2 : list X, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.
Proof.
  intros X l. induction l.
  - intros F. apply nodup_nil.
  - (* ??? *)

The state at this point:

1 subgoal
X : Type
x : X
l : list X
IHl : (forall l1 l2 : list X, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l
______________________________________(1/1)
(forall l1 l2 : list X, x :: l = l1 ++ l2 -> Disjoint l1 l2) ->
NoDup (x :: l)

But that is not at all the goal I would expect! Shouldn't x :: l = l1 ++ l2 be replaced by l = l1 ++ l2?

Here are the propositions I'm working with, in case you'd like to reproduce the problem and see for yourself:

Inductive Disjoint {X : Type}: list X -> list X -> Prop :=
  | disjoint_nil: Disjoint [] []
  | disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2
  | disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2).

Inductive NoDup {X: Type}: list X -> Prop :=
  | nodup_nil: NoDup []
  | nodup_cons: forall hd tl, NoDup tl -> ~(In hd tl) -> NoDup (hd :: tl).

Answer 1

But that is not at all the goal I would expect! Shouldn't x :: l = l1 ++ l2 be replaced by l = l1 ++ l2?

Short answer: It should not!

Induction principle for lists

Let's recall the induction principle for lists:

Check list_ind.
(*
list_ind
  : forall (A : Type) (P : list A -> Prop),
    P [] ->
    (forall (a : A) (l : list A), P l -> P (a :: l)) ->
    forall l : list A, P l
*)

It means that in order to prove that a predicate P holds for all lists (forall l : list A, P l), one needs to prove that

• P holds for the empty list -- P [];
• P holds for all non-empty lists, given that it holds for their tails -- (forall (a : A) (l : list A), P l -> P (a :: l)).

Applying the list induction principle to the goal

Now, we have the following goal:

(forall l1 l2, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.

To see what goals we should get when trying to prove the statement by induction on l, let's mechanically substitute l in the above with [] in one case and h :: tl the other.

[] case:

(forall l1 l2, [] = l1 ++ l2 -> Disjoint l1 l2) -> NoDup [].

h :: tl case:

(forall l1 l2, h :: tl = l1 ++ l2 -> Disjoint l1 l2) -> NoDup (h :: tl).

This is what you've got above (modulo the renaming). For the second case you are also getting the induction hypothesis, which we get from the original statement substituting tl for l:

(forall l1 l2, tl = l1 ++ l2 -> Disjoint l1 l2) -> NoDup tl.

---

Incidentally, the theorem is provable and you might find the following helper lemmas useful:

Lemma disjoint_cons_l {X} (h : X) l1 l2 :
  Disjoint (h :: l1) l2 -> Disjoint l1 l2.
Admitted.

Lemma disjoint_singleton {X} h (l : list X) :
  Disjoint [h] l -> ~ In h l.
Admitted.