1

我被困在一个关于归纳谓词的简单证明上。我必须证明自然 0 不是正数，其中自然是位列表，而 0 是任何只有位为 0 的列表。

H1: pos Empt
____________ (1/1)
Nat

Certified Programming with Dependents Types这一章似乎建议我使用inversion，但我收到一条错误消息。

Require Import Coq.Program.Program.

Inductive Bit: Type :=
  | Zer: Bit
  | One: Bit.

Inductive List (type1: Type): Type :=
  | Empt: List type1
  | Fill: type1 -> List type1 -> List type1.

Implicit Arguments Empt [[type1]].

Implicit Arguments Fill [[type1]].

Definition Nat: Type := List Bit.

Inductive pos: Nat -> Prop :=
  | pos_1: forall nat1: Nat, pos (Fill One nat1)
  | pos_2: forall nat1: Nat, pos nat1 -> forall bit1: Bit, pos (Fill bit1 nat1).

Program Fixpoint pred (nat1: Nat) (H1: pos nat1): Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat2 => Fill One (pred nat2 H1)
  | Fill One nat2 => Fill Zer nat2
  end.

Next Obligation.
inversion H1.
4

1 回答 1

1

你Theorem T1的不等同于Obligation. 在后者中，您应该构建一个 的元素Nat，它本身就是 a Type（顺便说一句，您为什么不在这里使用Set？您似乎没有在此开发中操纵高阶类型）。

正如错误消息所说，您不能inversion对 for that 的元素执行案例分析（基于此）Prop（具体参见Coq 手册的第 4.5.4 节）。但是，在这种情况下，您对构建一个实际的 不感兴趣Nat，您只是想证明这种情况是不可能的。为此，您可以apply False_rect（或者False_rec如果您选择使用Set而不是Type），这将让您证明False. False作为一个Prop，你就可以使用inversion H1.

请注意，您的定义的第二个分支存在问题pred：您不能使用(pred nat2 H1)，因为H1不是pos nat2. 最简单的方法可能也是在这里留下一个洞：(pred nat2 _)，这可以用 an 轻松解决inversion（这一次，你必须建立一个类型的术语pos nat2，即存在于 中的东西Prop）。

于 2012-11-27T15:13:33.563 回答