Transitivity of subsequence in COQ

user_16263522 0
Viewed 205

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.
Proof.
intros l1 l2 l3 H H0.
induction H.
  -  apply sseq_e.
  - induction l3. 
  -- inversion H0. 
  -- inversion H0. 
  ---   apply sseq_m.

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.

coq
1 Answers

I have something like subseq l2 x::l3 but then I need to prove subseq l2 l3 which seems like a dead end.

That experience suggests generalizing the induction hypothesis over l3.

(* near the beginning of the proof *)
generalize dependent l3.
induction H.
user_68637490
Related