
Hi all,
I try to prove that for set has at least two elements, there exists an element less than all other element in set.
Here I have two version, one is this set has exact two elements p1 and p2, and the other is not.
http://rise4fun.com/Dafny/uOtg
http://rise4fun.com/Dafny/YjTL
But dafny could not prove the later one, I wonder if I did something wrong here.
Thanks!


Developer
Aug 16, 2013 at 1:08 PM

Hi,
I assume that for a set of two elements the prover simply instantiates the quantifiers to show that the property holds. For an arbitrary nonempty set you can use induction to prove the property as follows:
http://rise4fun.com/Dafny/pfxH.
The base case (singleton set "{e}") is automatically proven and the step case is proven after invoking the lemma for the set "s  {e}".
Best regards,
Valentin



Thank you, Valentin! How does dafny know that {e} is the base case? Without the recursion/induction, Dafny doesn't seem to terminate. Is that because it is trying to do proof by contradiction and gets into an infinite loop, so to speak?
Another question: in http://rise4fun.com/Dafny/Njjm, did Dafny do the proof by contradiction? Thanks! Annie


Developer
Aug 27, 2013 at 1:40 PM

Hi Annie.
Thank you, Valentin! How does dafny know that {e} is the base case? Without the recursion/induction, Dafny doesn't seem to terminate. Is that because it is trying to do proof by contradiction and gets into an infinite loop, so to speak?
The ifthenelse statement indicates that there are two cases and the else branch corresponds to the base case. Yes, if Dafny does not terminate it might be because the prover gets stuck in a matching loop.
Another question: in
http://rise4fun.com/Dafny/Njjm, did Dafny do the proof by contradiction?
This is hard to know for sure since it is not really feasible to inspect the proofs that the underlying theorem prover (Z3) produces.
Best regards,
Valentin



Hi Valentin, I see. Thank you!
Who is the best Z3 expert we could ask if we want to learn the proofs better?
Annie


Developer
Sep 2, 2013 at 9:31 AM
Edited Sep 2, 2013 at 9:32 AM

Hi Annie,
if you have specific questions regarding Z3, you can ask them on stackoverflow (e.g.,
http://stackoverflow.com/questions/11531589/differencebetweenz3andcoq). Leonardo (one of the Z3 developers) usually replies to questions there.
However, if you have questions about proving certain things in Dafny this forum is probably more helpful.
Best regards,
Valentin



Hi Valentin, Thank you! We will try to tell which is which. :) Best, Annie

