copy over the real trigger

dafny-lang · Oct 3, 2024 · e7419fd · e7419fd
1 parent 0d90e8e
commit e7419fd
Showing 1 changed file with 10 additions and 10 deletions.
diff --git a/src/NonlinearArithmetic/DivMod.dfy b/src/NonlinearArithmetic/DivMod.dfy
@@ -209,7 +209,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)}
               :: 0 < d &&  R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d)
   {
-    forall (a: int, b: int, d: int, R: int {:trigger true} | 0< d &&  R == a%d + b%d - (a+b)%d)
+    forall (a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d &&  R == a%d + b%d - (a+b)%d)
       ensures d*((a+b)/d) - R == d*(a/d) + d*(b/d)
     {
       LemmaDividingSums(a, b, d, R);
@@ -724,7 +724,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, a: int, d: int {:trigger a / d, x * d, x * a}
               :: 0 < x && 0 <= a && 0 < d ==> 0 < x * d  &&  a / d == (x * a) / (x * d)
   {
-    forall x: int, a: int, d: int {:trigger true} | 0 < x && 0 <= a && 0 < d
+    forall x: int, a: int, d: int {:trigger a / d, x * d, x * a} | 0 < x && 0 <= a && 0 < d
       ensures 0 < x * d  &&  a / d == (x * a) / (x * d)
     {
       LemmaDivMultiplesVanishQuotient(x, a, d);
@@ -747,7 +747,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, r: int, d: int {:trigger d * ((a + r) / d)}
               :: 0 < d && a % d == 0 && 0 <= r < d ==> a == d * ((a + r) / d)
   {
-    forall a: int, r: int, d: int {:trigger true} | 0 < d && a % d == 0 && 0 <= r < d
+    forall a: int, r: int, d: int {:trigger d * ((a + r) / d)} | 0 < d && a % d == 0 && 0 <= r < d
       ensures a == d * ((a + r) / d)
     {
       LemmaRoundDown(a, r, d);
@@ -770,7 +770,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, b: int, d: int {:trigger (d * x + b) / d}
               :: 0 < d && 0 <= b < d ==> (d * x + b) / d == x
   {
-    forall x: int, b: int, d: int {:trigger true} | 0 < d && 0 <= b < d
+    forall x: int, b: int, d: int {:trigger (d * x + b) / d} | 0 < d && 0 <= b < d
       ensures (d * x + b) / d == x
     {
       LemmaDivMultiplesVanishFancy(x, b, d);
@@ -936,7 +936,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, b: int, c: int {:trigger b * (a / b) % (b * c)}
               :: 0 <= a && 0 < b && 0 < c ==> 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1)
   {
-    forall a: int, b: int, c: int {:trigger true} | 0 <= a && 0 < b && 0 < c
+    forall a: int, b: int, c: int {:trigger b * (a / b) % (b * c)} | 0 <= a && 0 < b && 0 < c
       ensures 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1)
     {
       LemmaPartBound1(a, b, c);
@@ -1205,7 +1205,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, m: int {:trigger (x + y) % m}
               :: 0 < m ==> (x + (y % m)) % m == (x + y) % m
   {
-    forall x: int, y: int, m: int {:trigger true} | 0 < m
+    forall x: int, y: int, m: int {:trigger (x + y) % m} | 0 < m
       ensures (x + (y % m)) % m == (x + y) % m
     {
       LemmaAddModNoopRight(x, y, m);
@@ -1243,7 +1243,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, m: int {:trigger (x - y) % m}
               :: 0 < m ==> (x - (y % m)) % m == (x - y) % m
   {
-    forall x: int, y: int, m: int {:trigger true} | 0 < m
+    forall x: int, y: int, m: int {:trigger (x - y) % m} | 0 < m
       ensures (x - (y % m)) % m == (x - y) % m
     {
       LemmaSubModNoopRight(x, y, m);
@@ -1306,7 +1306,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, d: int, q: int, r: int {:trigger q * d + r, x % d}
               :: d != 0 && 0 <= r < d && x == q * d + r ==> q == x / d && r == x % d
   {
-    forall x: int, d: int, q: int, r: int {:trigger true} | d != 0 && 0 <= r < d && x == q * d + r
+    forall x: int, d: int, q: int, r: int {:trigger q * d + r, x % d} | d != 0 && 0 <= r < d && x == q * d + r
       ensures q == x / d && r == x % d
     {
       LemmaFundamentalDivModConverse(x, d, q, r);
@@ -1499,7 +1499,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, k: int, d: int {:trigger x % (d * k)}
               :: 1 < d && 0 < k ==> 0 < d * k && x % d <= x % (d * k)
   {
-    forall x: int, k: int, d: int {:trigger true} | 1 < d && 0 < k
+    forall x: int, k: int, d: int {:trigger x % (d * k)} | 1 < d && 0 < k
       ensures d * k > 0 && x % d <= x % (d * k)
     {
       LemmaModOrdering(x, k, d);
@@ -1563,7 +1563,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, z: int {:trigger y * z, x % y}
               :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && (x % y) % (y * z) < y
   {
-    forall x: int, y: int, z: int {:trigger true} | 0 <= x && 0 < y && 0 < z
+    forall x: int, y: int, z: int {:trigger y * z, x % y} | 0 <= x && 0 < y && 0 < z
       ensures y * z > 0 && (x % y) % (y * z) < y
     {
       LemmaPartBound2(x, y, z);