证明进程在 merge_split 上繁忙

Question

我正在做软件基础练习，并且combine_split在尝试证明辅助引理时遇到了困难。

当在证明过程reflexivity中应用时assert，尽管方程显然(x, y) = (x, y)是正确的，但证明过程只是挂在那里。

这是实现

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y.
  intros l.
  induction l as [| n l' IHl'].
  - simpl. intros l1 l2 H. injection H as H1 H2. rewrite <- H1, <-H2. reflexivity.
  - destruct n as [n1 n2]. simpl. destruct (split l'). 
    intros l1 l2 H. injection H as H1 H2.
    rewrite <- H1, <- H2. simpl. 
    assert ( Hc : combine x y = l'). { apply IHl'. reflexivity.} 
    apply Hc.
Qed.

为什么会发生这种情况？

Answer 1

看起来像 Proof General 中的句子分割中的解析错误。reflexivity.}当您希望将其拆分reflexivity.为 并作为单独的命令时，它似乎会根据突出显示发送到 Coq }。在任何情况下，coqc都不会根据需要对其进行词法分析.}，将其解释为单个（未知）标记。（我实际上很困惑为什么如果它发送给reflexivity.}你却没有得到那个词法错误。）

您可以通过添加空格来解决此问题：reflexivity. }