我有以下代码。我没有编写完整的代码，但这应该可行。
Definition in_domain {X Y : Set} (f : X -> option Y) x := match (f x) with | Some y => True | None => False end.
Definition injective {X Y : Set} (f : X -> option Y) := forall x y z, f x = Some z -> f y = Some z -> x = y.
Definition surjective {X Y : Set} (f : X -> option Y) := forall y, exists x, f x = Some y.
Definition bijective {X Y : Set} (f : X -> option Y) := injective f /\ surjective f.
Definition compose {X Y Z : Set} (f : X -> option Y) (g : Y -> option Z) (H : forall x, in_domain f x -> in_domain g (f x)) := fun x => match (f x) with | Some y => g y | None => None end.
现在我想写Definition inverse {X Y : Set} (f : X -> option Y) (H : bijective f) : Y -> option X。我不能让该函数g是f x = Some y <-> g y = Some x。
如果可以生成这样的功能，请说明如何做？
您需要公理来执行此操作，因为默认情况下，Coq不允许您从存在证据中提取证人。在这种情况下，您只需要功能可扩展性和唯一选择原则，即选择公理的较弱变体。这是您的问题的简化变体的一种可能性：
Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.
Definition injective {X Y : Set} (f : X -> Y) := forall x y, f x = f y -> x = y.
Definition surjective {X Y : Set} (f : X -> Y) := forall y, exists x, f x = y.
Definition bijective {X Y : Set} (f : X -> Y) := injective f /\ surjective f.
Lemma inverse {X Y : Set} (f : X -> Y) :
bijective f -> {g : Y -> X | (forall x, g (f x) = x) /\
(forall y, f (g y) = y) }.
Proof.
intros [inj sur].
apply constructive_definite_description.
assert (H : forall y, exists! x, f x = y).
{ intros y.
destruct (sur y) as [x xP].
exists x; split; trivial.
intros x' x'P.
now apply inj; rewrite xP, x'P. }
exists (fun y => proj1_sig (constructive_definite_description _ (H y))).
split.
- split.
+ intros x.
destruct (constructive_definite_description _ _).
simpl.
now apply inj.
+ intros y.
now destruct (constructive_definite_description _ _).
- intros g' [H1 H2].
apply functional_extensionality.
intros y.
destruct (constructive_definite_description _ _) as [x e].
simpl.
now rewrite <- e, H1.
Qed.
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句