Mercurial > cpdt > repo
comparison src/Exercises.v @ 426:5f25705a10ea
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 25 Jul 2012 18:10:26 -0400 |
| parents | 5986e9fd40b5 |
| children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
| 425:6ed5ee4845e4 | 426:5f25705a10ea |
|---|---|
| 199 %\item%#<li># Define a function [lift : forall ts t t', exp ts t -> exp (t' :: ts) t], which handles simpler top-level lifts. This should be an easy one-liner based on [lift'].#</li># | 199 %\item%#<li># Define a function [lift : forall ts t t', exp ts t -> exp (t' :: ts) t], which handles simpler top-level lifts. This should be an easy one-liner based on [lift'].#</li># |
| 200 %\item%#<li># Define a recursive function [substVar : forall ts1 ts2 t t', member t (ts1 ++ t' :: ts2) -> (t' = t) + member t (ts1 ++ ts2)]. This function is the workhorse behind substitution applied to a variable. It returns [inl] to indicate that the variable we pass to it is the variable that we are substituting for, and it returns [inr] to indicate that the variable we are examining is _not_ the one we are substituting for. In the first case, we get a proof that the necessary typing relationship holds, and, in the second case, we get the original variable modified to reflect the removal of the substitutee from the typing context.#</li># | 200 %\item%#<li># Define a recursive function [substVar : forall ts1 ts2 t t', member t (ts1 ++ t' :: ts2) -> (t' = t) + member t (ts1 ++ ts2)]. This function is the workhorse behind substitution applied to a variable. It returns [inl] to indicate that the variable we pass to it is the variable that we are substituting for, and it returns [inr] to indicate that the variable we are examining is _not_ the one we are substituting for. In the first case, we get a proof that the necessary typing relationship holds, and, in the second case, we get the original variable modified to reflect the removal of the substitutee from the typing context.#</li># |
| 201 %\item%#<li># Define a recursive function [subst' : forall ts t (e : exp ts t) ts1 t' ts2, ts = ts1 ++ t' :: ts2 -> exp (ts1 ++ ts2) t' -> exp (ts1 ++ ts2) t]. This is the workhorse of substitution in expressions, employing the same proof-passing trick as for [lift']. You will probably want to use [lift] somewhere in the definition of [subst'].#</li># | 201 %\item%#<li># Define a recursive function [subst' : forall ts t (e : exp ts t) ts1 t' ts2, ts = ts1 ++ t' :: ts2 -> exp (ts1 ++ ts2) t' -> exp (ts1 ++ ts2) t]. This is the workhorse of substitution in expressions, employing the same proof-passing trick as for [lift']. You will probably want to use [lift] somewhere in the definition of [subst'].#</li># |
| 202 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li># | 202 %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li># |
| 203 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li># | 203 %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li># |
| 204 %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern. If you have an equality proof that you want to replace with [refl_equal] somehow, run [generalize] on that proof variable. Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version. To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side. You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it. [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes. Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li># | 204 %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern. If you have an equality proof that you want to replace with [eq_refl] somehow, run [generalize] on that proof variable. Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version. To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side. You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it. [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes. Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li># |
| 205 %\item%#<li># The [ext_eq] axiom from the end of this chapter is available in the Coq standard library as [functional_extensionality] in module [FunctionalExtensionality], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li># | 205 %\item%#<li># The [ext_eq] axiom from the end of this chapter is available in the Coq standard library as [functional_extensionality] in module [FunctionalExtensionality], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li># |
| 206 %\item%#<li># The [change] tactic should come in handy in the proofs about [lift] and [subst], where you want to introduce %``%#"#extraneous#"#%''% list concatenations with [nil] to match the forms of earlier theorems.#</li># | 206 %\item%#<li># The [change] tactic should come in handy in the proofs about [lift] and [subst], where you want to introduce %``%#"#extraneous#"#%''% list concatenations with [nil] to match the forms of earlier theorems.#</li># |
| 207 %\item%#<li># Be careful about [destruct]ing a term %``%#"#too early.#"#%''% You can use [generalize] on proof terms to bring into the proof context any important propositions about the term. Then, when you [destruct] the term, it is updated in the extra propositions, too. The [case_eq] tactic is another alternative to this approach, based on saving an equality between the original term and its new form.#</li># | 207 %\item%#<li># Be careful about [destruct]ing a term %``%#"#too early.#"#%''% You can use [generalize] on proof terms to bring into the proof context any important propositions about the term. Then, when you [destruct] the term, it is updated in the extra propositions, too. The [case_eq] tactic is another alternative to this approach, based on saving an equality between the original term and its new form.#</li># |
| 208 #</ol>#%\end{enumerate}% | 208 #</ol>#%\end{enumerate}% |
| 209 #</li># | 209 #</li># |