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'.

ここからは、常に truef : A -> Bである一意の関数として関数を定義したいと思います。P a (f a)

これどうやってするの？これはできますか？明らかに、私は次のようなものから始めるべきです

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

...しかし、これらの仮説に関して実際に関数をどのように記述すればよいでしょうか?

4

1 に答える 1

3

現在の設定では不可能だと思います。

問題は、定理からbを抽出できることですがexistence、これはにしか存在できませんProp。

だから、私はあなたが移動して中に移動するか、移動してA中に移動する必要があると信じています。BPropexistenceuniquenessSet

これにより、次のいずれかになります。

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 に答える