Dafny: Allow < and > for comparisons of datatype values (which then compares their ranks)

2 files changed, 2 insertions, 6 deletions

diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy
index 9668afb9..72415fea 100644
--- a/Test/dafny0/Substitution.dfy
+++ b/Test/dafny0/Substitution.dfy
@@ -69,7 +69,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
 

 static function SubstSeq(/*ghost*/ parent: Expression,

                          q: seq<Expression>, v: int, val: int): seq<Expression>

-  requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);

+  requires (forall a :: a in q ==> a < parent);

   decreases parent, false, q;

 {

   if q == [] then [] else

@@ -107,7 +107,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
 

 static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,

                                     v: int, val: int)

-  requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);

+  requires (forall a :: a in q ==> a < parent);

   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>

             SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));

diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index e5fe9473..b4fab490 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -33,7 +33,6 @@ class SumOfCubes {
     while (k < m) 

       invariant n <= k && k <= m;

       invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);

-      decreases m - k;

     {

       k := k + 1;

     }

@@ -65,7 +64,6 @@ class SumOfCubes {
     while (i < k)

       invariant i <= k;

       invariant SumEmDown(0, i) == GSum(i) * GSum(i);

-      decreases k - i;

     {

       call Lemma2(i);

       i := i + 1;

@@ -81,7 +79,6 @@ class SumOfCubes {
     while (i < k)

       invariant i <= k;

       invariant 2 * GSum(i) == i * (i - 1);

-      decreases k - i;

     {

       i := i + 1;

     }

@@ -102,7 +99,6 @@ class SumOfCubes {
     while (k < m)

       invariant n <= k && k <= m;

       invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);

-      decreases m - k;

     {

       k := k + 1;

     }