Quantifiers and arithmetic

Coordinator
Jul 29, 2015 at 10:17 PM
Here is a question I received about trying to prove universal mathematical facts. It leads to an issues about quantifiers and matching triggers.

Hi Rustan,

I have a question about the introduction of quantifiers. In the code below, I am trying to prove that
           Mod(a,c)!=0  implies forall i::  a!=i*c
I am attaching the proof (Mod and Div) I developed, and which Dafny rejected. I cannot understand why it does so, because, I thought that once B and C go thought, D and A should go through too.


I also developed another, schematic proof which introduces universal quantifiers (Qunatifiers), which does go through.

I do not understand why the difference. More importantly, how can we make the first proof go through?

Best wishes,

Sophia
// 1st Example: Mod and Div
function Md(a:int, c:int) : int
  requires a>0 && c>0
  ensures Md(a,c)>= 0
 
function Dv(a:int, c:int) : int
  requires a>0 && c>0 
  ensures Dv(a,c)>= 0
 
lemma BasicLemma(a:int, c:int) 
  requires a>c && c>0
  ensures Dv(a,c)>=0 && Md(a,c)>=0 &&
          a==c*Dv(a,c)+Md(a,c) && Md(a,c)<c
 
lemma ModLemmaAux(a:int, c:int, d: int, m:int, i: int) 
  requires a>0 && c>0 && c<a && m>0 && m<c && i>d>=0 && a==c*d + m
  ensures c*i != a
 
 
lemma ModLemma(a:int, c:int, d: int, m:int) 
  requires a>c && c>0 && d==Dv(a,c) && m==Md(a,c) && m>0
  ensures forall i:int:: a!=i*c           // A: Error here
{        
  forall (i: int)
    ensures c*i!=a         // B: OK
  { if ( i> d )
    { calc {
        c*i;
      != { BasicLemma(a,c);
           ModLemmaAux(a,c,d,m,i);  }
        a;
      }
      assert c*i != a;          
    } 
    else if (i==d)
    { BasicLemma(a,c);
      assert a == c*d + m;
      assert c*i!=a; 
    }                           
    else {
      BasicLemma(a,c);
      assert c*i!=a;
    }                           
 
    assert c*i!=a;                     // C: OK
  }
 
  assert forall i:int:: (a!=i*c);       // D: Getting Error here
}
 
// 2nd Example: Quantifiers
 
predicate P(a:int) 
 
predicate Q(a:int)
 
predicate R(a:int)
 
lemma NegImpliesP(a:int)
  requires a<0
  ensures P(a)
 
lemma PosImpliesQ(a:int)
  requires a>0
  ensures Q(a)
 
lemma PImpliesR(a:int)
  requires P(a)
  ensures R(a)
 
lemma QImpliesR(a:int)
  requires Q(a)
  ensures R(a)
 
lemma ZeroImpliesR()
  ensures R(0)

lemma AllR()
  ensures forall i:int :: R(i)
{
  forall (i: int) ensures  R(i);
  { if (i>0)
    { PosImpliesQ(i); 
      QImpliesR(i);
    }
    else if (i==0)
    { ZeroImpliesR(); }
    else 
    {
      assert i<0;
      NegImpliesP(i);
      PImpliesR(i);
    }
  }
  assert forall i:int :: R(i);
}
Coordinator
Jul 29, 2015 at 10:22 PM
The problem is that the quantifier forall i:int:: a!=i*c has no matching trigger. A matching trigger is a term (that is, an expression) that gives the verifier a clue that a universal quantifier should be instantiated. For example, if (in a precondition, say) you write a quantifier like
requires forall i :: 0 <= i ==> f(i) < 100
then you will be able to verify
assert f(20) + f(22) < 200;
This is because the verifier will use f(_) as the matching trigger for the quantifier, and then the presence of the terms f(20) and f(22) in the assertion will cause the quantifier to be instantiated with i:=20 and with i:=22. As another example, if you tried to prove
assert f(-18) + f(22) < 200;
then the verifier will instantiate the quantifier with i:=-18 and with i:=22, but the instantiation i:=-18 does not give any information about f(22), so the verifier will complain about not being able to verify the assertion.

Consider an example that involves another quantifier:
assert forall a,b :: 0 <= a && 0 <= b ==> f(a) + f(b) < 200;
Here, the verifier will consider an arbitrary a and b, and will be able to verify the body of the quantifier because it will instantiate the quantifier in the precondition with i:=a and with i:=b.

How did the verifier come up with the trigger f(_) in the first place? It looks in the body of the quantifier and tries to find expressions that involve the bound variable of the quantifier, like f(i) above. There are certain rules about what can be a trigger. Triggers cannot contain interpreted symbols, that is, boolean and arithmetic operators with a predefined meaning, like +, &&, <=, and ==. In your example, the quantifier:
forall i :: a != i*c
has no subexpression that makes an allowable trigger. Therefore, you can’t even prove something as obvious as:
lemma Test0(a: int, c: int)
  requires forall i :: a != i*c
{
  assert forall i :: a != i*c;  // error reported here
}
This is a problem with trying to prove properties that involve only built-in arithmetic and no user-defined functions. The solution is to introduce a(n uninterpreted) synonym for the built-in operation, here *. The following verifies:
function Mul(x: int, y: int): int { x * y }
lemma Test1(a: int, c: int)
  requires forall i :: a != Mul(i,c)
{
  assert forall i :: a != Mul(i,c);
}
In this example, Mul(_,c) gets picked as the matching trigger for the quantifier in the precondition, so when trying to prove a != Mul(i,c) for an arbitrary I in the assertion, the desired instantiation of the quantifier in the precondition takes places.

(There is actually a command-line option in Dafny that does this for you, namely /noNLarith. However, using this mode also disables more of non-linear arithmetic than you might like.)

I hope this explanation helps a bit. Do you mind if I post it on the Discussion board on dafny.codeplex.com?

Rustan

PS. There are other, more cryptic, workarounds, including the following:
function Id(x: int): int { x }
lemma Test2(a: int, c: int)
  requires forall i :: a != Id(i)*c
{
  assert forall i :: a != Id(i)*c;
}
 
predicate LookHere(i: int) { true }
lemma Test3(a: int, c: int)
  requires forall i :: LookHere(i) && a != i*c
{
  assert forall i :: LookHere(i) && a != i*c;
}
Marked as answer by rustanleino on 7/29/2015 at 2:22 PM