### changeset 141:ce4cc7fa9b2b

Templatize Match
author Adam Chlipala Mon, 27 Oct 2008 10:31:57 -0400 8cce3247496b 6a00d49e85fb src/Match.v 1 files changed, 59 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/Match.v	Mon Oct 27 10:09:10 2008 -0400
+++ b/src/Match.v	Mon Oct 27 10:31:57 2008 -0400
@@ -40,6 +40,7 @@
All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern].  A few examples should do best to explain how [Hint Extern] works. *)

Theorem bool_neq : true <> false.
+(* begin thide *)
auto.
(** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
Abort.
@@ -51,6 +52,7 @@
Theorem bool_neq : true <> false.
auto.
Qed.
+(* end thide *)

(** Our hint says: "whenever the conclusion matches the pattern [_ <> _], try applying [congruence]."  The [1] is a cost for this rule.  During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints.

@@ -63,6 +65,7 @@
Hypothesis both : forall x, P x /\ Q x.

Theorem forall_and : forall z, P z.
+(* begin thide *)
crush.
(** [crush] makes no progress beyond what [intros] would have accomplished.  [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal.  However, we can teach [auto] to handle this kind of goal. *)

@@ -73,6 +76,7 @@

auto.
Qed.
+(* end thide *)

(** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic.  [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *)
End forall_and.
@@ -163,16 +167,22 @@
Variable P : A -> Prop.
Variable g : A -> A.
Hypothesis f_g : forall x, P x -> f x = g x.
+(* begin thide *)
Hint Rewrite f_g using assumption : my_db.
+(* end thide *)

Lemma f_f_f' : forall x, f (f (f x)) = f x.
+(* begin thide *)
intros; autorewrite with my_db; reflexivity.
Qed.
+(* end thide *)

(** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)

Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
+(* begin thide *)
intros; autorewrite with my_db; reflexivity.
+(* end thide *)
Qed.
End garden_path.

@@ -180,7 +190,9 @@

Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
-> f x = f (f (f y)).
+(* begin thide *)
intros; autorewrite with my_db in *; assumption.
+(* end thide *)
Qed.

End autorewrite.
@@ -192,10 +204,12 @@

One common use for [match] tactics is identification of subjects for case analysis, as we see in this tactic definition. *)

+(* begin thide *)
Ltac find_if :=
match goal with
| [ |- if ?X then _ else _ ] => destruct X
end.
+(* end thide *)

(** The tactic checks if the conclusion is an [if], [destruct]ing the test expression if so.  Certain classes of theorem are trivial to prove automatically with such a tactic. *)

@@ -207,17 +221,21 @@
else if c
then True
else True.
+(* begin thide *)
intros; repeat find_if; constructor.
Qed.
+(* end thide *)

(** The [repeat] that we use here is called a %\textit{%#<i>#tactical#</i>#%}%, or tactic combinator.  The behavior of [repeat t] is to loop through running [t], running [t] on all generated subgoals, running [t] on %\textit{%#<i>#their#</i>#%}% generated subgoals, and so on.  When [t] fails at any point in this search tree, that particular subgoal is left to be handled by later tactics.  Thus, it is important never to use [repeat] with a tactic that always succeeds.

Another very useful Ltac building block is %\textit{%#<i>#context patterns#</i>#%}%. *)

+(* begin thide *)
Ltac find_if_inside :=
match goal with
| [ |- context[if ?X then _ else _] ] => destruct X
end.
+(* end thide *)

(** The behavior of this tactic is to find any subterm of the conclusion that is an [if] and then [destruct] the test expression.  This version subsumes [find_if]. *)

@@ -229,18 +247,23 @@
else if c
then True
else True.
+(* begin thide *)
intros; repeat find_if_inside; constructor.
Qed.
+(* end thide *)

(** We can also use [find_if_inside] to prove goals that [find_if] does not simplify sufficiently. *)

-Theorem duh2 : forall (a b : bool),
+Theorem hmm2 : forall (a b : bool),
(if a then 42 else 42) = (if b then 42 else 42).
+(* begin thide *)
intros; repeat find_if_inside; reflexivity.
Qed.
+(* end thide *)

(** Many decision procedures can be coded in Ltac via "[repeat match] loops."  For instance, we can implement a subset of the functionality of [tauto]. *)

+(* begin thide *)
Ltac my_tauto :=
repeat match goal with
| [ H : ?P |- ?P ] => exact H
@@ -257,6 +280,7 @@
let H := fresh "H" in
generalize (H1 H2); clear H1; intro H
end.
+(* end thide *)

(** Since [match] patterns can share unification variables between hypothesis and conclusion patterns, it is easy to figure out when the conclusion matches a hypothesis.  The [exact] tactic solves a goal completely when given a proof term of the proper type.

@@ -268,8 +292,10 @@
Variables P Q R : Prop.

Theorem propositional : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q.
+(* begin thide *)
my_tauto.
Qed.
+(* end thide *)
End propositional.

(** It was relatively easy to implement modus ponens, because we do not lose information by clearing every implication that we use.  If we want to implement a similarly-complete procedure for quantifier instantiation, we need a way to ensure that a particular proposition is not already included among our hypotheses.  To do that effectively, we first need to learn a bit more about the semantics of [match].
@@ -285,7 +311,9 @@
| [ |- _ ] => intro
| [ |- True ] => constructor
end.
+(* begin thide *)
Qed.
+(* end thide *)

(** The first case matches trivially, but its body tactic fails, since the conclusion does not begin with a quantifier or implication.  In a similar ML match, that would mean that the whole pattern-match fails.  In Coq, we backtrack and try the next pattern, which also matches.  Its body tactic succeeds, so the overall tactic succeeds as well.

@@ -304,15 +332,18 @@

By applying [pose], a convenient debugging tool for "leaking information out of [match]es," we see that this [match] first tries binding [H] to [H1], which cannot be used to prove [Q].  Nonetheless, the following variation on the tactic succeeds at proving the goal: *)

+(* begin thide *)
match goal with
| [ H : _ |- _ ] => exact H
end.
Qed.
+(* end thide *)

(** The tactic first unifies [H] with [H1], as before, but [exact H] fails in that case, so the tactic engine searches for more possible values of [H].  Eventually, it arrives at the correct value, so that [exact H] and the overall tactic succeed. *)

(** Now we are equipped to implement a tactic for checking that a proposition is not among our hypotheses: *)

+(* begin thide *)
Ltac notHyp P :=
match goal with
| [ _ : P |- _ ] => fail 1
@@ -322,6 +353,7 @@
| _ => idtac
end
end.
+(* end thide *)

(** We use the equality checking that is built into pattern-matching to see if there is a hypothesis that matches the proposition exactly.  If so, we use the [fail] tactic.  Without arguments, [fail] signals normal tactic failure, as you might expect.  When [fail] is passed an argument [n], [n] is used to count outwards through the enclosing cases of backtracking search.  In this case, [fail 1] says "fail not just in this pattern-matching branch, but for the whole [match]."  The second case will never be tried when the [fail 1] is reached.

@@ -331,14 +363,17 @@

With the non-presence check implemented, it is easy to build a tactic that takes as input a proof term and adds its conclusion as a new hypothesis, only if that conclusion is not already present, failing otherwise. *)

+(* begin thide *)
Ltac extend pf :=
let t := type of pf in
notHyp t; generalize pf; intro.
+(* end thide *)

(** We see the useful [type of] operator of Ltac.  This operator could not be implemented in Gallina, but it is easy to support in Ltac.  We end up with [t] bound to the type of [pf].  We check that [t] is not already present.  If so, we use a [generalize]/[intro] combo to add a new hypothesis proved by [pf].

With these tactics defined, we can write a tactic [completer] for adding to the context all consequences of a set of simple first-order formulas. *)

+(* begin thide *)
Ltac completer :=
repeat match goal with
| [ |- _ /\ _ ] => constructor
@@ -350,6 +385,7 @@
| [ H : forall x, ?P x -> _, H' : ?P ?X |- _ ] =>
extend (H X H')
end.
+(* end thide *)

(** We use the same kind of conjunction and implication handling as previously.  Note that, since [->] is the special non-dependent case of [forall], the fourth rule handles [intro] for implications, too.

@@ -365,6 +401,7 @@
Hypothesis H2 : forall x, R x -> S x.

Theorem fo : forall x, P x -> S x.
+(* begin thide *)
completer.
(** [[

@@ -379,10 +416,12 @@

assumption.
Qed.
+(* end thide *)
End firstorder.

(** We narrowly avoided a subtle pitfall in our definition of [completer].  Let us try another definition that even seems preferable to the original, to the untrained eye. *)

+(* begin thide *)
Ltac completer' :=
repeat match goal with
| [ |- _ /\ _ ] => constructor
@@ -394,6 +433,7 @@
| [ H : forall x, ?P x -> _, H' : ?P ?X |- _ ] =>
extend (H X H')
end.
+(* end thide *)

(** The only difference is in the modus ponens rule, where we have replaced an unused unification variable [?Q] with a wildcard.  Let us try our example again with this version: *)

@@ -405,12 +445,14 @@
Hypothesis H2 : forall x, R x -> S x.

Theorem fo' : forall x, P x -> S x.
+(* begin thide *)
(** [[

completer'.

Coq loops forever at this point.  What went wrong? *)
Abort.
+(* end thide *)
End firstorder'.

(** A few examples should illustrate the issue.  Here we see a [match]-based proof that works fine: *)
@@ -419,10 +461,13 @@
match goal with
| [ |- forall x, _ ] => trivial
end.
+(* begin thide *)
Qed.
+(* end thide *)

(** This one fails. *)

+(* begin thide *)
Theorem t1' : forall x : nat, x = x.
(** [[

@@ -434,6 +479,7 @@
User error: No matching clauses for match goal
]] *)
Abort.
+(* end thide *)

(** The problem is that unification variables may not contain locally-bound variables.  In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x].  By using a wildcard in the earlier version, we avoided this restriction.

@@ -444,6 +490,8 @@

(** * Functional Programming in Ltac *)

+(* EX: Write a list length function in Ltac. *)
+
(** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor.  However, there are a few syntactic conventions involved in getting programs to be accepted.  The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs.

To illustrate, let us try to write a simple list length function.  We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac].
@@ -474,6 +522,7 @@

The problem is that Ltac treats the expression [S (length ls')] as an invocation of a tactic [S] with argument [length ls'].  We need to use a special annotation to "escape into" the Gallina parsing nonterminal. *)

+(* begin thide *)
Ltac length ls :=
match ls with
| nil => O
@@ -516,9 +565,13 @@
False
]] *)
Abort.
+(* end thide *)
+
+(* EX: Write a list map function in Ltac. *)

(** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *)

+(* begin thide *)
Ltac map T f :=
let rec map' ls :=
match ls with
@@ -544,6 +597,7 @@
False
]] *)
Abort.
+(* end thide *)

(** * Recursive Proof Search *)
@@ -552,6 +606,7 @@

We can consider the maximum "dependency chain" length for a first-order proof.  We define the chain length for a hypothesis to be 0, and the chain length for an instantiation of a quantified fact to be one greater than the length for that fact.  The tactic [inster n] is meant to try all possible proofs with chain length at most [n]. *)

+(* begin thide *)
Ltac inster n :=
intuition;
match n with
@@ -560,6 +615,7 @@
| [ H : forall x : ?T, _, x : ?T |- _ ] => generalize (H x); inster n'
end
end.
+(* end thide *)

(** [inster] begins by applying propositional simplification.  Next, it checks if any chain length remains.  If so, it tries all possible ways of instantiating quantified hypotheses with properly-typed local variables.  It is critical to realize that, if the recursive call [inster n'] fails, then the [match goal] just seeks out another way of unifying its pattern against proof state.  Thus, this small amount of code provides an elegant demonstration of how backtracking [match] enables exhaustive search.

@@ -649,6 +705,7 @@

(** The first order of business in crafting our [matcher] tactic will be auxiliary support for searching through formula trees.  The [search_prem] tactic implements running its tactic argument [tac] on every subformula of an [imp] premise.  As it traverses a tree, [search_prem] applies some of the above lemmas to rewrite the goal to bring different subformulas to the head of the goal.  That is, for every subformula [P] of the implication premise, we want [P] to "have a turn," where the premise is rearranged into the form [P /\ Q] for some [Q].  The tactic [tac] should expect to see a goal in this form and focus its attention on the first conjunct of the premise. *)

+(* begin thide *)
Ltac search_prem tac :=
let rec search P :=
tac
@@ -731,6 +788,7 @@
repeat search_conc ltac:(apply True_conc || eapply ex_conc
|| search_prem ltac:(apply Match));
try apply imp_True.
+(* end thide *)

(** Our tactic succeeds at proving a simple example. *)

@@ -787,5 +845,3 @@
: forall (P : nat -> Prop) (Q : Prop),
(exists x : nat, P x /\ Q) --> Q /\ (exists x : nat, P x)
]] *)
-
-