Small library for creating record updaters in Coq

RecordUpdater.v

Definition Reader E T := E -> T.

Definition get {E} : Reader E E := fun e => e.

Definition pure {E T} (x:T) : Reader E T := fun _ => x.

Definition ap {E A B} (f: Reader E (A -> B)) : Reader E A -> Reader E B :=
  fun x => fun e => f e (x e).

Infix "<*>" := (ap) (at level 11, left associativity).

Definition bind {E T T'} (x: Reader E T) (f: T -> Reader E T') : Reader E T' :=
  fun e => f (x e) e.

Notation "f =<< x" := (bind x f) (at level 0).

Ltac prove_updater_ok :=
  match goal with
  | |- forall x, _ = _ =>
    solve [ destruct x; cbv; f_equal ]
  end || fail "updater appears to change record".

Ltac updater t proj :=
  let set :=
      (match eval pattern proj in t with
       | ?updater ?getter => constr:(fun x => updater (pure x))
       end) in
  let set := (eval cbv [pure ap] in set) in
  let updater_ok := constr:(forall x, set =<< proj x = get x) in
  let _ := constr:(ltac:(prove_updater_ok) : updater_ok) in
  exact set.

Tactic Notation "_updater" constr(t) constr(proj) := updater t proj.

Notation mkUpdater x proj := ltac:(_updater x proj).

Module Example.

  Record X := mkX { A : nat;
                    B: nat;
                    C: unit; }.

  Notation etaX := (pure mkX <*> A <*> B <*> C).

  (* oops, mixed up A and B *)
  Fail Definition setA := mkUpdater (pure mkX <*> B <*> A <*> C) A.
  Definition setA := mkUpdater etaX A.
  Definition setB := mkUpdater etaX B.
  Definition setC := mkUpdater etaX C.

  Print setA.

End Example.