The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Your question is somewhat underconstrained because you don't talk about which kinds of programs you want to prove equivalent.

If you want to view your program in a functional light, then yes, Coq can be used to reason about term equivalence: but the specifics will be very oriented toward the domain you're targeting.  There's certainly not a universal decision procedure for program equivalence, since in general function equivalence is undecidable (Rice's theorem).

Perhaps if you give a bit more information about what types of programs you want to prove equal we could offer some advice.  For example, if your programs mention equality, uniterpreted functions, and linear arithmetic, you could do it using congruence and omega.

So your question doesn't really apply to Coq, it mostly applies to program equivalence in general: if you have a decidable approximation to equivalence in mind you can definitely implement it in Coq.

Kris

On Wed, Aug 14, 2013 at 9:59 AM, <manjeetdahiya AT gmail.com> wrote:

Hello,

I want to know if coq can be used to prove equivalence of two different
programs? Please give me some pointers if it is doable.

Thanks!