The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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