在coq tactics语言中,intro和intros之间有什么区别

Question

在Coq战术语言中,有什么区别

intro

和

intros？

Answer 1

intro和intros不同的表现,如果没有提供任何参数

根据参考手册:

如果目标既不是产品也不是以定义开始,则策略intro应用策略hnf直到intro可以应用策略或者目标不是可以减少目标.

另一方面,intros作为intro战术的变种,

重复,intro直到它满足头部常数.它永远不会减少头部常数,它永远不会失败.

例:

Goal not False.
  (* does nothing *)
  intros.
  (* unfolds `not`, revealing `False -> False`;
     moves the premise to the context *)      
  intro.
Abort.       

注:这两个intro和intros做同样的事情,如果提供了参数(intro contra/ intros contra).

intros是polyvariadic,intro只能取0或1个参数

Goal True -> True -> True.
  Fail intro t1 t2.
  intros t1 t2.  (* or `intros` if names do not matter *)
Abort.

intro它不支持前奏图案

Goal False -> False.
  Fail intro [].
  intros [].
Qed.

有关介绍模式的一些信息可以在手册或Software Foundations一书中找到.另请参阅这个几个介绍模式的不那么简单组合的例子.

intros不支持after/ before/ at top/ at bottom开关

假设我们有这样的证明状态

H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True /\ True /\ True /\ True -> True

然后例如intro H4 after H3将修改证明状态,如下所示:

H1 : True
H2 : True /\ True
H4 : True /\ True /\ True /\ True 
H3 : True /\ True /\ True
==========
True

并intro H4 after H1会产生

H4 : True /\ True /\ True /\ True 
H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True