Induction hypothesis doesn't work?

Sep 7, 2015 at 11:17 AM
http://rise4fun.com/Dafny/bVR

It has been simplified to just show the problem that the assert after the recursive call to the lemma should be satisfied, it is the induction hypothesis.
Sep 24, 2015 at 4:41 PM
Edited Sep 24, 2015 at 4:43 PM
seems caused by the encoding of mod operator? might be you can add a postcondition to help the induction:
http://rise4fun.com/Dafny/Vkos
Sep 25, 2015 at 10:36 AM
I suspect that it is not a problem with the mod operator, please check this:

http://rise4fun.com/Dafny/O70K
Sep 25, 2015 at 1:52 PM
Edited Sep 25, 2015 at 3:45 PM
Hi, as far as I remember, Dafny translates to Boogie, and Boogie has syntax for div and mod operator, but their operational semantics are not complete (since their operation semantics various from language to language, e.g. when negative numbers are involved).

So in general I think because of this level of incompleteness, when proof involves these operators, the user might need to help the verifier a little bit, e.g. give more information, rewrite the proof obligation to be simpler or expand/rewrite the definition of these operator. I find this is quite common during my experience with Dafny or Boogie.

There are probably other reasons behind why your second example does not verified (and I am really interested in knowing ;-) ). But I find the trick of help Dafny with more information of mod and div operator still applies:
http://rise4fun.com/Dafny/iTz3

Cheers, Zheng
Sep 28, 2015 at 12:16 PM

Hi Zheng,

>>>>> Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0

Of course, it is not provable in general, but (n/m)*m != n <==> n%m==0.

So, I used it as a trick to avoid the use of the mod operator.

Thanks,

Paqui

De: zcheng [email removed]
Enviado el: viernes, 25 de septiembre de 2015 15:52
Para: [email removed]
Asunto: Re: Induction hypothesis doesn't work? [dafny:644665]

From: zcheng

Hi, as far as I remember, Dafny translates to Boogie, and Boogie has syntax for div and mod operator, but their operational semantics are not complete (since their operation semantics various from language to language, e.g. when negative numbers are involved, or whether 1/2 == 0).

Because of this level of incompleteness, when trivial lemma involve these operators, the user might need to help the verifier a little bit, e.g. rewrite the proof obligation to be simpler or expand/rewrite the definition of these operator. I find this is quite common during my experience with Dafny or Boogie.

Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0

Cheers, Zheng

Oct 5, 2015 at 12:24 PM
Hi Zheng,
Back to your second example, correct me if I am wrong, I do not think it is provable, since (n/m)*m != n, e.g. (1/2) * 2 == 0
Of course, it is not provable in general, but (n/m)*m != n <==> n%m==0.
So, I used it as a trick to avoid the use of the mod operator.

Thanks,
Paqui