Mercurial > cpdt > repo
comparison src/Match.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 06 Nov 2009 10:52:43 -0500 |
| parents | ce4cc7fa9b2b |
| children | f05514cc6c0d |
comparison
equal
deleted
inserted
replaced
| 203:71ade09024ac | 204:cbf2f74a5130 |
|---|---|
| 782 | 782 |
| 783 (** Our final [matcher] tactic is now straightforward. First, we [intros] all variables into scope. Then we attempt simple premise simplifications, finishing the proof upon finding [False] and eliminating any existential quantifiers that we find. After that, we search through the conclusion. We remove [True] conjuncts, remove existential quantifiers by introducing unification variables for their bound variables, and search for matching premises to cancel. Finally, when no more progress is made, we see if the goal has become trivial and can be solved by [imp_True]. *) | 783 (** Our final [matcher] tactic is now straightforward. First, we [intros] all variables into scope. Then we attempt simple premise simplifications, finishing the proof upon finding [False] and eliminating any existential quantifiers that we find. After that, we search through the conclusion. We remove [True] conjuncts, remove existential quantifiers by introducing unification variables for their bound variables, and search for matching premises to cancel. Finally, when no more progress is made, we see if the goal has become trivial and can be solved by [imp_True]. *) |
| 784 | 784 |
| 785 Ltac matcher := | 785 Ltac matcher := |
| 786 intros; | 786 intros; |
| 787 repeat search_prem ltac:(apply False_prem || (apply ex_prem; intro)); | 787 repeat search_prem ltac:(simple apply False_prem || (simple apply ex_prem; intro)); |
| 788 repeat search_conc ltac:(apply True_conc || eapply ex_conc | 788 repeat search_conc ltac:(simple apply True_conc || simple eapply ex_conc |
| 789 || search_prem ltac:(apply Match)); | 789 || search_prem ltac:(simple apply Match)); |
| 790 try apply imp_True. | 790 try simple apply imp_True. |
| 791 (* end thide *) | 791 (* end thide *) |
| 792 | 792 |
| 793 (** Our tactic succeeds at proving a simple example. *) | 793 (** Our tactic succeeds at proving a simple example. *) |
| 794 | 794 |
| 795 Theorem t2 : forall P Q : Prop, | 795 Theorem t2 : forall P Q : Prop, |