Mercurial > cpdt > repo
comparison src/Equality.v @ 488:31258618ef73
Incorporate feedback from Nathan Collins
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Jan 2013 14:38:56 -0500 |
| parents | 5025a401ad9e |
| children | 7d2339cbd39c |
comparison
equal
deleted
inserted
replaced
| 487:8bfb27cf0121 | 488:31258618ef73 |
|---|---|
| 626 match pf in (_ = ls) return (fhlist B ls) with | 626 match pf in (_ = ls) return (fhlist B ls) with |
| 627 | eq_refl => (a0, f) | 627 | eq_refl => (a0, f) |
| 628 end | 628 end |
| 629 ]] | 629 ]] |
| 630 | 630 |
| 631 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood. | 631 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations contain some positions where only variables are allowed. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood. |
| 632 | 632 |
| 633 In this case, it is helpful to generalize over our two proofs as well. *) | 633 In this case, it is helpful to generalize over our two proofs as well. *) |
| 634 | 634 |
| 635 generalize pf pf'. | 635 generalize pf pf'. |
| 636 (** [[ | 636 (** [[ |