6

我很好奇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

现在我完全糊涂了。这还是比较复杂的。谁能解释这里发生了什么？

4

2 回答 2

9

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

l1 : A = B -> False

l1是一个含义，因此通过 Curry-Howard 对应它是一个抽象（函数）：

fun H : A = B =>

现在我们需要构造我们的抽象体，它必须有 type 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 ...)。

顺便说一句，很容易看出我们可以进一步简化我们的主体——因为False_ind它需要提供 的证明False，但这正是我们在这里尝试构建的！因此，我们可以完全摆脱False_ind，得到以下内容：

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

eq_ind是相等的归纳原理，说equals可以代替equals：

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给我们的（模一些包装）。

于 2017-03-23T07:33:25.477 回答
7

另一个答案侧重于判别部分，我将侧重于手动证明。你试过：

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

使用 Coq 时应该注意并且让我经常感到不舒服的是，Coq 接受定义不明确的定义，并在内部将其重写为类型良好的术语。这允许不那么冗长，因为 Coq 自己添加了一些部分。但另一方面，Coq 使用的术语与我们输入的术语不同。

你的证明就是这种情况。自然，模式匹配e应该涉及到构造函数eq_refl，它是该eq类型的单个构造函数。在这里，Coq 检测到不存在相等性并因此了解如何修改您的代码，但您输入的内容不是正确的模式匹配。

有两种成分可以帮助理解这里发生了什么：

  • 的定义eq
  • 完整的模式匹配语法，aswithin和returnterms

首先，我们可以看一下 的定义eq。

Inductive eq {A : Type} (x : A) : A -> Prop :=  eq_refl : x = x.

请注意，此定义与看起来更自然的定义不同（无论如何，更对称）。

Inductive eq {A : Type} : A -> A -> Prop :=  eq_refl : forall (x:A), x = x.

eq用第一个定义而不是第二个定义来定义这一点非常重要。特别是，对于我们的问题，重要的是，inx = y是x一个参数，而y是一个索引。也就是说，x在所有构造函数中是恒定的，而y在每个构造函数中可以不同。您与 type 有相同的区别Vector.t。如果添加元素，向量元素的类型不会改变，这就是它作为参数实现的原因。然而，它的大小是可以改变的，这就是它被实现为索引的原因。

现在，让我们看看扩展的模式匹配语法。我在这里对我所理解的内容做一个非常简短的解释。不要犹豫，查看参考手册以获取更安全的信息。该return子句可以帮助指定每个分支都不同的返回类型。该子句可以使用模式匹配的asandin子句中定义的变量，它分别绑定匹配的术语和类型索引。该return子句将在每个分支的上下文中进行解释，替换as并in使用该上下文的变量，逐个对分支进行类型检查，并用于match从外部角度键入。

这是一个带有as子句的人为示例：

Definition test n :=
  match n as n0 return (match n0 with | 0 => nat | S _ => bool end) with
  | 0 => 17
  | _ => true
  end.

根据 的值n，我们不会返回相同的类型。的类型test是forall n : nat, match n with | 0 => nat | S _ => bool end。但是当 Coq 可以决定我们在哪种情况下匹配时，它可以简化类型。例如：

Definition test2 n : bool := test (S n).

在这里，Coq 知道，无论是什么n，S n给定的test结果都是 type bool。

对于相等，我们可以做类似的事情，这次使用in从句。

Definition test3 (e:A=B) : False :=
  match e in (_ = c) return (match c with | B => False | _ => True end) with
  | eq_refl => I
  end.

这里发生了什么 ？本质上，Coq 分别对 the 的分支match和match自身的分支进行类型检查。在唯一的分支eq_refl中，c等于A（因为它的定义eq_refl实例化了与参数相同的值的索引），因此我们声称我们返回了一些类型的值True，这里I。但是从外部的角度来看，c等于B（因为e是 type A=B），这一次return子句声称match返回了一些 type 的值False。我们在这里使用 Coq 的功能来简化我们刚刚看到的类型中的模式匹配test2。请注意，我们True在其他情况下使用了B，但我们并不True特别需要。我们只需要一些有人居住的类型，这样我们就可以在eq_refl分支中返回一些东西。

回到 Coq 产生的奇怪术语，Coq 使用的方法做了类似的事情，但在这个例子中，肯定更复杂。特别是，当 CoqIDProp需要idProp无用的类型和术语时，它经常使用类型。它们对应于True并I在上面使用。

最后，我给出了关于 coq-club 的讨论链接，它确实帮助我理解了如何在 Coq 中键入扩展模式匹配。

于 2017-03-23T13:39:40.443 回答