Search code examples
proofdafny

How to extract a variable from an exist clause

I am triying to make a simple reduction to absurd proof with Dafny, normally when I do so (in real life mathematics) I use arguments like "ok, now lets choose a p that fullfills this property which we know exists because [...]" and then continue to use that p for the rest of the demostration. I am triying to replicate this form of reasoning with Dafny but I don't know how to "extract" the variable p from the "exists" clause. Hope you can help me!

if(exists p | ini <= p < border <= fin :: is_true_on_segment(s, p, fin, P)){
                    closed_on_left_lemma(P);
                    upper_limit(s, ini, fin - 1, P);

                    assert exists p | ini <= p < border <= fin :: is_true_on_segment(s, p, fin - 1, P);

                    assert false;
                }

It seems to be a standard mathematical procedure, so I hope there is a way to do it. I have tried to search the docs and the book "Program Proofs" without success.

Solution

  • The syntax is

    var p :| ini <= p < border <= fin && is_true_on_segment(s, p, fin - 1, P);

    which will bring into scope a variable p that satisfies those predicates.