Mercurial > cpdt > repo

comparison src/Reflection.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'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}% *)