Coqに暗黙的に関数を組み込むには？

Question

私はすべてのグループに逆関数があることを証明しようとしています。

次のように私はグループを定義しています

Record Group:Type := { 
G:Set; 
mult:G->G->G; 
e:G; 
assoc:forall x y z:G, mult x (mult y z)=mult (mult x y) z; 
neut:forall x:G, mult e x=x /\ mult x e=x; 
inverse:forall x:G,exists y:G, mult x y = e 
}. 

私がしたい主な理由は、私はそれだけでinverse:forall x:G, {y: mult x y = e}.、あるいはinverse:G->G. is_inverse:forall x:G, mult x (inverse x)=e.によって逆公理を置き換えるために優れていることを承知していますが、私は私の定義を好みます教室で与えられたものと同一であることを意味する。

だから私は選択公理のに適したバージョンが含まれている：

Axiom indefinite_description : forall (A : Type) (P: A->Prop), ex P -> sig P. 
Axiom functional_choice : forall A B (R:A->B->Prop), (forall x, exists y, R x y) -> (exists f, forall x, R x (f x)). 

今、私は自分の主張を証明することができます。

Lemma inv_func_exists(H:Group):exists inv_func:G H->G H, (forall x:G H, mult H x (inv_func(x))=e H). 
generalize (inverse H). 
apply functional_choice. 
Qed. 

今、私は存在を証明していることを、私はしたいと思います実際の関数を定義する。ここで私は物事が乱雑になり始めると感じます。次の定義は、実際の関数を作成しますが、醜いと複雑に思える：

Definition inv_func(H:Group):G H->G H. 
pose (inv_func_exists H). 
pose indefinite_description. 
generalize e0 s. 
trivial. 
Qed. 

最後に、私はそのinv_funcを証明したいと思い、実際に逆関数である：

Lemma inv_func_is_inverse:forall (H:Group), forall x:(G H), mult H x (inv_func H x)=e H. 

私はコックが知っていることがわかりますどのようにinv_funcが定義されたか（例えばPrint inv_func）、正式に補題を証明する方法はわかりません。

結論として、私は最後の補題を証明する方法と、inv_funcを定義するより良い方法を提案していただきたいと思います（私のグループの定義の下では、そのような関数の存在をグループ定義に含めません。この質問は、各要素の対応関係を証明し、関数としてこの対応を構築する必要がある他の多くの状況でも適切です）。

Answer 1

ご質問の中にはかなりの質問があります。私はそれらのすべてを解決しようとするでしょう：

• まず、{x | P}上exists x, P +説明を好む理由はない、確かに、あなたがそうする奇妙なようです。 {x | P}は「計算できるxが存在する」と完全に有効です。私はあなたのグループでその定義を使用したいと思います。

• 第2に、戦術を使用して定義を作成するときは、コマンドDefinedを使用して校正を終了する必要があります。 Qedを使用すると、定義が「不透明」であることが宣言されます。つまり、展開できないため、証明ができなくなります。

• あなたの定義から証人を抽出する方法は、投影を使用することです。この場合、proj1_sig。

上記のすべての私たちが到着使い方：

Definition inv_func' (H:Group) (x : G H) : G H. 
Proof. 
destruct (inverse H x) as [y _]. 
exact y. 
Defined. 

Definition inv_func (H:Group) (x : G H) : G H := proj1_sig (inverse H x). 

Lemma inv_func_is_inverse (H:Group) (x: G H) : mult H x (inv_func H x) = e H. 
Proof. now unfold inv_func; destruct (inverse H x). Qed.