aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-27 18:02:28 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-27 18:02:28 +0200
commit046fd92ae9d233a8d3ffb0e1f5a4ff76f1129744 (patch)
treec9a18867fb0a6b6b2f0d86b77cc009dcd763e888 /theories/QArith
parentbb383ae81838aabae9fe77fdbeaecf46bb85b4f2 (diff)
parent84e274fb6d36bbd8306c2977520ebe1cf410349a (diff)
Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful
Diffstat (limited to 'theories/QArith')
-rw-r--r--theories/QArith/QArith_base.v20
-rw-r--r--theories/QArith/Qabs.v7
2 files changed, 27 insertions, 0 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a19f9f902..5996d30f2 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -171,6 +171,26 @@ Proof.
auto with qarith.
Qed.
+Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.
+Proof.
+ apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_refl x: Qeq_bool x x = true.
+Proof.
+ rewrite Qeq_bool_iff. now reflexivity.
+Qed.
+
+Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.
+Proof.
+ rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.
+Proof.
+ rewrite !Qeq_bool_iff; apply Qeq_trans.
+Qed.
+
Hint Resolve Qnot_eq_sym : qarith.
(** * Addition, multiplication and opposite *)
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 116aa0d42..ec2ac7832 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -100,6 +100,13 @@ rewrite Z.abs_mul.
reflexivity.
Qed.
+Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q).
+Proof.
+ intros [n d]; simpl.
+ unfold Qinv.
+ case_eq n; intros; simpl in *; apply Qeq_refl.
+Qed.
+
Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).
Proof.
unfold Qminus, Qopp. simpl.