diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-27 18:02:28 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-27 18:02:28 +0200 |
| commit | 046fd92ae9d233a8d3ffb0e1f5a4ff76f1129744 (patch) | |
| tree | c9a18867fb0a6b6b2f0d86b77cc009dcd763e888 /theories | |
| parent | bb383ae81838aabae9fe77fdbeaecf46bb85b4f2 (diff) | |
| parent | 84e274fb6d36bbd8306c2977520ebe1cf410349a (diff) | |
Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/QArith_base.v | 20 | ||||
| -rw-r--r-- | theories/QArith/Qabs.v | 7 |
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. |