[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
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
More information about the Why3-club
mailing list