Description  Running "framac wp wpprop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like AltErgo and Cvc4. However, another reason is that FramaC's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.
As a result, in the attached mlw file,
"(L_Foo(a,b+c)=true) > (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) > (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
"(L_Foo(a,c+b)=true) > (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the sourcecode. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.
If the goal is changed to "(L_Foo(a,i_2+i_1)=true) > (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and AltErgo proves it in a few milliseconds.
Unless there are good reasons to swap the arguments of "+", they should be kept in their sourcecode order; this way, the user has a chance to control what is given to the provers.
However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.
A possible explanation for the above behavior of FramaC is that, for some
reason, sourcecode variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue #2100).
