coq - 使用 'convoy pattern' 对模式匹配表达式使用 destruct

Question

出于这个问题的目的，假设我有:

Parameter eq_bool : forall (A:Type), A -> A -> bool.

Arguments eq_bool {A} _ _.

Axiom eq_bool_correct : forall (A:Type) (x y:A),
    eq_bool x y = true -> x = y.

Axiom eq_bool_correct' : forall (A:Type) (x y:A),
     x = y -> eq_bool x y = true.

我有一个函数，它给出了两个值 x y:A返回 Some x = y的证明每当 x = y和 None除此以外。这个函数是通过 eq_bool x y 上的模式匹配来实现的。测试相等性，并使用 convoy 模式作为一种技巧，在您的代码中访问与匹配分支对应的相等性证明:

Definition test (A:Type) (x y:A) : option (x = y) :=
    match eq_bool x y as b return eq_bool x y = b -> option (x = y) with
    | true  => fun p => Some (eq_bool_correct A x y p)
    | false => fun _ => None
    end (eq_refl (eq_bool x y)).

我现在试图证明一个关于这个函数的简单结果:

Theorem basic: forall (A:Type) (x y:A),
    x = y -> test A x y <> None.
Proof.
    intros A x y H. rewrite H. unfold test.

A : Type
x, y : A
H : x = y
============================
(if eq_bool y y as b return (eq_bool y y = b -> option (y = y))
 then fun p : eq_bool y y = true => Some (eq_bool_correct A y y p)
 else fun _ : eq_bool y y = false => None) eq_refl <> None

这时候感觉不得不用 destruct在 eq_bool y y (可能保持方程):

destruct (eq_bool y y).

Error: Abstracting over the term "b" leads to a term
fun b0 : bool =>
(if b0 as b1 return (b0 = b1 -> option (y = y))
 then fun p : b0 = true => Some (eq_bool_correct A y y p)
 else fun _ : b0 = false => None) eq_refl <> None
which is ill-typed.
Reason is: Illegal application: 
The term "eq_bool_correct" of type
 "forall (A : Type) (x y : A), eq_bool x y = true -> x = y"
cannot be applied to the terms
 "A" : "Type"
 "y" : "A"
 "y" : "A"
 "p" : "b0 = true"
The 4th term has type "b0 = true" which should be coercible to
 "eq_bool y y = true".

我知道我必须阅读 CPDT(尤其是在 convoy 模式上)，但我对 Software Foundation 的书(适合初学者)有更好的学习经验:以我目前的技能水平，除了 destruct 我什么都想不起来了并希望有人可以提出一种方法来完成这个证明。

Answer 1

这是粗心的抽象使术语类型错误的典型情况。一般来说，你想使用稍微不同的原则来避免这些问题，匹配于 sumbool或 reflect可能会为您提供更好的结果。

在这种特殊情况下，为了让事情顺利通过，您首先需要对目标进行一些概括(因此它不依赖于 eq_refl ，这是匹配时的问题，因为它的类型规则太严格了)然后选择适当的子项。我使用 ssreflect 模式语言，因为它更方便:

(* Do From Coq Require Import ssreflect. *)
Theorem basic (A : Type) (x y : A) (p : x = y) : test x y <> None.
Proof.
rewrite p /test; move: eq_refl; case: {2 3}(eq_dec y y) => //.
by rewrite eq_dec_correct'.
Qed.

事实上，我们需要选择匹配 eq_dec 的匹配项。在比赛中和等式证明的右侧。您可以逐步执行上述证明，或者您可以将上述证明视为构建和证明更一般的引理:

Theorem basic0 (A : Type) (x : A) b (p : eq_dec x x = b) :
  match b as b1 return eq_dec x x = b1 -> option (x = x) with
  | true  => fun p => Some (eq_dec_correct p)
  | false => fun _ => None
  end p <> None.
Proof. by case: b p; rewrite ?eq_dec_correct'. Qed.

Theorem basic1 (A : Type) (x y : A) (p : x = y) : test x y <> None.
Proof. by rewrite p; apply: basic0. Qed.

请注意，在这里，通过仔细选择我们的参数，我们如何避免使用模式选择来执行技巧。关键步骤是从 eq_dec 中“取消链接”匹配中的 bool 值。 “convoy”参数中出现了witness，所以我们仍然可以正确地输入对 eq_dec_correct 的调用。 .最后一个有趣的地方是我们还必须转 eq_dec x x = eq_dec x x进入 eq_dec x x = b ，因此我们需要对等式证明进行抽象。

但正如我之前所说，您可能想要定义一个更一般的引理。 [为什么不使用 eqtype 中已经存在的一些引理?]