0

假设我在 Coq 中有以下定义：

Inductive Compare := Lt | Eq | Gt.

Fixpoint compare (x y : nat) : Compare :=
  match x, y with
  | 0, 0   => Eq
  | 0, S _ => Lt
  | S _, 0 => Gt
  | S x', S y' => compare x' y'
  end.

现在考虑这个引理：

Lemma foo : forall (x: nat),
    (forall z, match compare x z with
               | Lt => False
               | Eq => False
               | Gt => False
               end) -> nat -> False.
Proof.
  intros x H y.

此时证明状态如下所示：

   x : nat
   H : forall z : nat,
       match compare x z with
       | Lt => False
       | Eq => False
       | Gt => False
       end
   y : nat
   ============================
   False

我想写 Ltacmatch goal来检测：

a）有一个假设x : nat被用作compare量化假设内部某处的论据H

b) 还有一些其他类型的假设nat——即y——可以用来专门化量化假设。

c）一旦我们有这两件事H专门y

我试着这样做：

 match goal with
 | [ X : nat, Y : nat
   , H : forall (z : nat), context [ compare X z ] |- _ ] => specialize (H Y)
 end.

但是这段代码至少有两点有问题：

  1. context在 a 下使用似乎forall是不允许的。

  2. 我想不出一个正确的方法来X作为参数传递给compare 它，因为它被认为是作为假设存在的东西。这样做是这样的：

4

2 回答 2

2

这并不完全符合您的要求，但它有点接近：

match goal with
| [ X : nat, Y : nat, H : context[compare ?a _] |- _ ] =>
  match type of H with
  | forall (z: nat), _ =>
    match a with
    | X => specialize (H Y)
    end
  end
end.

但是，这不会检查第二个参数是否与 .绑定的compare相匹配。zforall

于 2017-07-29T16:54:31.887 回答
2

如果要检查X量化假设中出现的情况H，只需在用任何不包含 的值实例化后检查它是否出现在 H 中X。例如，您可以H通过Y简单地将应用程序H作为函数编写到Y. 这是我的建议：

match goal with | X : nat, H : _, Y : nat |- _ =>
  match type of (H Y) with | context[X] => specialize (H Y) end
end.

这个 Ltac 文本确实检查了 H 是一个函数。如果您想更精确并声明它H确实应该是一个通用量化（或产品类型），那么您可以检查该类型是否(H Y)也包含Y，如下面的片段所示：

match goal with | X : nat, H : _, Y : nat |- _ =>
  match type of (H Y) with | context[X] => 
    match type of (H Y) with | context [Y] => specialize (H Y) end
  end
end.
于 2017-07-31T14:33:26.317 回答