coq - COQ 证明助手 - 应用假设

Question

我正在 Coqide 做一个非常简单的证明作业。
我正在尝试将假设H2应用于我的子目标，但由于某种原因它不起作用。我不知道为什么；有人可以解释为什么apply H2.命令不适用。

2 subgoals
A : Type
x : A
l1, l2 : list A
H : Prefix l1 l2
H2 : x :: l2 = (x :: l1) ++ [] -> Prefix (x :: l1) (x :: l2)
______________________________________(1/2)
x :: l2 = (x :: l1) ++ []
______________________________________(2/2)
exists l3 : list A, x :: l2 = (x :: l1) ++ l3

标签： coqcoq-tactic

Answer 1

apply H2没有机会工作，因为它的结论是Prefix (x :: l1) (x :: l2)看起来不像你的目标。的前提H2 是你的目标：x :: l2 = (x :: l1) ++ []然而，这意味着你只有apply H2在你设法首先解决你的目标时才能做到……不是很有用。