归纳式"or"中X的错误消去:
Incorrect elimination of X in the inductive type "or":
我正在尝试在 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
,我正在尝试在我的定义中使用它。
问题是您想通过检查 f'_spec
的内容来构建术语。这个析取存在于Prop
,所以它只能构建其他Prop
。您想要构建更多 Type
中的内容。因此,您需要一个至少存在于 Set
中(更普遍地存在于 Type
中)的析取版本。我建议您将 Foo \/ Bar
语句替换为 sumbool
的用法,它使用符号 {Foo}+{Bar}
.
有两种解决此类问题的方法:简单方法和困难方法。
简单的方法是想想您是否正在做比您必须做的事情更复杂的事情。在这种情况下,如果你仔细看,你会发现你的 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
的两个公式是等价的证明,但如果它们不是等价的,同样的想法也适用,并且你有一些引理允许你从一个到另一个。
我个人不是很喜欢这种风格,因为它很难用,而且适合阅读复杂的程序。但它可以有它的用途...
我正在尝试在 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
,我正在尝试在我的定义中使用它。
问题是您想通过检查 f'_spec
的内容来构建术语。这个析取存在于Prop
,所以它只能构建其他Prop
。您想要构建更多 Type
中的内容。因此,您需要一个至少存在于 Set
中(更普遍地存在于 Type
中)的析取版本。我建议您将 Foo \/ Bar
语句替换为 sumbool
的用法,它使用符号 {Foo}+{Bar}
.
有两种解决此类问题的方法:简单方法和困难方法。
简单的方法是想想您是否正在做比您必须做的事情更复杂的事情。在这种情况下,如果你仔细看,你会发现你的 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
的两个公式是等价的证明,但如果它们不是等价的,同样的想法也适用,并且你有一些引理允许你从一个到另一个。
我个人不是很喜欢这种风格,因为它很难用,而且适合阅读复杂的程序。但它可以有它的用途...