Mercurial > cpdt > repo
comparison src/Reflection.v @ 205:f05514cc6c0d
'make doc' works with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 12:15:05 -0500 |
parents | e71904f61e69 |
children | 54e8ecb5ec88 |
comparison
equal
deleted
inserted
replaced
204:cbf2f74a5130 | 205:f05514cc6c0d |
---|---|
116 Theorem even_255 : isEven 255. | 116 Theorem even_255 : isEven 255. |
117 (** [[ | 117 (** [[ |
118 | 118 |
119 prove_even_reflective. | 119 prove_even_reflective. |
120 | 120 |
121 ]] | |
122 | |
121 [[ | 123 [[ |
122 | 124 |
123 User error: No matching clauses for match goal | 125 User error: No matching clauses for match goal |
124 ]] | 126 ]] |
125 | 127 |
126 Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the [match]. | 128 Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the [match]. |
127 | 129 |
128 [[ | 130 [[ |
129 | 131 |
130 exact (partialOut (check_even 255)). | 132 exact (partialOut (check_even 255)). |
133 | |
134 ]] | |
131 | 135 |
132 [[ | 136 [[ |
133 | 137 |
134 Error: The term "partialOut (check_even 255)" has type | 138 Error: The term "partialOut (check_even 255)" has type |
135 "match check_even 255 with | 139 "match check_even 255 with |
631 | 635 |
632 [[ | 636 [[ |
633 Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1 | 637 Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1 |
634 -> z + (8 # 1) * x == 20 # 1 | 638 -> z + (8 # 1) * x == 20 # 1 |
635 -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1. | 639 -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1. |
640 | |
641 ]] | |
642 | |
636 [[ | 643 [[ |
637 | 644 |
638 intros; reflectContext; assumption. | 645 intros; reflectContext; assumption. |
646 | |
647 ]] | |
639 [[ | 648 [[ |
640 Qed. | 649 Qed. |
650 | |
651 ]] | |
641 | 652 |
642 Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==]. | 653 Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==]. |
643 | 654 |
644 %\begin{enumerate}%#<ol># | 655 %\begin{enumerate}%#<ol># |
645 %\item%#<li># Define an inductive type [exp] of expressions over rationals (which inhabit the Coq type [Q]). Include variables (represented as natural numbers), constants, addition, substraction, and multiplication.#</li># | 656 %\item%#<li># Define an inductive type [exp] of expressions over rationals (which inhabit the Coq type [Q]). Include variables (represented as natural numbers), constants, addition, substraction, and multiplication.#</li># |
678 | [ |- ?X == ?Y -> _ ] => | 689 | [ |- ?X == ?Y -> _ ] => |
679 ring_simplify X Y; intro | 690 ring_simplify X Y; intro |
680 end ] | 691 end ] |
681 end. | 692 end. |
682 | 693 |
694 ]] | |
695 | |
683 #</ol>#%\end{enumerate}% | 696 #</ol>#%\end{enumerate}% |
684 #</li># | 697 #</li># |
685 | 698 |
686 #</ol>#%\end{enumerate}% *) | 699 #</ol>#%\end{enumerate}% *) |