COQ 证明助手 - 应用假设
COQ Proof Assistant - Apply the hyppothesis
我正在 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
apply H2 没有机会工作，因为它的结论是 Prefix (x :: l1) (x :: l2) 这看起来不像你的目标。
H2 的前提是 你的目标： x :: l2 = (x :: l1) ++ [] 但是，这意味着你只能 apply H2 如果你设法解决你的问题目标第一……不是很有用。
我正在 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
apply H2 没有机会工作，因为它的结论是 Prefix (x :: l1) (x :: l2) 这看起来不像你的目标。
H2 的前提是 你的目标： x :: l2 = (x :: l1) ++ [] 但是，这意味着你只能 apply H2 如果你设法解决你的问题目标第一……不是很有用。