coq - 区分策略如何工作？

Question

我对discriminate策略如何在幕后起作用感到很好奇。因此，我做了一些实验。

首先是一个简单的归纳定义:

Inductive AB:=A|B.

然后可以通过 discriminate策略证明一个简单的引理:

Lemma l1: A=B -> False.
intro.
discriminate.
Defined.

让我们看看证明是什么样的:

Print l1.

l1 = 
fun H : A = B =>
(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)
     : A = B -> False

这看起来相当复杂，我不明白这里发生了什么。因此，我试图更明确地证明相同的引理:

Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined.

让我们再次看看Coq对此做了什么:

Print l2.

l2 = 
fun e : A = B =>
match
  e as e0 in (_ = a)
  return
    (match a as x return (A = x -> Type) with
     | A => fun _ : A = A => IDProp
     | B => fun _ : A = B => False
     end e0)
with
| eq_refl => idProp
end
     : A = B -> False

现在我完全感到困惑。这仍然更加复杂。
谁能解释这是怎么回事？

Answer 1

让我们回顾一下l1术语并描述它的每个部分。

l1 : A = B -> False

l1是一个暗示，因此通过Curry-Howard对应关系，它是一个抽象(函数):

fun H : A = B =>

现在，我们需要构造抽象主体，其抽象类型必须为 False。 discriminate策略选择将主体实现为应用程序 f x，其中 f = fun H0 : False => False_ind False H0只是 False归纳原理的包装，这表示如果您有 False的证明，则可以得到您想要的任何命题的证明( False_ind : forall P : Prop, False -> P ):

(fun H0 : False => False_ind False H0)
  (eq_ind A
     (fun e : AB => match e with
                    | A => True
                    | B => False
                    end) I B H)

如果我们执行减少beta的步骤，则将上述内容简化为

False_ind False
          (eq_ind A
             (fun e : AB => match e with
                            | A => True
                            | B => False
                           end) I B H)

False_ind的第一个参数是我们正在构建的术语的类型。如果要证明 A = B -> True，那就应该是 False_ind True (eq_ind A ...)。

顺便说一句，很容易看出我们可以进一步简化我们的 body -为了使 False_ind正常工作，需要提供 False的证明，但这正是我们在这里试图构造的!因此，我们可以完全摆脱 False_ind，得到以下结果:

eq_ind A
  (fun e : AB => match e with
                 | A => True
                 | B => False
                 end) I B H

eq_ind是平等的归纳原则，说平等可以代替平等:

eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
   P x -> forall y : A, x = y -> P y

换句话说，如果有人证明 P x，那么对于等于 y的所有 x， P y成立。

现在，让我们使用 False逐步创建 eq_ind的证明(最后，我们应该获得 eq_ind A (fun e : AB ...)术语)。

当然，我们从 eq_ind开始，然后将其应用于一些 x-为此，我们使用 A。接下来，我们需要谓词 P。写下 P时要记住的重要一件事是，我们必须能够证明 P x。这个目标很容易实现-我们将使用 True命题，它有一个简单的证明。要记住的另一件事是我们要证明的命题( False)-如果输入参数不是 A，我们应该返回它。
通过以上所有条件，谓词几乎可以自己编写:

fun x : AB => match x with
              | A => True
              | B => False
              end

我们有 eq_ind的前两个参数，还需要另外三个参数: x是 A的分支的证明，这是 True的证明，即 I。一些 y，这将使我们得出我们想要得到证明的命题，即 B，以及该答案一开始即 A = B的证明(即 H)的证明。将它们相互堆叠我们得到

eq_ind A
       (fun x : AB => match x with
                  | A => True
                  | B => False
                  end)
       I
       B
       H

而这正是 discriminate给我们的(以某种方式包装)。