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

Alan Schmitt alan.schmitt at polytechnique.org
Mon Nov 19 14:21:48 CET 2012


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


I feel like I'm missing something obvious here. Is there a way to give a
hint to why3 as how to solve this?



More information about the Why3-club mailing list