The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I'm trying to write a simple logic in Coq in which, in monadic style, proofs have some associated context, where this context gets carried along through the application of inference rules to construct larger proofs. I'm wondering whether someone out there has done this, and what design patterns in Coq might best be employed. 

To make my goal a little clearer, here's a simple example.

Suppose I have three propositions: P1: Prop, P2: Prop, and P1 /\ P2: Prop. 

A "monadic proof", mp1, of P1, would be a pair (p1, c1), where p1: P1 is an ordinary proof of P1, and where c1 is monadic context associated with this proof.

Similarly a monadic proof mp2 of P2 would be a pair (p2, c2), where p2: P2, and where c2 is context associated with this proof.

Now I want to apply an inference rule (proof constructor) to build a "monadic proof," ma, of P1 /\ P2 from the component (monadic) proofs, m1=(p1,c1) and m2=(p2,c2). This new proof, ma, would be of the form (conj p1 p2, c1 + c2). The first element of this monadic proof object,  conj p1 p2, is an ordinary proof of P1 /\ P2. The new context, c1 + c2 is a combined context object, associated with this proof, built from the smaller context objects, where the combination is effected by the application of the monadic proof constructor. 

The problem of course is that a value of type (Prop * Context) is not of type Prop, and so the usual design patterns for embedding a logic into Coq don't apply.

Ideas? Wisdom?

Thanks,

Kevin Sullivan