2

只有在命令成功后，有没有办法在 Ltac 中打印（使用idtac？）一条消息？就像是

first [ a; idtac "a did it!" | b; idtac "b did!" | idtac "nope"; fail ]

这几乎可以工作，除了多个子目标会导致打印多条消息：

Goal True /\ True.
  split; idtac "Split did it!".

仅过滤第一个目标似乎有效......

Goal True /\ True.
  split; [ idtac "Split did it!" | .. ].

...除非它没有：

Goal True /\ True.
  tauto; [ idtac "Tauto did it!" | .. ].

我可能可以将这两种模式合二为一，但我不太热衷于 100% 的点球命中率。这仍然不能解决完全实现目标的策略的情况。

（我最感兴趣的是 8.5 之前的 Coq 的答案，因为在 8.5Info和类似版本中为此提供了很好的设施。即使在 8.5 中，能够仅在某些点打印调试消息也会很有趣）

4

1 回答 1

1

仅idtac在 Coq >= 8.5 中使用作品。

这几乎可以工作，除了多个子目标会导致打印多条消息：

Goal True /\ True.
  split; idtac "Split did it!".

这不是真的; 如果是的话，let n := numgoals in idtac n也会打印多次。这是我看到的输出：

$ ~/.local64/coq/coq-8.5pl3/bin/coqtop
Welcome to Coq 8.5pl3 (November 2016)

Coq < Goal True /\ True.
1 subgoal

  ============================
    True /\ True

Unnamed_thm < split; idtac "Split did it!".
Split did it!
2 subgoals

  ============================
    True

subgoal 2 is:
 True

Unnamed_thm <

在 Coq <= 8.4 中，您不能这样做，因为 Ltac 评估具有不同的模型。相反，如果您愿意稍微复杂化证明术语，并且您可以访问策略序列的开头，则可以这样做：

Ltac duplicate_goal :=
  lazymatch goal with
  | [ |- ?G ] => cut G
  end.

Goal True /\ True.
  duplicate_goal; [ | split ]; [ idtac "Split did it!"; exact (fun x => x) | .. ].

这个想法是，通过复制目标，您可以首先在目标的一个副本中运行您的策略，然后，假设成功，您可以在目标的另一个副本中进行 idtac（无论您是否第一种策略创建多个子目标或解决目标或其他），最后使用恒等函数解决重复目标。

于 2017-07-28T04:45:28.837 回答