coq - 证明过程忙于 combine_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. }