对“护航模式”模式匹配表达式的破坏

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返回x = y的Some证明，而x = y和None则不然。此函数是在eq_bool x y上使用模式匹配来实现的，以测试是否相等，并将车队模式用作在代码中访问对应于匹配分支的相等性的证据的技巧：

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

此时，它认为我必须在eq_bool y y上使用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 (特别是车队模式)，但我有更好的学习经验，使用软件基础书籍(适合初学者)：在我目前的技能水平上，除了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见证中“断开”匹配中的布尔值，这样我们仍然可以正确地键入对eq_dec_correct的调用。最后一个有趣的地方是，我们还必须将eq_dec x x = eq_dec x x转换为eq_dec x x = b，因此我们需要对等式的证明进行抽象。

但正如我前面说过的，你可能想要定义一个更一般的引理。为什么不使用eqtype中已经存在的一些引理？