Proving exist quantification

Aug 12, 2013 at 5:29 PM
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!
Aug 16, 2013 at 2: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 non-empty 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
Aug 20, 2013 at 2:54 PM
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
Aug 27, 2013 at 2: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 if-then-else 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
Aug 27, 2013 at 3:53 PM

Hi Valentin, I see. Thank you!

Who is the best Z3 expert we could ask if we want to learn the proofs better?

Annie

Sep 2, 2013 at 10:31 AM
Edited Sep 2, 2013 at 10:32 AM
Hi Annie,

if you have specific questions regarding Z3, you can ask them on stackoverflow (e.g., http://stackoverflow.com/questions/11531589/difference-between-z3-and-coq). 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
Sep 2, 2013 at 12:28 PM
Hi Valentin, Thank you! We will try to tell which is which. :-) Best, Annie