在coq战术语言中，intro和intros有什么区别

Question

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

intro

和

intros?

Answer 1

如果不提供参数，intro 和 intros 的行为会有所不同

根据reference manual：

如果目标既不是产品，也不是以 let 定义开头，则策略 intro 将应用策略 hnf，直到可以应用策略 intro 或目标不可缩小。

另一方面，intros，作为intro 策略的变体，

重复intro，直到遇到head-constant。它永远不会减少 head-constants 并且永远不会失败。

例子：

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 是多变量，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.

有关介绍模式的一些信息可以在manual 或Software Foundations 书中找到。另请参阅 this example 几个介绍模式的不那么简单的组合。

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