1
Vote

Assertion violation - induction hypothesis

description

Please, some help with the following assertion violation
http://rise4fun.com/Dafny/cLnNL

comments

lexicalscope wrote Sep 20, 2016 at 2:15 PM

Non-linear arithmetic is not decidable by the underlying SMT solver. So you probably need to give Dafny some more help with the % operator.

jiplucap wrote Oct 3, 2016 at 3:37 PM

http://rise4fun.com/Dafny/jsv2

In this case the induction hypothesis does not should be applied, but apparently it is applied, though one of its preconditions is violated.
I know that there is a simpler proof of the lemma, but I would like to know why this exactly works.

lexicalscope wrote Oct 3, 2016 at 4:26 PM

You can disable automatic induction using an anotation
lemma {:induction false} Lemma_SquareAndHalve(b:int, e:nat)

lexicalscope wrote Oct 3, 2016 at 4:29 PM

My guess is that the proof being constructed goes something like this:

http://rise4fun.com/Dafny/0FG7
function power(b:int,e:nat):int            
{ 
if e == 0 then 1 else b*power(b,e-1) 
}

lemma {:induction false} Lemma_SquareAndHalve(b:int, e:nat)
    requires e%2 == 0 && e >  0
    ensures power(b,e) == power(b*b,e/2);
{
if e == 2 { 
          assert power(b,2) == b*power(b,1) == power(b*b,1);
          }
else {
        calc {
             power(b*b,e/2);
             ==
             b*b*power(b*b,(e/2)-1);
             ==
             b*b*b*b*power(b*b,(e/2)-2);
             ==
             b*b*b*b*power(b*b,(e-4)/2);
             == {if(e>4) { Lemma_SquareAndHalve(b,e-4);} else {assert (e-4)/2 == 0;} }
             b*b*b*b*power(b,e-4);
             ==
             b*b*power(b,e-2);
             ==
             power(b,e);
             }
     }
}

jiplucap wrote Oct 3, 2016 at 5:01 PM

Thanks a lot.