# [Why3-club] Consistency of map theory

Santiago Zanella szanella at gmail.com
Thu Nov 22 15:15:50 CET 2012

I agree, this is the real reason for the inconsistency, i.e. that
permut_eq does not follow from the inductive definition of permut_sub.
Please disregard my hasty previous message.
On Thu, Nov 22, 2012 at 1:48 PM, Alan Schmitt <
alan.schmitt at polytechnique.org> wrote:

> 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
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20121122/c3c54d07/attachment.html>