[Termtools] problem with Coccinelle's RPO?

[Frederic Blanqui]

Hello!

By looking at some CPF file of last year competition, I discovered that 
there is perhaps some problem with Coccinelle's formalization of RPO. I 
did no statistics to see how many CPF files would have been accepted by 
CiME3 or Rainbow (which uses Coccinelle's formalization of RPO) if there 
was not this problem.

It seems that Coccinelle's RPO equivalence is not strong enough to 
handle some example, especially after arguments filtering. Indeed, 
Coccinelle's equivalence is as follows:

     Inductive equiv : term -> term -> Prop :=
     | Eq : forall t, equiv t t
     | Eq_lex :
       forall f l1 l2, status P f = Lex -> equiv_list_lex l1 l2 ->
         equiv (Term f  l1) (Term f l2)
     | Eq_mul :
       forall f l1 l2,  status P f = Mul -> permut0 equiv l1 l2 ->
         equiv (Term f l1) (Term f l2)

You can see that this is the same symbol f that is used in the cases 
Eq_lex and Eq_mul. This means that two constants a and b with the same 
precedence are not considered as equal. But this possibility is used in 
some CPF files.

It means that, unless Coccinelle's formalization of RPO is fixed, 
provers should avoid this kind of proof if they want them to be checked 
by CiME3 or Rainbow.

Is this problem already fixed or is there any plan to fix it before next 
competition?

Frederic.