coq - 在coq战术语言中，介绍和介绍有什么区别

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 中找到。或在 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