3
$\begingroup$

I have made the following code, and I'm in stuck.


From mathcomp Require Import all_ssreflect.

Require Import QArith.


Lemma Lem1 (x : Q) (y : Q) :
not (x <= y) <-> x > y.
Proof.
split. apply Qnot_le_lt. apply Qlt_not_le.
Qed.

Lemma Zlt_or_eq (n : Z) (m : Z) :
(n < m)%Z \/ (n = m)%Z <-> (n <= m)%Z.
Proof.
assert (H : (n = m)%Z = (inject_Z n == inject_Z m)).
{ unfold inject_Z. unfold Qeq. simpl.
  rewrite Z.mul_comm. rewrite Z.mul_1_l.
  rewrite Z.mul_comm. rewrite Z.mul_1_l. reflexivity. }
rewrite Zle_Qle. rewrite Zlt_Qlt. rewrite H.
rewrite Qle_lteq. reflexivity.
Qed.

Theorem Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.
rewrite Lem1. unfold Qle. unfold Qlt.
rewrite -Zlt_or_eq.

Edit : Sorry, my question is about $\mathbb{Q}$, however my previous theorem is related to $\mathbb{Z}$. I edit it.


When I go to the last line, I want to apply Ztrichotomy, $$\forall n, ~m : \mathbb{Z} ~:~ n < m ~\lor ~ n = m ~ \lor ~ n > m.$$

However, my last term is (Qnum y * QDen x < Qnum x * QDen y)%Z,

instead of (Qnum x * QDen y > Qnum y * QDen x)%Z.

I want to change the order direction in Z-scope.

$\endgroup$
4
  • $\begingroup$ What have you leared? What are your (failed) attempts? Providing these helps us better answer your question. $\endgroup$
    – Trebor
    Jul 12, 2022 at 5:27
  • $\begingroup$ @Trebor I add my attempt. $\endgroup$ Jul 12, 2022 at 5:45
  • 1
    $\begingroup$ How much on the standard library are you ready to use? Your use of Ztrichotomy lets me infer that you are ready to use ZArith, which already contains a lemma corresponding to what you want to prove, called Z.le_gt_cases. $\endgroup$ Jul 12, 2022 at 8:26
  • 1
    $\begingroup$ Do you want to prove your lemma for rational numbers (Q, fractions), or for integers (Z)? Your example is for Z but your title mentions Q. $\endgroup$
    – Ana Borges
    Jul 12, 2022 at 10:47

1 Answer 1

1
$\begingroup$

You can use the following tactic setoid_rewrite <- Z.gt_lt_iff at 2., and then use Ztrichotomy to conclude. To decompose a bit what happens, setoid_rewrite is a tactic that allows rewriting with other relations than equality, provided the contexts under which the rewriting happens is "nice enough". Concretely, here the relation we are rewriting with is logical equivalence <->, and we are rewriting under \/, which respects equivalence, so everything goes well. The <- part of the tactic is the equivalent of - in mathcomp, meaning we want to rewrite from right to left rather than left to right, and the at 2 part selects the part of the term we want to rewrite (the second one matching the conclusion of Z.gt_lt_iff).

$\endgroup$

Your Answer

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

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