Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Trying out Mtac
(** 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 *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment