Coq - 仮定の名前をインラインで指定する方法

Question

P-> QにPの名前を付けたいと思います。合理的には、QがPに依存するP-> Q型の定理を述べることです。

次の例では、 '???'を置き換える必要があります。

私はセクションを開いて、（x <> 0）を名前付きパラメータとして持つことができます。その後、私がセクションを閉じると、私はthm2に何かを得ますが、私はthm2を1つの行に記述したいと思います。

（勿論、次の例では、多少愚かである。それは私の問題を実証するための単なる一例です。）今

Require Import QArith. 

Definition my_inv(x:Q)(x<>0):Q. 
intros. 
exact (1/x). 
Defined. 

Thm thm1: forall x:Q, x>0 -> x<>0. 
Proof. 
... 
Qed. 

Theorem thm2: forall x:Q, x>0-> (my_inv x (thm1 x ???)) > 0. 

、??? Coqをx> 0と仮定するべきである。私はそれが述べられているのと同じ行でその仮定を参照する方法を見つけることができませんでした。

Answer 1

forallを使用して、指定したバインダーを紹介することができます。forall (x:Q) (p : x>0), (...)これは私たちに与えます：

Require Import QArith. 

Definition my_inv(x:Q) (p : x <> 0):Q. 
intros. 
exact (1/x). 
Defined. 

Theorem thm1 : forall x:Q, x>0 -> x<>0. 
Proof. 
Admitted. 

Theorem thm2: forall (x:Q) (p : x>0), (my_inv x (thm1 x p)) > 0.