comparison src/InductiveTypes.v @ 39:fd18331e5c0b

Publishing to the web
author Adam Chlipala <adamc@hcoop.net>
date Fri, 12 Sep 2008 17:18:11 -0400
parents 95e24b629ad9
children 02e8e9ef2746
comparison
equal deleted inserted replaced
38:95e24b629ad9 39:fd18331e5c0b
1096 1096
1097 (** %\begin{enumerate}%#<ol># 1097 (** %\begin{enumerate}%#<ol>#
1098 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># 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 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 meanings of expressions.#</li># 1101 %\item%#<li># Modify the first example language of Chapter 2 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 meanings of expressions.#</li>#
1102 1102
1103 %\item%#<li># Reimplement the second example language of Chapter 1 to use mutually-inductive types instead of dependent types. That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type. To keep things simple, you may consider only the binary operators that take naturals as operands. Add natural number variables to the language, as in the last exercise, and add an "if" expression form taking as arguments one boolean expression and two natural number expressions. Define semantics and constant-folding functions for this new language. Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also "if" expressions with known values for their test expressions but possibly undetermined "then" and "else" cases. Prove that constant-folding a natural number expression preserves its meaning.#</li># 1103 %\item%#<li># Reimplement the second example language of Chapter 2 to use mutually-inductive types instead of dependent types. That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type. To keep things simple, you may consider only the binary operators that take naturals as operands. Add natural number variables to the language, as in the last exercise, and add an "if" expression form taking as arguments one boolean expression and two natural number expressions. Define semantics and constant-folding functions for this new language. Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also "if" expressions with known values for their test expressions but possibly undetermined "then" and "else" cases. Prove that constant-folding a natural number expression preserves its meaning.#</li>#
1104 1104
1105 %\item%#<li># Using a reflexive inductive definition, define a type [nat_tree] of infinitary trees, with natural numbers at their leaves and a countable infinity of new trees branching out of each internal node. Define a function [increment] that increments the number in every leaf of a [nat_tree]. Define a function [leapfrog] over a natural [i] and a tree [nt]. [leapfrog] should recurse into the [i]th child of [nt], the [i+1]st child of that node, the [i+2]nd child of the next node, and so on, until reaching a leaf, in which case [leapfrog] should return the number at that leaf. Prove that the result of any call to [leapfrog] is incremented by one by calling [increment] on the tree.#</li># 1105 %\item%#<li># Using a reflexive inductive definition, define a type [nat_tree] of infinitary trees, with natural numbers at their leaves and a countable infinity of new trees branching out of each internal node. Define a function [increment] that increments the number in every leaf of a [nat_tree]. Define a function [leapfrog] over a natural [i] and a tree [nt]. [leapfrog] should recurse into the [i]th child of [nt], the [i+1]st child of that node, the [i+2]nd child of the next node, and so on, until reaching a leaf, in which case [leapfrog] should return the number at that leaf. Prove that the result of any call to [leapfrog] is incremented by one by calling [increment] on the tree.#</li>#
1106 1106
1107 %\item%#<li># Define a type of trees of trees of trees of (repeat to infinity). That is, define an inductive type [trexp], whose members are either base cases containing natural numbers or binary trees of [trexp]s. Base your definition on a parameterized binary tree type [btree] that you will also define, so that [trexp] is defined as a nested inductive type. Define a function [total] that sums all of the naturals at the leaves of a [trexp]. Define a function [increment] that increments every leaf of a [trexp] by one. Prove that, for all [tr], [total (increment tr) >= total tr]. On the way to finishing this proof, you will probably want to prove a lemma and add it as a hint using the syntax [Hint Resolve name_of_lemma.].#</li># 1107 %\item%#<li># Define a type of trees of trees of trees of (repeat to infinity). That is, define an inductive type [trexp], whose members are either base cases containing natural numbers or binary trees of [trexp]s. Base your definition on a parameterized binary tree type [btree] that you will also define, so that [trexp] is defined as a nested inductive type. Define a function [total] that sums all of the naturals at the leaves of a [trexp]. Define a function [increment] that increments every leaf of a [trexp] by one. Prove that, for all [tr], [total (increment tr) >= total tr]. On the way to finishing this proof, you will probably want to prove a lemma and add it as a hint using the syntax [Hint Resolve name_of_lemma.].#</li>#
1108 1108