Trying out Mtac

MtacCancel.v

(** An axiomatization of commutative monoids
 **)
Parameter m : Type.
Parameter star : m -> m -> m.
Local Infix "*" := star.
Parameter one : m.

Axiom star_comm : forall a b : m, a * b = b * a.
Axiom star_assoc : forall a b c : m, (a * b) * c = a * (b * c).
Axiom one_star : forall a : m, one * a = a.

Goal forall a b c : m, a * b * c = c * b * a.
Proof.
  intros.
  rewrite star_assoc. rewrite (star_comm _ a).
  rewrite (star_comm c b). reflexivity.
Qed.


(** Import the Mtac library & notations **)
Require Import Mtac.Mtac.
Import MtacNotations.

(** A simple 'optmizing' version of star. It converts
 ** defintions such as [star x one] into [x]. Note that the
 ** return type is a an Mtac program (M) that returns a monoidal
 ** expression [x] and a proof that [x] is provably equal to [star a b].
 **)
Definition opt_star (a b : m) : M { x : m | x = a * b }.
refine (
  mmatch a as a return M { x : m | x = a * b } with
  | one => ret (@exist _ _ b _ (* first proof *))
  | [? z] z =>
    mmatch b as b return M { x : m | x = z * b } with
    | one => ret (@exist _ _ a _ (* second proof *))
    | _ => ret (@exist _ _ (a * b) _ (* third proof *))
    end
  end).
(** Now we need to complete each of the proofs.
 ** I use 'abstract' to avoid inlining the proofs.
 **)
{ clear; abstract (symmetry; apply one_star). }
{ abstract (symmetry; subst; rewrite star_comm; apply one_star). }
{ abstract (subst; reflexivity). }
Defined.

(** We can run our Mtac program using [Mrun].
 **)
Let x := Mrun (opt_star one one).
Eval compute in proj1_sig x.
(** = one
 **)

(** If we want to see the full result, then we can simply print
 ** the result.
 **)
Print x.
(** x =
 ** exist (fun x : m => x = star one one) one (opt_star_subproof one)
 **      : {x : m | x = star one one}
 **
 ** Note that the proof is embedded directly in the result as the second
 ** part of the pair.
 **)

(** * Performing Cancellation **)
(** I'll start with the 'benchmark'.
 **)
Require Import Coq.Lists.List.
Axiom asM : nat -> m. (** Just a way to construct 'm's **)

(** Build a large 'm' from a list. **)
Fixpoint big (n : nat) : list m :=
  match n with
  | 0 => nil
  | S n => asM n :: big n
  end.

Fixpoint stars (l : list m) : m :=
  match l with
  | nil => one
  | l :: nil => l
  | l :: ls => l * stars ls
  end.

(** This will allow us to set up problems that are reasonably 'difficult'
 ** to solve.
 **)
Definition benchmark (n : nat) : Prop :=
  stars (big n) = stars (rev (big n)).

Ltac bench n :=
  let p := eval compute in (benchmark n) in
  refine p.

Goal ltac:(bench 3).
Abort.

(** I implement cancellation in two steps.
 ** 1/ A procedure [remove] that takes two monoidal expressions
 **    and searches for the first in the second. If it fines the first
 **    in the second, then it returns the rest of the term, otherwise
 **    it fails with 'NotFound' (defined below)
 ** 2/ A procedure [cancel] repeatedly removes each atomic element on
 **    the left-hand-side from the right-hand-side and returns a pair
 **    containing the resulting terms and a proof that proving them
 **    equivalent implies the two input expressions are equivalent.
 **)

(** Declare a new exception. We need to make sure that
 ** the definition is opaque otherwise Mtac will try to unfold it
 ** and it won't look like NotFound
 **)
Definition NotFound : Exception.
  exact exception.
Qed.
Print Mtac.

(** ** Attempt #0: Naively Using Program **)
(** **)
Program Definition remove (x : m)
: forall s, M { s' : m | s = x * s' } :=
  (mfix1 f (s : m) : M { s' : m | s = x * s' } :=
    mmatch s as s return M { s' : m | s = x * s' } with
    | x => ret (@exist _ _ one _)
    | [? l r ] star l r =>
      mtry
        il <- f l ;
        ret (@exist _ _ (il * r) _)
      with _ =>
        ir <- f r ;
        ret (@exist _ _ (l *ir) _)
      end
    | _ => raise NotFound
    end).
Next Obligation.
  clear.
  rewrite star_comm. symmetry. apply one_star.
Qed.
Next Obligation.
  clear.
  simpl. rewrite star_assoc. reflexivity.
Qed.
Next Obligation.
  clear.
  simpl. rewrite <- star_assoc. rewrite (star_comm l x0). rewrite star_assoc.
  reflexivity.
Qed.

Print remove.
(** The term isn't very pretty looking. But let's try it out
 **)
Time Check Mrun (remove (asM 9) (stars (big 10))).
(** The proof is huge (about 73 lines) but it we look at it, we notice that
 ** a major piece of it is the fact that the [remove] code is embedded inside.
 ** Consulting the code, we realize that there are opportunities for
 ** simplification that [Mrun] did not reduce because [Mrun] uses Coq's
 ** [hnf] (head-normal form) reduction strategy. This means that when
 ** we have constructors (or abstract proofs), we need to make sure their
 ** arguments are already reduced.
 **
 ** Performance isn't too bad for this small problem, but if we start
 ** adding more terms, things start to go south, e.g. removing [asM 9] from
 ** [stars (big 16)] takes 3.4 seconds.
 **)
Time Check Mrun (remove (asM 9) (stars (big 16))).

(** ** Attempt #1: Using Refine + Abstract + Explicit Matches **)
(** We can remedy this by doing two things:
 ** 1/ Lift matches so that [Mrun] reduces them by making sure that they return
 **    values of type [M].
 ** 2/ Use [abstract] to hide internal proofs.
 **)
Definition remove_refine (x : m)
: forall (s : m), M { s' : m | s = x * s' }.
refine
  (mfix1 f (s : m) : M { s' : m | s = x * s' } :=
    mmatch s as s return M { s' : m | s = x * s' } with
    | x => ret (@exist _ _ one _)
    | [? l r ] star l r =>
      mtry
        il <- f l ;
        match il with
        | exist _ il1 il2 =>
          ret (@exist _ _ (il1 * r) _)
        end
      with _ =>
        ir <- f r ;
        match ir with
        | exist _ ir1 ir2 =>
          ret (@exist _ _ (l * ir1) _)
        end
      end
    | _ => raise NotFound
    end).
{ clear.
  abstract (rewrite star_comm; symmetry; apply one_star). }
{ clear - il2.
  abstract (subst; rewrite star_assoc; reflexivity). }
{ clear - ir2.
  abstract (subst; rewrite <- star_assoc; rewrite (star_comm l x0);
            rewrite star_assoc; reflexivity). }
Defined.

Print remove_refine.
(** The code still doesn't look beautiful, but we made massive progress in
 ** performance. The same problem that took more than 3 seconds before now
 ** takes 0.073s (a 45x performance improvement)
 **)
Time Check Mrun (remove_refine (asM 9) (stars (big 16))).
(** Inspecting the resulting proof shows that we have completely eliminated
 ** the dangling tactics which were the problem above.
 **)

(** ** Implementing Cancellation **)
(** With what we know, we can implement the full cancellation procedure.
 ** The main thing to note here is that we need to strengthen the specification
 ** witih the universal quantifier [Z] so that we can lift subproblems to
 ** the entire problem.
 **
 ** Note that as above, I'm using explicit matching on pairs to extract
 ** the values rather than using [fst] and [snd].
 **)

Program Definition cancel
: forall (l r : m), M { xy : m * m
                      | forall Z, match xy with
                                  | (x,y) => Z * x = y -> Z * l = r
                                  end} :=
  mfix2 cancel (l : m) (r : m)
  : M { xy : m * m
      | forall Z, match xy with
                  | (x,y) => Z * x = y -> Z * l = r
                  end } :=
    mmatch l as l
      return M { xy : m * m
               | forall Z, match xy with
                           | (x,y) => Z * x = y -> Z * l = r
                           end} with
    | [? a' a''] star a' a'' =>
      res <- cancel a' r ;
      match res with
      | (res11,res12) =>
        res' <- cancel a'' res12 ;
        match res' with
        | (res'11,res'12) =>
          ret (@exist _ _ (res11 * res'11, res'12) _)
        end
      end
    | _ =>
      mtry
        res <- remove_refine l r ;
        ret (@exist _ _ (one, proj1_sig res) _)
      with _ =>
        ret (@exist _ _ (l, r) _)
      end
    end.
Next Obligation.
  clear - H1 H2.
   abstract (
  simpl in *;
  rewrite <- (H2 (Z * a''));
  [ rewrite (star_comm a' a''); rewrite star_assoc; reflexivity
  | clear H2;
    rewrite <- (H1 (Z * m2));
    [ do 2 rewrite star_assoc; rewrite (star_comm a'' m2); reflexivity
    | rewrite star_assoc; reflexivity ] ]).
Defined.
Next Obligation.
  clear cancel.
  abstract (simpl in *;
  subst; rewrite star_comm; rewrite (star_comm _ one); rewrite one_star;
  reflexivity).
Defined.

(** When we print this basic definition of cancel we find that it is not
 ** what we expected.
 **)
Print cancel.
(** In particular, the use of [Program] has added a lot of extra [let]
 ** declarations which, under head-normal-form reduction will simply
 ** get substituted. These are useful for communicating more information
 ** to types but it isn't very pretty for reduction purposes.
 ** The bigger thing to note is the way the proofs were integrated.
 **
 ** Note that [cancel_obligation_1] is applied to 13 arguments!
 ** If we were reducing that term then it would be fine since we [Defined]
 ** the proof, but since it is the argument of a constructor, Mtac is not
 ** going to reduce it.
 **)
About cancel_obligation_1.

(** These two issues (primarily the second one), has a *huge* impact on the
 ** runtime. To see, let's first define a simple theorem to take the
 ** generalized proof that we get out of [cancel] and use it to solve the goal.
 **)
Theorem finish_cancel (a b c d : m)
        (pf : forall Z, Z * c = d -> Z * a = b)
  : c = d -> a = b.
Proof.
  intros. specialize (pf one). subst.
  repeat rewrite one_star in *. auto.
Qed.

(** Now we can write a simple tactic to solve the goal. We'll use this tactic
 ** again so we'll parameterize it by the Mtac tactic to run.
 **)
Ltac solve_it tac :=
  match goal with
  | |- @eq m ?X ?Y =>
    let z := constr:(Mrun (tac X Y)) in
    match z with
    | @exist _ _ _ ?pf =>
      apply (@finish_cancel _ _ _ _ pf) ; reflexivity
    end
  end.

(** Performance for large problems is really bad. Solving a problem of size 5
 ** takes about 1.784 seconds and similarly, proof checking takes equally long.
 **)
Goal ltac:(bench 5).
  Time solve_it cancel. (* 1.784s *)
  (** Showing the proof easily reveals the problem. **)
  Show Proof.
Time Qed. (* 1.58s *)

(** * Cancellation Revised **)
(** We can fix the problem by avoiding the use of [Program] and writing our
 ** program explicitly.
 **)
Definition cancel_refine
: forall (l r : m), M { xy : m * m
                      | forall Z, Z * fst xy = snd xy -> Z * l = r }.
refine (
  mfix2 cancel (l : m) (r : m)
  : M { xy : m * m
      | forall Z, Z * fst xy = snd xy -> Z * l = r } :=
    mmatch l as l
      return M { xy : m * m
               | forall Z, Z * fst xy = snd xy -> Z * l = r }
    with
    | [? a' a''] star a' a'' =>
      res <- cancel a' r ;
      (** NOTE(1): the explicit pattern matching and casting! **)
      match res with
      | exist _ _res1 _res2 =>
        match _res1 as xy
              return (forall Z, Z * fst xy = snd xy -> Z * _ = _) -> _
        with
        | (fst_res1,snd_res1) => fun res2 =>
          res' <- cancel a'' (snd_res1) ;
          match res' with
          | exist _ _res'1 _res'2 =>
            match _res'1 as xy
                  return (forall Z, Z * fst xy = snd xy -> Z * _ = _) -> _
            with
            | (fst_res'1,snd_res'1) => fun res'2 =>
              ret (@exist _ _ (fst_res1 * fst_res'1, snd_res'1) _)
            end _res'2
          end
        end _res2
      end
    | [? x ] x =>
      (** NOTE(2): Here we capture the full term **)
      mtry
        (** NOTE(2): and then we use it here **)
        res <- remove_refine x r ;
        match res with
        | exist _ res1 res2 =>
          ret (@exist _ _ (one, res1) _)
        end
      with _ =>
        ret (@exist _ _ (x, r) _)
      end
    end).
{ clear - res2 res'2.
  abstract(
  subst;
  intros; simpl in *;
  rewrite <- (res2 (star Z a''));
  [ rewrite (star_comm a' a''); rewrite star_assoc; reflexivity
  | rewrite <- (res'2 (star Z fst_res1));
    [ do 2 rewrite star_assoc; f_equal; apply star_comm
    | rewrite star_assoc; assumption ] ]). }
{ clear - res2.
  abstract (subst; simpl; intro;
            rewrite star_comm; rewrite one_star; intros; subst; rewrite star_comm; reflexivity). }
{ clear. abstract (simpl; subst; eauto). }
Defined.

(** NOTE(2) is a bit subtle but it is important due to the way that dependent
 ** pattern matching works. Naively, since we are matching [l] against anything
 ** we could also just use [_] for the pattern and [l] for in place of [x].
 ** However, this is not as nice. In particular, it requires that we later
 ** perform an explicit match on the proof of equality between the value
 ** captured by [_] and [l]. Since the proof is generated by Mtac, we know that
 ** that proof will be [eq_refl], but the match is still necessary to make the
 ** term type check.
 **)

(** Print the proof shows that it is substantially simpler. The extra
 ** [let] declarations have been removed and the subproofs now take
 ** relatively few arguments.
 **)
Print cancel_refine.

(** The performance improvement is huge **)
Goal ltac:(bench 5).
  Time solve_it cancel_refine. (* 0.073s *)
Time Qed. (* 0.011s *)
(** That is a 24x speedup for the search and 143x speedup for checking the
 ** proof.
 **)


(** After all of the optimization, the implemntation scales reasonably well.
 ** Problems that were not even solvable previously now complete in about
 ** 6 seconds.
 **)
Goal ltac:(bench 30).
  Time solve_it cancel_refine. (* 5.797s *)
Time Qed. (* 0.792s *)