Coq - 如何命名内联假设
Coq - how to name an assumption inline
我想在 P->Q 中为 P 命名。有理数是陈述一个 P->Q 类型的定理，其中 Q 取决于 P.
在下面的示例中，我需要替换“???”。
我知道我可以打开一个部分并将 (x<>0) 作为具有名称的参数。然后在我关闭该部分后，我得到了一些东西到我的 thm2，但我想只在一行中说明 thm2。
（当然，下面的例子有点傻，这只是一个演示我的问题的例子。）
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。我找不到在声明该假设的同一行中引用该假设的方法。
您可以使用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.
我想在 P->Q 中为 P 命名。有理数是陈述一个 P->Q 类型的定理，其中 Q 取决于 P.
在下面的示例中，我需要替换“???”。
我知道我可以打开一个部分并将 (x<>0) 作为具有名称的参数。然后在我关闭该部分后，我得到了一些东西到我的 thm2，但我想只在一行中说明 thm2。
（当然，下面的例子有点傻，这只是一个演示我的问题的例子。）
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。我找不到在声明该假设的同一行中引用该假设的方法。
您可以使用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.