[Why3-club] Consistency of map theory
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)
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club