coq tactics语言中，intro和intros有什么区别

Question

在Coq战术语言中，

有什么区别

intro

和

intros?

Answer 1

如果没有提供参数，

intro 和 intros 的行为会有所不同

根据 reference manual:

If the goal is neither a product nor starting with a let definition, the tactic intro applies the tactic hnf until the tactic intro can be applied or the goal is not head-reducible.

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

repeats intro until it meets the head-constant. It never reduces head-constants and it never fails.

示例：

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 or in the Software Foundations book. See also 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