软件基础：应用...与...策略

Question

我正在尝试运行皮尔斯 "Software Foundations" 战术的一些简单示例 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

我该如何解决这个错误？

Answer 1

问题不在于 apply，而是您之前代码中的拼写错误。 trans_eq的定义应该是：

Theorem trans_eq: forall (X:Type) (n m o: X), n = m -> m = o -> n = o.

注意n m o的类型应该是X，而不是Type。

软件基础：应用...与...策略

Software Foundations: apply ... with ... tactic

coq

logical-foundations