Equational Reasoning in Coq, using tactics inside terms!

EquationalReasoning.v

Require Import Coq.Setoids.Setoid.
Require Import Arith.

Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).

Definition times2 : forall n, n + n = 2 * n := fun n =>
  `Begin
    (n + n)       =]$( rewrite (plus_n_O n) at 2; reflexivity )$]
    (n + (n + 0)) =]$( reflexivity                            )$]
    (2 * n)
  `End.

Definition times2' : forall n, n + n = 2 * n := fun n =>
  `Begin
    (n + n)       =]$( apply plus_n_O   )$]
    (n + n + 0)   =[$( apply plus_assoc )$[
    (n + (n + 0)) =]$( reflexivity      )$]
    (2 * n)
  `End.