The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

If you interpret do-notation as a query notation (usually specialized to the 
set monad, etc), then I think what you're calling a 'monad proof context' 
corresponds to the notion of a 'tableau' in database theory.  Typically, 
tableaux are written in a very stylized inscrutable notation, but you might 
try to reference below (e.g. page 9), which I'd be happy to chat about 
offline.  For my thesis I'm interested in deep analysis of tableau as a way 
to optimize certain kinds of do-blocks, but I'm not aware of any other work 
in a mechanized setting.

@INPROCEEDINGS{Popa99anequational,
    author = {Lucian Popa and Val Tannen},
    title = {An Equational Chase for Path-Conjunctive Queries, Constraints, 
and Views},
    booktitle = {In ICDT},
    year = {1999},
    pages = {39--57}
}

On Sep 7, 2012, at 2:26 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:

> Any references on the autogeneration of monad proof context that I
> (presumably re-)discovered?  Here's a simplified example of how it
> works:
> 
> Section augmented_Reader.
> 
> Variable S : Type.
> 
> Definition Reader (X : Type) : Type := S -> X.
> 
> Definition Reader' (X : Type) (P : S -> Prop) : Type :=
>  forall s:S, P s -> X.
> 
> Definition Reader'_bind {X P} (x : Reader X)
>  {Y} (f : forall x0:X, Reader' Y (fun s => P s /\ x s = x0)) :
> Reader' Y P :=
> fun s H => f (x s) s (conj H eq_refl).
> 
> Definition augment_Reader {X P} (x : Reader X) : Reader' X P :=
>  fun s _ => x s.
> 
> Definition unaugment_Reader {X} (x : Reader' X (fun _ => True)) :
>  Reader X :=
> fun s => x s I.
> 
> Notation "'do' x0 <- x ; y" :=
>  (Reader'_bind x (fun x0 => y))
>  (right associativity, x0 ident, at level 70).
> Notation "'return_' x" :=
>  (fun _ _ => x) (at level 0).
> 
> Section augmented_Reader_example.
> 
> Variables X Y : Type.
> Variable x : Reader X.
> Variable y : Reader Y.
> 
> Variable R : X -> Y -> Prop.
> Variable Z : Type.
> Variable f : forall x y, R x y -> Z.
> 
> Hypothesis Rxy : forall s:S, R (x s) (y s).
> 
> Program Definition fxy : Reader Z :=
>  unaugment_Reader (
>  do x0 <- x;
>  do y0 <- y;
>  return_ (f x0 y0 _)).
> Next Obligation.
> intros; rename H into s.
> destruct H0 as [[? ?] ?]; subst.
> apply Rxy.
> Qed.
> 
> End augmented_Reader_example.
> 
> End augmented_Reader.
> -- 
> Daniel Schepler