From 6a957f5633243216dea5daf3f5b2c29e168714a7 Mon Sep 17 00:00:00 2001
From: Sandro Stucki <sandro.stucki@gmail.com>
Date: Wed, 19 Aug 2015 09:17:37 +0200
Subject: [PATCH] Adds test case illustrating reasoning by implication.
---
.../verification/proof/implication.scala | 59 +++++++++++++++++++
1 file changed, 59 insertions(+)
create mode 100644 testcases/verification/proof/implication.scala
diff --git a/testcases/verification/proof/implication.scala b/testcases/verification/proof/implication.scala
new file mode 100644
index 000000000..b2e394ba2
--- /dev/null
+++ b/testcases/verification/proof/implication.scala
@@ -0,0 +1,59 @@
+package test
+
+import leon.lang._
+import leon.proof._
+
+object ImplicationExample {
+ /*
+ * Some implication example.
+ *
+ * This example actually is based on incorrect premises but
+ * the proof in itself should correct.
+ */
+
+ sealed abstract class Animal
+ case class Insect() extends Animal
+ case class Mamal() extends Animal
+
+ sealed abstract class AnimalKind
+ case object InsectKind extends AnimalKind
+ case object MamalKind extends AnimalKind
+
+ sealed abstract class LegsProperty
+ case object HasEigthLegs extends LegsProperty
+ //case object HasTwoLegs extends LegsProperty
+
+ sealed abstract class PlayerKind
+ case object PockerKind extends PlayerKind
+ //
+
+ val jeff = Insect()
+
+ def isEqual(a: Animal, b: Animal): Boolean = a == b
+
+ def isKindOf(a: Animal, k: AnimalKind): Boolean = a match {
+ case Insect() => k == InsectKind
+ case Mamal() => k == MamalKind
+ }
+
+ def hasLegsProperty(k: AnimalKind, l: LegsProperty): Boolean = k match {
+ case InsectKind => l == HasEigthLegs
+ case MamalKind => l != HasEigthLegs
+ }
+
+ def isKindOf(l: LegsProperty, p: PlayerKind): Boolean = l match {
+ case HasEigthLegs => p == PockerKind
+ }
+
+ def implies(a: Boolean, b: Boolean) = a ==> b
+
+ // Jeff plays Poker
+ def lemma(animal: Animal): Boolean = {
+ isEqual(animal, jeff) ==>
+ isKindOf(jeff, InsectKind) ==>
+ hasLegsProperty(InsectKind, HasEigthLegs) ==>
+ isKindOf(HasEigthLegs, PockerKind)
+ }.holds
+
+}
+
--
GitLab