[Why3-club] Suggesting the use of a lemma in an assertion

Alan Schmitt alan.schmitt at polytechnique.org
Mon Nov 19 14:36:32 CET 2012


Sorry for the noise, I needed to increase the timeout. The context was
too big and more time was needed.

Alan

Alan Schmitt <alan.schmitt at polytechnique.org> writes:

> Hello,
>
> I'm almost finished with a why3 proof, with the exception of one
> assertion (required to finish the proof) that none of the installed
> prover can deal with (Alt-Ergo, CVC3, Spass, Z3). What I find surprising
> is that this is an instance of a lemma.
>
> Here is the relevant information, including the lemma I think should be
> used (taken from the top-right pane of why3ide).
>
> #+BEGIN_SRC why3
>
> axiom permut_exists :
>   forall a1:map int 'a, a2:map int 'a.
>    forall l:int, u:int.
>     permut_sub a1 a2 l u ->
>      (forall i:int.
>        l <= i /\ i < u ->
>         (exists j:int. (l <= j /\ j < u) /\ a2[i] = a1[j]))
>
> constant n : int
>
> constant i : int
>
> constant a5 : map int int
>
> constant a7 : map int int
>
> axiom H23 : permut_sub a5 a7 i n
>
> constant k : int
>
> axiom H27 : i <= k
>
> axiom H28 : k < n
>
> goal WP_parameter_quicksort :
>   exists l:int. (i <= l /\ l < n) /\ get a7 k = get a5 l
>
> @+END_SRC
>
> I feel like I'm missing something obvious here. Is there a way to give a
> hint to why3 as how to solve this?
>
> Thanks,
>
> Alan
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club



More information about the Why3-club mailing list