【发布时间】：2016-01-21 05:17:48
【问题描述】：
我尝试在 Pierce 的“软件基础”中的 apply ... with ... 策略上运行一些简单的示例。
看来书中的例子对我不起作用：
Theorem trans_eq: forall (X: Type) (n m o: Type),
n = m -> m = o -> n = o.
Proof.
intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2. reflexivity.
Qed.
Example trans_eq_example' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* If we simply tell Coq apply trans_eq at this point,
it can tell (by matching the goal against the
conclusion of the lemma) that it should instantiate X
with [nat], n with [a,b], and o with [e,f].
However, the matching process doesn't determine an
instantiation for m: we have to supply one explicitly
by adding with (m:=[c,d]) to the invocation of
apply. *)
apply trans_eq with (m:=[c;d]). apply eq1. apply eq2. Qed.
trans_eq_example' 失败并出现错误：
trans_eq_example' < apply trans_eq with (m:=[c;d]).
Toplevel input, characters 6-30:
> apply trans_eq with (m:=[c;d]).
> ^^^^^^^^^^^^^^^^^^^^^^^^
Error: Impossible to unify "?1707 = ?1709" with "[a; b] = [e; f]".
关于 Coq 版本的更多信息：
coqtop -v
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 23:12:44 with OCaml 4.01.0
我该如何解决这个错误？
【问题讨论】：
-
由于我手头没有软件基金会的源代码，你能给我们
[a;b]代表什么的符号吗？是列表吗？ -
这个错误似乎很微不足道。在
trans_eq、n、m和o中必须是X类型，而不是Type类型。请注意，目前X未在您的定理中使用。 -
该死的@eponier，你比我早 1 分钟 :) 你应该在答案部分发布答案。
-
@Vinz 我犹豫了，因为这是一个特例。当我有更多有趣的事情要写时，我会发布答案。我不确定这是否是一个足够笼统的问题，可以保留在 SO 上。至少，我建议更改标题以反映实际问题。
-
我同意，标题应该更正。