0

使用 Coq 8.4pl3，我在使用eqn:归纳时遇到错误：参考手册中归纳下未列出的变体。

(* Export below requires Software Foundations 4.0. *)
Require Export Logic.

Inductive disjoint (X : Type) (l1 l2 : list X) : Prop :=
  | nil1 : l1 = [] -> disjoint X l1 l2
  | nil2 : l2 = [] -> disjoint X l1 l2
  | bothCons : forall x:X, 
                 In x l1 -> 
                   not (In x l2) -> 
                     disjoint X l1 l2.

Fixpoint head (X : Type) (l : list X) : option X :=
  match l with
  | [] => None
  | h :: t => Some h
  end.

Fixpoint tail (X : Type) (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => t
  end.

Inductive NoDup (X : Type) (l : list X) : Prop :=
  | ndNil : l = [] -> NoDup X l
  | ndSingle : forall x:X, l = [x] -> NoDup X l
  | ndCons : forall x:X, head X l = Some x ->
               not (In x (tail X l)) /\ NoDup X (tail X l) -> 
                 NoDup X l.

Theorem disjoint__app_NoDup : 
      forall (X : Type) (l1 l2 : list X),
        disjoint X l1 l2 /\ NoDup X l1 /\ NoDup X l2 ->
          NoDup X (l1 ++ l2).
Proof.
      intros. induction H eqn:caseEqn.

如果我只用简单的“归纳 H”代替最后一步，我不会收到任何错误，但是使用上面的 eqn: 参数，我会收到错误：

错误：a 用于结论。

（以前在定理语句中缺少一个条件，并且相同的错误列出了标识符d。）

参考手册将“在结论中使用”列为使用assert的错误。从某种意义上说，在幕后，eqn:可能正在生成断言，但我在上下文中没有可见的标识符a，而且我看不到 Coq 试图自动使用它做什么。

尝试将证明的开头替换为

  intros. remember H. induction H.

现在进行归纳的尝试给出了与以前相同的错误，只是使用H而不是a。（当定理缺少附加条件时，Coq 还明确地在上下文中添加了一个d，与假设H相同。）

我怎样才能在这里前进？我试图避免从上下文中丢失信息。

4

1 回答 1

0

这是一个小错误；我已经举报了。但是，您在这里尝试做的事情并不是特别明智。请注意，您正在调用induction合取 ( /\)，并要求 Coq 给您留下一个等式，该等式表明原始假设等于两个生成的证明的合取。这里有两个问题：

  1. 您的假设不会在任何地方以依赖的方式使用，因此您无需记住它。
  2. 你的假设不是递归的，所以你也可以做destruct H而不是induction H。

至于错误消息，如果您注意到替换/\为*使induction H eqn:caseEqn通过，并将您的假设分成名为aand的两部分，它会变得更加清楚b。induction H eqn:...实际问题是，当H' 的类型为 a时，由 构造的证明项是错误类型的Prop，因为您无法消除Props 来获取信息。我怀疑代码只是试图a对它以特定方式创建的 做某事，并假设任何未能做到这一点的原因一定是因为a在结论中使用了，而不是因为它创建的证明项格式不正确.

于 2018-02-28T06:34:52.927 回答