Tactics for Reasoning modulo AC in Coq

Details Tactics for Reasoning modulo AC in Coq Tactics for Reasoning modulo AC in Coq

2011-06-22

arxiv.org/abs/1106.4448v2

Computer Science

Mathematical Software

16p

Scientific paper

We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC; second, an OCaml plug-in for pattern matching modulo AC. We handle associative only operations, neutral elements, uninterpreted function symbols, and user-defined equivalence relations. By relying on type-classes for the reification phase, we can infer these properties automatically, so that end-users do not need to specify which operation is A or AC, or which constant is a neutral element.

Affiliated with

Also associated with

No associations

Rating

Tactics for Reasoning modulo AC in Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Tactics for Reasoning modulo AC in Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Tactics for Reasoning modulo AC in Coq will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-206723