Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 37:c9ade53b27aa
TVL and constant-folding exercises
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 12 Sep 2008 15:30:59 -0400 |
| parents | 9e46ade5af21 |
| children | 95e24b629ad9 |
comparison
equal
deleted
inserted
replaced
| 36:9e46ade5af21 | 37:c9ade53b27aa |
|---|---|
| 1089 change (pred (S n) = pred (S m)). | 1089 change (pred (S n) = pred (S m)). |
| 1090 rewrite H. | 1090 rewrite H. |
| 1091 reflexivity. | 1091 reflexivity. |
| 1092 Qed. | 1092 Qed. |
| 1093 | 1093 |
| 1094 | |
| 1095 (** * Exercises *) | |
| 1096 | |
| 1097 (** %\begin{enumerate}%#<ol># | |
| 1098 | |
| 1099 %\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe]. [Yes] stands for certain truth, [False] for certain falsehood, and [Maybe] for an unknown situation. Define "not," "and," and "or" for this replacement boolean algebra. Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li># | |
| 1100 | |
| 1101 %\item%#<li># Modify the first example language of Chapter 1 to include variables, where variables are represented with [nat]. Extend the syntax and semantics of expressions to accommodate the change. Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable. Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant. Prove that constant folding preserves the meaning of expressions.#</li># | |
| 1102 | |
| 1103 #</ol>#%\end{enumerate}% *) |