From cc2072ee09657aac25a71a11868b4e65ba30964c Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 14 Jul 2015 09:53:00 +0200
Subject: [PATCH] proving properties of equivalence over rationals
---
.../verification/math/RationalProps.scala | 20 +++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/testcases/verification/math/RationalProps.scala b/testcases/verification/math/RationalProps.scala
index 60d30a6c6..aec07246e 100644
--- a/testcases/verification/math/RationalProps.scala
+++ b/testcases/verification/math/RationalProps.scala
@@ -66,4 +66,24 @@ object RationalProps {
require(p.isRational && q.isRational && q.nonZero)
((p / q) * q) ~ p
} holds
+
+
+ /*
+ * properties of equivalence
+ */
+
+ def equivalentIsReflexive(p: Rational): Boolean = {
+ require(p.isRational)
+ p ~ p
+ } holds
+
+ def equivalentIsSymmetric(p: Rational, q: Rational): Boolean = {
+ require(p.isRational && q.isRational && p ~ q)
+ q ~ p
+ } holds
+
+ def equivalentIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+ require(p.isRational && q.isRational && r.isRational && p ~ q && q ~ r)
+ p ~ r
+ } holds
}
--
GitLab