Proving forall x xs ys, subseq (x :: xs) ys -> subseq xs ys in Coq

Question

I have the following definition

Inductive subseq : list nat -> list nat -> Prop :=
| empty_subseq : subseq [] []
| add_right : forall y xs ys, subseq xs ys -> subseq xs (y :: ys)
| add_both : forall x y xs ys, subseq xs ys -> subseq (x :: xs) (y :: ys).

Using this, I wish to prove the following lemma

Lemma del_l_preserves_subseq : forall x xs ys,
    subseq (x :: xs) ys -> subseq xs ys.
forall (x : nat) (xs ys : list nat),
subseq (x :: xs) ys -> subseq xs ys

So, I tried looking at the proof of subseq (x :: xs) ys by doing destruct H.

Proof.
forall (x : nat) (xs ys : list nat),
subseq (x :: xs) ys -> subseq xs ys
  intros.
x: nat
xs, ys: list nat
H: subseq (x :: xs) ys
subseq xs ys induction H.
x: nat
xs: list nat
subseq xs []
x: nat
xs: list nat
y: nat
xs0, ys: list nat
H: subseq xs0 ys
IHsubseq: subseq xs ys
subseq xs (y :: ys)
x: nat
xs: list nat
x0, y: nat
xs0, ys: list nat
H: subseq xs0 ys
IHsubseq: subseq xs ys
subseq xs (y :: ys)

Why does the first subgoal ask me to prove subseq xs []? Shouldn't the destruct tactic know that the proof cannot be of the form empty_subseq since the type contains x :: xs and not []?

In general how do I prove the lemma that I am trying to prove?

Answer (Li-yao Xia)

Shouldn't the destruct tactic know that the proof cannot be of the form empty_subseq since the type contains x :: xs and not []?

In fact, destruct doesn't know that much. It just replaces x :: xs and xs with [] and [] in the empty_subseq case. In particular, this frequently leads to lost information in the context. Better alternatives:

• Use inversion instead of destruct.

• Use remember to ensure both type indices of subseq are variables before destruct. (remember (x :: xs) as xxs in H.) This more explicit goal management also works well with induction.

Answer (Agnishom Chattopadhyay)

Li-yao's answer was actually useful. This is a proof of the lemma.

Lemma del_l_preserves_subseq : forall x xs ys,
    subseq (x :: xs) ys -> subseq xs ys.
forall (x : nat) (xs ys : list nat),
subseq (x :: xs) ys -> subseq xs ys
Proof.
forall (x : nat) (xs ys : list nat),
subseq (x :: xs) ys -> subseq xs ys
  intros x xs ys.
x: nat
xs, ys: list nat
subseq (x :: xs) ys -> subseq xs ys induction ys as [|y ys'].
x: nat
xs: list nat
subseq (x :: xs) [] -> subseq xs []
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
subseq (x :: xs) (y :: ys') -> subseq xs (y :: ys')
  -
x: nat
xs: list nat
subseq (x :: xs) [] -> subseq xs [] intros.
x: nat
xs: list nat
H: subseq (x :: xs) []
subseq xs [] inversion H.
  (* Inversion will detect that no constructor matches the type of H *)
  -
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
subseq (x :: xs) (y :: ys') -> subseq xs (y :: ys') intros.
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
subseq xs (y :: ys') inversion H.
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
y0: nat
xs0, ys: list nat
H2: subseq (x :: xs) ys'
H1: xs0 = x :: xs
H0: y0 = y
H3: ys = ys'
subseq xs (y :: ys')
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
x0, y0: nat
xs0, ys: list nat
H1: subseq xs ys'
H0: x0 = x
H2: xs0 = xs
H3: y0 = y
H4: ys = ys'
subseq xs (y :: ys')
    (* Inversion will automatically discharge the first case *)
    + (* When [subseq (x :: xs) ys'] holds *)
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
y0: nat
xs0, ys: list nat
H2: subseq (x :: xs) ys'
H1: xs0 = x :: xs
H0: y0 = y
H3: ys = ys'
subseq xs (y :: ys')
      apply IHys' in H2.
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
y0: nat
xs0, ys: list nat
H2: subseq xs ys'
H1: xs0 = x :: xs
H0: y0 = y
H3: ys = ys'
subseq xs (y :: ys') now apply add_right.
    + (* When [subseq xs ys'] holds *)
x: nat
xs: list nat
y: nat
ys': list nat
IHys': subseq (x :: xs) ys' -> subseq xs ys'
H: subseq (x :: xs) (y :: ys')
x0, y0: nat
xs0, ys: list nat
H1: subseq xs ys'
H0: x0 = x
H2: xs0 = xs
H3: y0 = y
H4: ys = ys'
subseq xs (y :: ys')
      now apply add_right.
Qed.