问关于介绍[=]和介绍[= <- H]的问题

EN

有关这方面的文档是here。我将添加一点解释说明。

intro模式的第一个历史用途是动态分解打包在归纳对象中的数据。这是第一个简单的示例(使用coq 8.13.2测试)。

Lemma forall A B, A /\ B -> B /\ A.
Proof.

如果你运行intros A B H策略，那么假设H将是A /\ B的证明。从道德上讲，这包含了A持有的知识，但它不能这样使用，因为它是一个更强有力的事实的证明。通常情况下，用户希望直接分解此假设，这通常是通过键入destruct H as [Ha Hb]来完成的。但是如果你马上就知道你不会保持假设H，为什么不找一个更短的表达式呢？这就是intro模式的用途。

因此，您可以键入以下命令并获得结果目标：

Intros A B [Ha Hb].
(* resulting goal
  A, B : Prop
  Ha : A
  Hb : B
  ============================
  B /\ A
*)
Abort.

我不会完成这个证明的。但是您已经了解了intro模式的用途:当归纳类型(如这里的合取)将多个信息打包在一起时，动态地分解信息。

现在，相等信息也可以将几条信息打包在一起。现在假设我们正在处理自然数的列表，并且我们有以下等式。

Require Import List.

Lemma intro_pattern_example2 n m p q l1 l2 :
  (n :: S m :: l1) = (p :: S q :: l2) -> q :: p :: l2 = m :: n :: l1.

含义左侧的相等是两个列表之间的相等，但它实际上打包了几个更基本的信息：n = p、m = q和l1 = l2。如果您只输入intros H，您将获得两个长度为3的列表之间的相等，但是如果您输入intros [=]，您将要求证明系统探索每个相等成员的结构，并检查构造函数何时出现，以便可以将较小的信息放在单独的假设中，而不是放在较大的假设中。这是使用injection策略的速记。下面是一个示例。

intros [= Hn Hm Hl1].

(*resulting goal:
  n, m, p, q : nat
  l1, l2 : list nat
  Hn : n = p
  Hm : m = q
  Hl1 : l1 = l2
  ============================
  q :: p :: l2 = m :: n :: l1
*)

所以你看，这个介绍模式解开了原本会被困在更复杂的假设中的信息。

现在，当一个假设是一个相等时，您可能想要立即执行另一个操作。你可能想用它来重写。在intro模式中，这是通过用箭头替换您将为该相等指定的名称来完成的。让我们在前一个目标上测试一下。

Undo.
intros [= -> -> ->].
(* resulting goal
  p, q : nat
  l2 : list nat
  ============================
  q :: p :: l2 = q :: p :: l2
*)

现在，这个目标可以通过reflexivity、trivial或auto快速解决。请注意，假设是用来重写的，但它们没有保存在目标上下文中，因此必须谨慎使用直接从intro模式重写的可能性，因为您实际上丢失了一些信息。

当两个成员都是数据类型构造函数时，[= ] intro模式尤其适用于等式。它利用了这些构造函数的自然内射性。数据类型构造函数还考虑了另一个属性。事实是，具有不同头构造函数的两个数据片段永远不会相等。在Coq中，discriminate策略利用了这一点。[=]简介模式是injection和discriminate策略的简写。