1

为了尽可能地隔离这个问题，假设我开始一个 Coq 会话，如下所示。

Parameter A : Type.
Parameter B : Type.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

从这里开始，我想将一个函数定义为始终为真的f : A -> B唯一函数。P a (f a)

我怎样才能做到这一点？我可以这样做吗？显然我应该从类似的东西开始

Definition f : A -> B.
  intro a.
  assert (E := existence a).
  assert (U := uniqueness a).

...但是我如何根据这些假设实际编写函数？

4

1 回答 1

3

我相信在您当前的设置中这是不可能的。

问题是您可以从existence定理中提取 b，但这只能存在于Prop.

所以，我相信你要么必须搬进A去B，Prop要么搬进existence去uniqueness。Set

这将导致以下任一情况：

Parameter A : Prop.
Parameter B : Prop.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

Parameter A : Set.
Parameter B : Set.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, { b : B | P a b }.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

很可能这些都不是您真正想要的。在这种情况下，我需要更多详细信息才能提供帮助。可能是你愿意做一些在直觉主义环境中不可能的事情。

PS：我不是专家。

于 2012-10-22T07:32:18.893 回答