归纳类型“或”中X的错误消除： [英] Incorrect elimination of X in the inductive type "or":

问题描述

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

I am trying to define a relatively simple function on 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'要么返回 None 或（Some z），其中 z 小于 i 并且我正在尝试在定义中使用它。

I think I understand the reason for this limitation, but I am having difficulty coming up with a workaround. How something like this could be implemented? Basically I have a function f' for which I have a separate proof that values less than 'o' it either returns None or a (Some z) where z is less than i and I am trying to use it in my definition.

推荐答案

有两种方法可以解决此类问题：简便方法和困难方法。

There are two approaches to a problem like this: the easy way and the hard way.

简单方法是考虑您是否在做比复杂的事情你必须。在这种情况下，如果仔细看，您会发现 f'_spec 等效于以下语句，从而避免了 \ / ：

The easy way is to think whether you're doing anything more complicated than you have to. In this case, if you look carefully, you will see that your f'_spec is equivalent to the following statement, which avoids \/:

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.

因此，您可以重新定义 f'_spec VnthIndexedMapped 中的c $ c>并直接使用了证明。

Thus, you could have rephrased the type of f'_spec in VnthIndexedMapped and used the proof directly.

当然，有时无法制作东西更简单。然后，您需要遵循艰苦的方法，并尝试了解Coq的细节，以使其接受您想要的内容。

Of course, sometimes there's no way of making things simpler. Then you need to follow the hard way, and try to understand the nitty-gritty details of Coq to make it accept what you want.

正如Vinz所指出的，您< （通常是例外）不能消除构造某种计算的命题证明。但是，您可以消除一个证明以构造另一个证明，也许该证明可以满足您的需求。例如，您可以这样写：

As Vinz pointed out, you usually (there are exceptions) can't eliminate the proof of proposition to construct something computational. However, you can eliminate a proof to construct another proof, and maybe that proof gives you what need. For instance, you can write this:

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 是等效的，但如果不是，则适用相同的想法，并且您有一些引理，可以让您从一个过渡到另一个。

This definition uses the proof that both formulations of f'_spec are equivalent, but the same idea would apply if they weren't, and you had some lemma allowing you to go from one to the other.

I我个人不太喜欢这种风格，因为它很难使用，并且易于阅读复杂的程序。但是它可以有用途...

I personally don't like this style very much, as it is hard to use and lends itself to programs that are complicated to read. But it can have its uses...

这篇关于归纳类型“或”中X的错误消除：的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！