The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Kevin --

I actually worked on something that I think is very related to this in my thesis on reflective proof automation. It sounds like you want to do a shallow encoding (my work does a deep encoding to use computational reflection), but most of the ideas should be similar. The main abstraction that I used was applicative functors from which I could derive pretty much everything that I needed. Applying this to your problem, you would define your monad as something like:

Definition Pf (ctx : Context) (p : Prop) : Type :=

  ctx -> p.

Things can obivously get a bit more complex than this, but I roughly feel like this is what you want. You can wrap this in a dependent pair if you want but I think that you might need to know what the context is in order to apply rules, e.g. the assumption rule.

I hope this helps. I'd be happy to discuss further, this is an interesting question that I have thought a fair bit about.

The code for my thesis is available here: https://github.com/gmalecha/mirror-core

My thesis itself is here:  http://gmalecha.github.io/publications/ (the thesis is the first paper). The second paper is a short (2-page) summary of the logic embedding that I did.

Another thing to possibly look at is Jesper Bengston's Charge! library.

On Fri, Apr 17, 2015 at 8:45 AM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/