[Why3-club] Consistency of map theory

Alan Schmitt alan.schmitt at polytechnique.org
Thu Nov 22 14:48:53 CET 2012


Benedikt Huber <benedikt.huber at gmail.com> writes:

> Hello!
>
> I recently started playing around with Why3 (using coq+Z3), and I'm
> really impressed so far.
>
> However, I believe that the lemma 'permut_eq' (theory map.why) is
> wrong. While playing with the VCs of the quicksort example, I found
> that it is possible to prove that "all maps Z->Z are equal" using this
> lemma (see below). Does this imply the map theory is inconsistent, or
> did I miss something?

I agree with you. I think there are two interpretations of what
"permut_sub" represents, and when they collide you get inconsistency.

Interpretation 1: the sub arrays are permutations, and we don't know
anything about the rest. This is what the inductive definition of
permut_sub does (in the reflexive case).

Interpretation 2: the sub arrays are permutation and are equal
otherwise. This is what permut_eq says. However it cannot be proven from
the definition, and leads to the inconsistency you pointed out.

Interestingly enough, I recently proved the quicksort.mlw from the
examples using only Alt-Ergo and CVC3. I did not use permut_eq, but I'll
have to check it was not used behind my back, as I introduced a very
similar predicate:

  predicate array_eq_out (a1 a2 : array int) (m n : int) =
    array_eq_sub a1 a2 0 m /\ array_eq_sub a1 a2 n (length a2)

Alan



More information about the Why3-club mailing list