Transitivity of subsequence in Coq

Link:: https://stackoverflow.com/q/69797654

Display all goals and responses

Question

I have been working my way through logical foundations and have gotten very stuck on the transitivity of subsequences exercise.

Exercise: 2 stars, advanced (subsequence)

A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,

(Optional, harder) Prove subseq_trans that subsequence is transitive -- that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!

Inductive subseq : list nat -> list nat -> Prop :=
| sseq_e (l2 : list nat) : subseq [] l2
| sseq_m (l1 l2 : list nat) (n : nat) (H: subseq l1 l2) : subseq (n::l1) (n::l2)
| sseq_nm (l1 l2 : list nat) (n : nat) (H: subseq l1 l2) : subseq l1 (n::l2).

Theorem subseq_trans : forall l1 l2 l3 : list nat,
    subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.forall l1 l2 l3 : list nat,
subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3
Proof.forall l1 l2 l3 : list nat,
subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3
  intros l1 l2 l3 H H0.l1, l2, l3: list nat
H: subseq l1 l2
H0: subseq l2 l3
subseq l1 l3 induction H.l3, l2: list nat
H0: subseq l2 l3
subseq [] l3
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) l3
IHsubseq: subseq l2 l3 -> subseq l1 l3
subseq (n :: l1) l3
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) l3
IHsubseq: subseq l2 l3 -> subseq l1 l3
subseq l1 l3
  -l3, l2: list nat
H0: subseq l2 l3
subseq [] l3 apply sseq_e.
  -l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) l3
IHsubseq: subseq l2 l3 -> subseq l1 l3
subseq (n :: l1) l3 induction l3.l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) []
IHsubseq: subseq l2 [] -> subseq l1 []
subseq (n :: l1) []
a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
subseq (n :: l1) (a :: l3)
    +l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) []
IHsubseq: subseq l2 [] -> subseq l1 []
subseq (n :: l1) [] inversion H0.
    +a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
subseq (n :: l1) (a :: l3) inversion H0.a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq (a :: l1) (a :: l3)
a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq (n :: l1) (a :: l3)
      *a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq (a :: l1) (a :: l3) apply sseq_m.a: nat
l3, l1, l2: list nat
n: nat
H: subseq l1 l2
H0: subseq (n :: l2) (a :: l3)
IHsubseq: subseq l2 (a :: l3) -> subseq l1 (a :: l3)
IHl3: subseq (n :: l2) l3 ->
(subseq l2 l3 -> subseq l1 l3) ->
subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq l1 l3

I am having trouble getting the right induction hypothesis after having tried a couple of different approaches. I have tried a number of approaches and end up with a situation where, in my assumptions, I have something like subseq l2 (x::l3) but then I need to prove subseq l2 l3 which seems like a dead end. Any pointers in the right direction would be much appreciated.

Answer

That experience suggests generalizing the induction hypothesis over l3.

Theorem subseq_trans : forall l1 l2 l3 : list nat,
    subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.forall l1 l2 l3 : list nat,
subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3
Proof.forall l1 l2 l3 : list nat,
subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3
  intros l1 l2 l3 H.l1, l2, l3: list nat
H: subseq l1 l2
subseq l2 l3 -> subseq l1 l3 generalize dependent l3.l1, l2: list nat
H: subseq l1 l2
forall l3 : list nat, subseq l2 l3 -> subseq l1 l3 induction H; intros l3 H0.l2, l3: list nat
H0: subseq l2 l3
subseq [] l3
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
l3: list nat
H0: subseq (n :: l2) l3
subseq (n :: l1) l3
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
l3: list nat
H0: subseq (n :: l2) l3
subseq l1 l3
  -l2, l3: list nat
H0: subseq l2 l3
subseq [] l3 apply sseq_e.
  -l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
l3: list nat
H0: subseq (n :: l2) l3
subseq (n :: l1) l3 induction l3.l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
H0: subseq (n :: l2) []
subseq (n :: l1) []
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
subseq (n :: l1) (a :: l3)
    +l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
H0: subseq (n :: l2) []
subseq (n :: l1) [] inversion H0.
    +l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
subseq (n :: l1) (a :: l3) inversion H0.l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq (a :: l1) (a :: l3)
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq (n :: l1) (a :: l3)
      *l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq (a :: l1) (a :: l3) specialize (IHsubseq l3 H2).l1, l2: list nat
n: nat
H: subseq l1 l2
l3: list nat
IHsubseq: subseq l1 l3
a: nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq (a :: l1) (a :: l3) apply (sseq_m l1 l3 a IHsubseq).
      *l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq (n :: l1) (a :: l3) specialize (IHl3 H3).l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l1) l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq (n :: l1) (a :: l3) apply (sseq_nm (n :: l1) l3 a IHl3).
  -l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
l3: list nat
H0: subseq (n :: l2) l3
subseq l1 l3 induction l3.l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
H0: subseq (n :: l2) []
subseq l1 []
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
subseq l1 (a :: l3)
    +l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
H0: subseq (n :: l2) []
subseq l1 [] inversion H0.
    +l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
subseq l1 (a :: l3) inversion H0.l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq l1 (a :: l3)
l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq l1 (a :: l3)
      *l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq l1 (a :: l3) specialize (IHsubseq l3 H2).l1, l2: list nat
n: nat
H: subseq l1 l2
l3: list nat
IHsubseq: subseq l1 l3
a: nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
l0, l4: list nat
n0: nat
H2: subseq l2 l3
H1: n0 = n
H3: l0 = l2
H4: n = a
H5: l4 = l3
subseq l1 (a :: l3) apply (sseq_nm l1 l3 a IHsubseq).
      *l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq (n :: l2) l3 -> subseq l1 l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq l1 (a :: l3) specialize (IHl3 H3).l1, l2: list nat
n: nat
H: subseq l1 l2
IHsubseq: forall l3 : list nat,
subseq l2 l3 -> subseq l1 l3
a: nat
l3: list nat
H0: subseq (n :: l2) (a :: l3)
IHl3: subseq l1 l3
l0, l4: list nat
n0: nat
H3: subseq (n :: l2) l3
H2: l0 = n :: l2
H1: n0 = a
H4: l4 = l3
subseq l1 (a :: l3) apply (sseq_nm l1 l3 a IHl3).
Qed.