1
$\begingroup$

Suppose in Coq we have the following hypotheses:

x, y, z: Z
H : x < y
H0 : y < z

and I would like to introduce also the hypothesis

H1 : x < z

which follows from H and H0 using Z.lt_trans. Is there a better way to do this than the following?

assert (H1 : x < z). 
{ apply Z.lt_trans with y.
  exact H. exact H0.  }
$\endgroup$

2 Answers 2

5
$\begingroup$

You may for instance write specialize (Z.lt_trans _ _ _ H H0) as H1.

$\endgroup$
3
$\begingroup$

In addition to Pierre's answer, here are two more options.

First, you can use transitivity y instead of having to dig through the library to discover Z.lt_trans:

Require Import ZArith.
Open Scope Z.

Lemma rabbit (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  assert (H1 : x < z).
  { now transitivity y. }
  trivial.
Qed.

Second, you can use ssreflect have tactic like this:

Require Import ZArith.
Open Scope Z.
From Coq Require Import ssreflect.

Lemma chicken (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  have H1 : x < z by transitivity y.
  trivial.
Qed.

```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.