Skip to main content
Proof Assistants Beta

Return to Question

deleted 12 characters in body
Source Link
taylor.2317
taylor.2317
  • 1.3k
  • 8
  • 36

I makehave made the following code, and I'm in stuck. Please help me.

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.

I make the following code, and I'm in stuck. Please help me.

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.

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.

added 855 characters in body
Source Link
with-forest
with-forest
  • 387
  • 1
  • 8

How to prove "$x \le y$" or "$y < x$""$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

From mathcomp Require Import all_ssreflect.

Require Import QArith. 


Lemma Lem2Lem1 (ax : ZQ) (by : 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) :
(a<=bn < m)%Z \/ (bn = m)%Z <-> a(n <= m)%Z.
Proof.
assert (H : (an <= bm)%Z \/ (a = b)%Z(inject_Z \/n (a== >inject_Z bm)%Z).
{ applyunfold Ztrichotomyinject_Z. unfold Qeq. simpl.
  rewrite Z.mul_comm. rewrite Z.mul_1_l.
  rewrite Z.mul_comm. rewrite Z.mul_1_l. reflexivity. }
destructrewrite Zle_Qle. rewrite Zlt_Qlt. rewrite H.
-rewrite leftQle_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.

AndEdit : Sorry, my question is about $\mathbb{Q}$, however my previous theorem is related to $\mathbb{Z}$. I could not proceededit 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.

How to prove "$x \le y$" or "$y < x$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Lem2 (a : Z) (b : Z) : 
(a<=b)%Z \/ (b < a)%Z.
Proof.
assert (H : (a < b)%Z \/ (a = b)%Z \/ (a > b)%Z).
{ apply Ztrichotomy. }
destruct H.
- left.

And I could not proceed.

How to prove "$x \le y$" or "$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

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.

deleted 37 characters in body; edited title
Source Link
with-forest
with-forest
  • 387
  • 1
  • 8

How to prove "$x \le y$" or "not $(x \le y)$""$y < x$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

 
From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Qle_totalLem2 (xa : QZ) (yb : QZ) :
x <= y
(a<=b)%Z \/ not (xb <=< ya)%Z.
Proof.

My trial is as follows :

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Lem1assert (xH : Q) (ya :< Qb)%Z :
not\/ (xa <== yb)%Z <->\/ y(a <> x.
Proofb)%Z).
split. apply Qnot_le_lt.{ apply Qlt_not_le.
QedZtrichotomy.

Lemma Qle_total (x : Q) (y : Q) :}
x <= y \/ not (x <=destruct y).
ProofH.
rewrite- Lem1left.

And I could not proceed.

How to prove "$x \le y$" or "not $(x \le y)$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.

My trial is as follows :

From mathcomp Require Import all_ssreflect.

Require Import QArith.

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

Lemma Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.
rewrite Lem1.

And I could not proceed.

How to prove "$x \le y$" or "$y < x$" for rational numbers $x$ and $y$ in Coq?

I make the following code, and I'm in stuck. Please help me.

 
From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Lem2 (a : Z) (b : Z) : 
(a<=b)%Z \/ (b < a)%Z.
Proof.
assert (H : (a < b)%Z \/ (a = b)%Z \/ (a > b)%Z).
{ apply Ztrichotomy. }
destruct H.
- left.

And I could not proceed.

added 357 characters in body
Source Link
with-forest
with-forest
  • 387
  • 1
  • 8
Source Link
with-forest
with-forest
  • 387
  • 1
  • 8