[Termtools] [Cime-club] problem with Coccinelle's RPO?

[Frederic Blanqui]

Yes, please, send me your modified rpo.v file. Thank you very much Sorin!

Le 28/06/2010 20:24, sorin stratulat a écrit :
> Hello !
>
> I have met this problem some time ago, while trying to validate Spike proofs.
>
> The problem is fixed by now (together with some other extensions that
> I included in rpo.v). I can send the modified source code, so please
> tell me how to proceed. The original source code has been downloaded
> from
>
> http://a3pat.ensiie.fr/pub/index.en.html
>
> by clicking on the right of the text "Relevant Coccinelle 8.2 version:"
>
> However, I think that the changes can be easily integrated into more
> recent versions of Coccinelle.
>
> Best regards,
>
> Sorin
>
> 2010/6/28 Frederic Blanqui<frederic.blanqui at inria.fr>:
>> 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.
>>
>> _______________________________________________
>> Cime-club mailing list
>> Cime-club at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/cime-club
>>