Mercurial > cpdt > repo

comparison src/Match.v @ 340:23b06f87bd30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More coqdoc bug workarounds
author Adam Chlipala <adam@chlipala.net>
date Thu, 13 Oct 2011 10:24:39 -0400
parents 386b7ad8849b
children 50e1d338728c
comparison
equal deleted inserted replaced
339:aaeba4cfd075 340:23b06f87bd30
1122 1122
1123 (** printing exists $\exists$ *) 1123 (** printing exists $\exists$ *)
1124 1124
1125 (** Recall that [exists] formulas are desugared to uses of the [ex] inductive family. In particular, a pattern like the following can be used to extract the domain of an [exists] quantifier into variable [T]: 1125 (** Recall that [exists] formulas are desugared to uses of the [ex] inductive family. In particular, a pattern like the following can be used to extract the domain of an [exists] quantifier into variable [T]:
1126 1126
1127 [| [ |- ex ( A := ?T) _ ] => ...] 1127 [| ]#[#%[%[ |- ex (][A := ?][T) _ ]#]#%]%[ => ...]
1128 1128
1129 The [equate] tactic used as an example in this chapter will probably be useful, to unify two terms, for instance if the first is a unification variable whose value you want to set. 1129 The [equate] tactic used as an example in this chapter will probably be useful, to unify two terms, for instance if the first is a unification variable whose value you want to set.
1130 [[ 1130 [[
1131 Ltac equate E1 E2 := let H := fresh in 1131 Ltac equate E1 E2 := let H := fresh in
1132 assert (H : E1 = E2) by reflexivity; clear H. 1132 assert (H : E1 = E2) by reflexivity; clear H.
1133 ]] 1133 ]]
1134 1134
1135 Finally, there are some minor complications surrounding overloading of the [*] operator for both numeric multiplication and Cartesian product for sets (i.e., pair types). To ensure that an Ltac pattern is using the type version, write it like this: 1135 Finally, there are some minor complications surrounding overloading of the [*] operator for both numeric multiplication and Cartesian product for sets (i.e., pair types). To ensure that an Ltac pattern is using the type version, write it like this:
1136 1136
1137 [| (?T1 * ?T2)%type => ...]#</li># 1137 [| (?T1 * ?T2)%][type => ...]#</li>#
1138 1138
1139 %\item%#<li># An exercise in the last chapter dealt with automating proofs about rings using [eauto], where we must prove some odd-looking theorems to push proof search in a direction where unification does all the work. Algebraic proofs consist mostly of rewriting in equations, so we might hope that the [autorewrite] tactic would yield more natural automated proofs. Indeed, consider this example within the same formulation of ring theory that we dealt with last chapter, where each of the three axioms has been added to the rewrite hint database [cpdt] using [Hint Rewrite]: 1139 %\item%#<li># An exercise in the last chapter dealt with automating proofs about rings using [eauto], where we must prove some odd-looking theorems to push proof search in a direction where unification does all the work. Algebraic proofs consist mostly of rewriting in equations, so we might hope that the [autorewrite] tactic would yield more natural automated proofs. Indeed, consider this example within the same formulation of ring theory that we dealt with last chapter, where each of the three axioms has been added to the rewrite hint database [cpdt] using [Hint Rewrite]:
1140 [[ 1140 [[
1141 Theorem test1 : forall a b, a * b * i b = a. 1141 Theorem test1 : forall a b, a * b * i b = a.
1142 intros; autorewrite with cpdt; reflexivity. 1142 intros; autorewrite with cpdt; reflexivity.
1147 [[ 1147 [[
1148 Theorem test2 : forall a, a * e * i a * i e = e. 1148 Theorem test2 : forall a, a * e * i a * i e = e.
1149 intros; autorewrite with cpdt. 1149 intros; autorewrite with cpdt.
1150 ]] 1150 ]]
1151 1151
1152 The goal is merely reduced to [a * (i a * i e) = e], which of course [reflexivity] cannot prove. The essential problem is that [autorewrite] does not do backtracking search. Instead, it follows a %``%#"#greedy#"#%''% approach, at each stage choosing a rewrite to perform and then never allowing that rewrite to be undone. An early mistake can doom the whole process. 1152 The goal is merely reduced to [a * (][i a * i e) = e], which of course [reflexivity] cannot prove. The essential problem is that [autorewrite] does not do backtracking search. Instead, it follows a %``%#"#greedy#"#%''% approach, at each stage choosing a rewrite to perform and then never allowing that rewrite to be undone. An early mistake can doom the whole process.
1153 1153
1154 The task in this problem is to use Ltac to implement a backtracking version of [autorewrite] that works much like [eauto], in that its inputs are a database of hint lemmas and a bound on search depth. Here our search trees will have uses of [rewrite] at their nodes, rather than uses of [eapply] as in the case of [eauto], and proofs must be finished by [reflexivity]. 1154 The task in this problem is to use Ltac to implement a backtracking version of [autorewrite] that works much like [eauto], in that its inputs are a database of hint lemmas and a bound on search depth. Here our search trees will have uses of [rewrite] at their nodes, rather than uses of [eapply] as in the case of [eauto], and proofs must be finished by [reflexivity].
1155 1155
1156 An invocation to the tactic to prove [test2] might look like this: 1156 An invocation to the tactic to prove [test2] might look like this:
1157 [[ 1157 [[