Redux fails to find triggers for some pure autolemma

[elKei24]

Hi Bart,

there is an internal error "Redux could not find suitable triggers for axiom ..." with some pure autolemmas, for example the following ones:

lemma_auto void list_distinct_indices<t>(list<t> xs, t y, t z);
    requires y != z && mem(y, xs) == true;
    ensures index_of(y, xs) != index_of(z, xs);

lemma_auto void lists_equal<t>(list<t> list1, list<t> list2);
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == (list1 == list2);

I tried to provide a trigger myself like lemma_auto(index_of(y, xs) != index_of(z, xs)), but this only causes an other error: "Redux supports only symbol applications at the top level of axiom triggers.".

Best regards,
Elias

[btj]

Yes. Currently, Redux does not support special operators such as ==, !=, <, <=, >, >=, +, - in axiom triggers.

I notice that Z3 does support it: the following verifies with vfide -prover z3v4.5:

/*@

lemma_auto void list_distinct_indices<t>(list<t> xs, t y, t z);
    requires y != z && mem(y, xs) == true;
    ensures index_of(y, xs) != index_of(z, xs);

lemma_auto void lists_equal<t>(list<t> list1, list<t> list2);
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == (list1 == list2);

lemma void list_distinct_indices_test<t>(list<t> xs, t y, t z)
    requires y != z && mem(y, xs) == true;
    ensures index_of(y, xs) != index_of(z, xs);
{}

lemma void lists_equal_test<t>(list<t> list1, list<t> list2)
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == (list1 == list2);
{}

@*/

A workaround in Redux is to introduce a pure function that wraps the special operator. This verifies:

/*@

fixpoint bool eq<t>(t x, t y) { return x == y; }

lemma_auto void list_distinct_indices<t>(list<t> xs, t y, t z);
    requires y != z && mem(y, xs) == true;
    ensures !eq(index_of(y, xs), index_of(z, xs));

lemma_auto void lists_equal<t>(list<t> list1, list<t> list2);
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == eq(list1, list2);

lemma void test1<t>(list<t> xs, t y, t z)
    requires y != z && mem(y, xs) == true;
    ensures !eq(index_of(y, xs), index_of(z, xs));
{}

lemma void test2<t>(list<t> list1, list<t> list2)
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == eq(list1, list2);
{}

@*/

[elKei24]

Thank you for the two solutions. Unfortunately, Z3 won't halt with my current project, but that might have a different reason. The workaround you suggested works great.

However, I noticed that maintaining the order of the two lemmas is important, because the following causes an other error:

fixpoint bool eq<t>(t x, t y) {return x == y; }

lemma_auto void lists_equal<t>(list<t> list1, list<t> list2);
  requires true;
  ensures (head(list1) == head(list2) && tail(list1) == tail(list2) && length(list1) == length(list2)) == eq(list1, list2);

lemma_auto void list_index_nonneg<t>(list<t> xs, t y);
    requires true;
    ensures index_of(y, xs) >= 0;

lemma void list_distinct_indices<t>(list<t> xs, t y, t z)
    requires y != z && mem(y, xs) == true;
    ensures !eq(index_of(y, xs), index_of(z, xs));
{
    switch (xs) {
      case nil:
      case cons(head, tail):
        if (head != y) list_distinct_indices(tail, y, z);
    }
}

The log says exception File "redux.ml", line 377, characters 73-79: Assertion failed. It might be related with the type confusions mentioned in #34 and #68, because the line before says Entering Redux.assume_core(true ==> 0 <= length([2550=2551]index_of([2061=2062]z, [2074=2075]cons([2069=2059]head0, [2072=2073]tail0)))), so I guess Redux disregarded that list_equal is only applicable to lists and thus considered it to be a candidate for proving the postcondition of list_distinct_indices?

Using specialized eqs for every type instead of a single general one fixes the problem.

[btj]

Indeed. As it happens, I've been working on #125 the last few days, and I think I'm quite close to finishing it, so this should be fixed soon.