软件基础第 1 卷：策略：injection_ex3

Question

有人可以解释一下如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)

练习来自 SF 第 1 卷，如标题所示，内容如下：

(** **** Exercise: 3 stars, standard (injection_ex3) *)
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.

现在，我在介绍所有术语后尝试通过injectionon来解决这个问题H0。injection经过重写后H2，我最终得到了以下目标，但我不知道如何前进。

1 subgoal (ID 174)
  
  X : Type
  x, y, z : X
  l, j : list X
  H2 : x = z
  H3 : y :: l = j
  H1 : j = z :: l
  ============================
  z = y

很明显，如果我设法:: l在等式两边都添加，那么我可以用 来完成reflexivity，但是什么策略可以让我:: l在两边都添加呢？

此致

Answer 1

从H3和H1，您应该能够得到一个假设，您可以根据该假设再次使用注入来得出结论。