coq - COQ中子序列的传递性

Question

我一直在努力打通逻辑基础，并且非常坚持子序列练习的传递性。

(** **** 练习：2 星，高级（子序列）

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. 

在尝试了几种不同的方法后，我无法获得正确的归纳假设。我尝试了多种方法，最终遇到这样一种情况，在我的假设中，我有类似 subseq l2 x::l3 的东西，但是我需要证明 subseq l2 l3 这似乎是一个死胡同。任何指向正确方向的指针都将不胜感激。

标签： coq

Answer 1

我有类似 subseq l2 x::l3 的东西，但是我需要证明 subseq l2 l3 这似乎是一个死胡同。

该经验建议将归纳假设推广到l3.

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