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.