归纳式"or"中X的错误消去：

Question

我正在尝试在 Coq 上定义一个相对简单的函数：

    (* Preliminaries *)
    Require Import Vector.
    Definition Vnth {A:Type} {n} (v : Vector.t A n) : forall i, i < n -> A. admit. Defined.

    (* Problematic definition below *)
    Definition VnthIndexMapped {A:Type}
    {i o:nat}
    (x: Vector.t (option A) i)
    (f': nat -> option nat)
    (f'_spec:  forall x, x<o ->
                    (forall z,(((f' x) = Some z) -> z < i)) \/
                                   (f' x = None))
    (n:nat) (np: n<o)
    : option A
    :=
      match (f' n) as fn, (f'_spec n np) return f' n = fn -> option A with        
      | None, _ => fun _ => None
      | Some z, or_introl zc1  => fun p => Vnth x z (zc1 z p)
      | Some z, or_intror _  => fun _ => None (*  impossible case *)
      end.

并出现以下错误：

Error:
Incorrect elimination of "f'_spec n np" in the inductive type "or":
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

我想我理解此限制的原因，但我很难想出解决方法。如何实施这样的事情？基本上我有一个函数 f' ，我有一个单独的证明值小于 'o' 它要么是 returns None 要么是 (Some z) where z 小于 i，我正在尝试在我的定义中使用它。

Answer 1

问题是您想通过检查 f'_spec 的内容来构建术语。这个析取存在于Prop，所以它只能构建其他Prop。您想要构建更多 Type 中的内容。因此，您需要一个至少存在于 Set 中（更普遍地存在于 Type 中）的析取版本。我建议您将 Foo \/ Bar 语句替换为 sumbool 的用法，它使用符号 {Foo}+{Bar}.

Answer 2

有两种解决此类问题的方法：简单方法和困难方法。

简单的方法是想想您是否正在做比您必须做的事情更复杂的事情。在这种情况下，如果你仔细看，你会发现你的 f'_spec 相当于下面的语句，它避免了 \/:

Lemma f'_spec_equiv i o (f': nat -> option nat) :
   (forall x, x<o ->
                               (forall z,(((f' x) = Some z) -> z < i)) \/
                               (f' x = None))
    <-> (forall x, x<o -> forall z,(((f' x) = Some z) -> z < i)).
Proof.
  split.
  - intros f'_spec x Hx z Hf.
    destruct (f'_spec _ Hx); eauto; congruence.
  - intros f'_spec x Hx.
    left. eauto.
Qed.

因此，您可以在 VnthIndexedMapped 中重新表述 f'_spec 的类型并直接使用证明。

当然，有时没有办法让事情变得更简单。那么你就需要循循善诱，努力去理解 Coq 的细节，让它接受你想要的东西。

正如 Vinz 指出的那样，您通常（也有例外）不能消除命题证明来构造计算性的东西。但是，您可以消除一个证明来构造 另一个证明 ，也许那个证明可以满足您的需要。例如，您可以这样写：

Definition VnthIndexMapped {A:Type}
           {i o:nat}
           (x: Vector.t (option A) i)
           (f': nat -> option nat)
           (f'_spec:  forall x, x<o ->
                                (forall z,(((f' x) = Some z) -> z < i)) \/
                                (f' x = None))
           (n:nat) (np: n<o)
: option A
  :=
    match (f' n) as fn return f' n = fn -> option A with
      | None => fun _ => None
      | Some z => fun p =>
                    let p' := proj1 (f'_spec_equiv i o f') f'_spec n np z p in
                    Vnth x z p'
    end eq_refl.

这个定义使用 f'_spec 的两个公式是等价的证明，但如果它们不是等价的，同样的想法也适用，并且你有一些引理允许你从一个到另一个。

我个人不是很喜欢这种风格，因为它很难用，而且适合阅读复杂的程序。但它可以有它的用途...

归纳式"or"中X的错误消去：

Incorrect elimination of X in the inductive type "or":

coq