仅在战术成功时才打印消息

Question

只有在命令成功后，才有方法在Ltac中打印（使用？）消息？喜欢的东西

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.5 Info等为此提供了很好的设备，即使在8.5中，只能在某些点打印调试消息也会很有趣）

Answer 1

只使用在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 < 

---

在勒柯克< = 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) | .. ]. 

的想法是，通过复制目标，可以首先在目标副本中运行你的策略，然后，假设成功，你可以在目标的另一个副本（作为单一目标存在，无论你的第一个策略是否创建了多个子目标或解决目标或任何其他目标） ，最后用身份函数解决重复的目标。