CODEWITHSUNDEEP
coqdependent-type
tomjerry7
tomjerry7

Reputation: 101

Coq - how to name an assumption inline

I would like to have some name for P in P->Q. The rational is to state a theorem of type P->Q in which Q depends on P.

In the following example I need to replace the '???'.

I know I could open a Section and have (x<>0) as a Parameter with a name. Then after I close the section I get something to my thm2, but I would like to just state thm2 in one line.

(Ofcourse, the following example is somewhat silly. That's just an example to demonstrate my problem.)

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.

Now, the ??? should refer Coq to the assumption that x>0. I couldn't find a way to refer to that assumption in the same line in which it is stated.

Upvotes: 0

Views: 123

Answers (1)

gallais
gallais

Reputation: 12103

You can use forall to introduce named binders: forall (x:Q) (p : x>0), (...). Which gives us:

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.

Upvotes: 3

Related Questions