Coq - 如何命名內聯的假設

Question

我想在P-> Q中使用P的名稱。合理的是陳述一個類型P> Q的定理，其中Q取決於P.

在以下示例中，我需要替換'???'。

我知道我可以打開一個部分，並將（x <> 0）作爲帶名稱的參數。然後，在關閉該部分之後，我得到了一些東西，但我想只在一行中說明thm2。

（Ofcourse，下面的例子是有點傻了。這只是證明我的問題的例子。）

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.