Re: [Why3-club] Why3-club Digest, Vol 86, Issue 4

[Claude Marché]

Le 10/02/2018 à 15:03, Ziqing Luo a écrit :
> 
> Thanks for telling me that provers have problems with "existential" goals.
> 

have "problems" is not really well said. Never forget that provers are
trying to solve queries that are indeed undecidable. Existential
quantifiers are just one of the multiple sources of undecidability.

Regarding your initial question: when you add "k=2" in hypothesis might
add "2" as a potential trigger for the prover, in other words it gives
it a "hint" that trying the witness "2" might solves the goal.

Depending on your initial problem, you should consider translating "0 <=
k <= 3 " into "k=0 \/ k=1 \/ k=2 \/ k=3"

- Claude

-- 
Claude Marché  | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France   |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] Why3-club Digest, Vol 86, Issue 4

[Ziqing Luo]

Hi,

Sorry, I forgot to mention that I used why3 v0.88.3 with theorem provers:
z3(v4.6.0), alt-ergo (v2.0.0) and cvc4 (v1.5).

I also tried z3(4.4.0) but it still doesn't work for me.

Thanks for telling me that provers have problems with "existential" goals.

Ziqing Luo
University of Delaware


On Sat, Feb 10, 2018 at 5:57 PM, 
wrote:

> Send Why3-club mailing list submissions to
> why3-club@lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> or, via email, send a message with subject or body 'help' to
> why3-club-requ...@lists.gforge.inria.fr
>
> You can reach the person managing the list at
> why3-club-ow...@lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Why3-club digest..."
>
>
> Today's Topics:
>
>1. A predicate that cannot be proved by why3 (Ziqing Luo)
>2. Re: A predicate that cannot be proved by why3
>   (Jean-Christophe Filliatre)
>
>
> --
>
> Message: 1
> Date: Sat, 10 Feb 2018 09:42:26 +0800
> From: Ziqing Luo 
> To: why3-club@lists.gforge.inria.fr
> Subject: [Why3-club] A predicate that cannot be proved by why3
> Message-ID:
>  gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear Why3 Club,
>
> I have a why3 script that I think is relatively simple but why3 cannot
> prove it.  I wander if I did anything wrong.
>
> *constant X : (map int int)*
>
> *context:
>*
>
> *  X[4] = X[6] && X[5] = X[6] && X[6] < X[7]
>*
>
> *predicate:
>*
>
> *  exists k : int.  0 <= k && k <= 3 && not(X[k+4] = X[k+5])*
>
> It is obvious that there exists such a k = 2.   If I modify the predicate a
> lilltle bit to :
>
> *predicate:
>*
>
> *  exists k : int.  0 <= k && k <= 3 && k = 2 && not(X[k+4] = X[k+5])*
>
>
> why3 then has no problem to prove it.  So I'm confused that why why3 cannot
> prove the original case.
>
> Thanks,
> Ziqing Luo
> University of Delaware
>
> The following is the whole why3 script:
>
> theory Why3Query_408
>
> use import int.Int
>
> use import map.Map
>
> constant _X : (map int int)
>
>
> (*
>
>
>
>
>
> context:
>
>
>   X[4] = X[6]
>
>
>   X[5] = X[6]
>
>
>   X[6] < X[7]
>
>
>
>
>
> predicate:
>
>
>   exists k : int.  0 <= k && k <= 3 && not(X[k+4] = X[k+5])
>
>
>
>
>
>  *)
>
>
> predicate context = (((0)  =  ((get _X (4))  +  ((-1)  *  (get _X (6)
> &&
>
> ((0)  =  ((get _X (5))  +  ((-1)  *  (get _X (6)
> &&
>
> (((get _X (6))  +  ((-1)  *  (get _X (7)))  +  (1))
> <=  (0)))
>
>
> goal G0: context -> ((exists k : int. (((k  +  (-3))  <=  (0))  &&  ((0)
> <=  k)  &&
>
> (not ((0)  =  ((get _X (k  +  (4)))  +  ((-1)  *
> (get _X (k  +  (5) )
>
>
> end
> -- next part --
> An HTML attachment was scrubbed...
> URL:  attachments/20180210/8bf8edcd/attachment-0001.html>
>
> --
>
> Message: 2
> Date: Sat, 10 Feb 2018 10:57:42 +0100
> From: Jean-Christophe Filliatre 
> To: why3-club@lists.gforge.inria.fr
> Subject: Re: [Why3-club] A predicate that cannot be proved by why3
> Message-ID: <5a7ec216.6030...@lri.fr>
> Content-Type: text/plain; charset=utf-8
>
> Hi,
>
> When you say "why3 cannot prove it", it means "the provers installed on
> my machine and called from Why3 cannot prove it". So listing the provers
> you've tried on this example would be helpful.
>
> Indeed, ATPs have trouble proving existential goals, especially when
> combined with arithmetic (SMT solvers struggle with arithmetic triggers,
> and TPTP provers sometimes simply do not have support for arithmetic).
>
> But at least Z3 4.4.0 was able to prove your goal on my machine.
>
> Hope this helps,
> --
> Jean-Christophe
>
>
> On 10/02/2018 02:42, Ziqing Luo wrote:
> > Dear Why3 Club,
> >
> > I have a why3 script that I think is relatively simple but why3 cannot
> > prove it.  I wander if I did anything wrong.
> >
> > *constant X : (map int int)*
> >
> > *context:
> >*
> >
> > *  X[4] = X[6] && X[5] = X[6] && X[6] < X[7]
> >  *
> >
> > *predicate:
> >*
> >
> > *  exists k : int.  0 <= k && k <= 3 && not(X[k+4] = X[k+5])*
> >
> >
> > It is obvious that there exists such a k = 2.   If I modify the
> > predicate a lilltle bit to :
> >
> >